x✝ y z✝ x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ^ z ≤ x ^ z
x✝ y z✝ x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ≤ x ^ z
rw [← one_rpow z]
no goals
x✝ y z✝ x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ^ z ≤ x ^ z
exact rpow_le_rpow zero_le_one hx hz