x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ x ^ y
rw [rpow_def_of_nonneg hx]
no goals
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else exp (log x * y)
split_ifs <;>
simp only [zero_le_one, le_refl, le_of_lt (exp_pos _)]