case h.e'_4
x✝ y z✝ x z : ℝ
hx : 1 < x
hz : z < 0
⊢ 1 = x ^ 0
x✝ y z✝ x z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < 1
convert rpow_lt_rpow_of_exponent_lt hx hz
no goals
case h.e'_4
x✝ y z✝ x z : ℝ
hx : 1 < x
hz : z < 0
⊢ 1 = x ^ 0
exact (rpow_zero x).symm