case h.e'_3
x y z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 = x ^ 0
x y z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 ≤ x ^ z
convert rpow_le_rpow_of_exponent_ge hx1 hx2 hz
no goals
case h.e'_3
x y z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z ≤ 0
⊢ 1 = x ^ 0
exact (rpow_zero x).symm