x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ^ 1 ≤ x ^ z
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ≤ x ^ z
nth_rw 1 [← ENNReal.rpow_one x]
no goals
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ^ 1 ≤ x ^ z
exact ENNReal.rpow_le_rpow_of_exponent_le hx h_one_le