x : ℝ≥0
y : ℝ
⊢ ↑x ^ y = ↑0 ↔ ↑x = 0 ∧ y ≠ 0
x : ℝ≥0
y : ℝ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
rw [← NNReal.coe_eq, coe_rpow, ← NNReal.coe_eq_zero]
no goals
x : ℝ≥0
y : ℝ
⊢ ↑x ^ y = ↑0 ↔ ↑x = 0 ∧ y ≠ 0
exact Real.rpow_eq_zero_iff_of_nonneg x.2