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_lt_rpow zero_le_one hx hz