x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (1 / z) ≤ y ^ 1 ↔ x ≤ y ^ z
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (1 / z) ≤ y ↔ x ≤ y ^ z
nth_rw 1 [← ENNReal.rpow_one y]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (1 / z) ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (1 / z) ≤ y ^ 1 ↔ x ≤ y ^ z
nth_rw 2 [← @_root_.mul_inv_cancel _ _ z hz.ne.symm]
no goals
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (1 / z) ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z
rw [ENNReal.rpow_mul, ← one_div, ENNReal.rpow_le_rpow_iff (one_div_pos.2 hz)]