English
If a,b ∈ ℝ are nonnegative, then (a b)^r = a^r b^r for any complex r.
Русский
Пусть a,b ∈ ℝ, a ≥ 0 и b ≥ 0. Тогда (a b)^r = a^r b^r для любого комплексного r.
LaTeX
$$$(a b)^r = a^r b^r \quad \text{если } a,b \ge 0$$$
Lean4
theorem mul_cpow_ofReal_nonneg {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (r : ℂ) :
((a : ℂ) * (b : ℂ)) ^ r = (a : ℂ) ^ r * (b : ℂ) ^ r :=
by
rcases eq_or_ne r 0 with (rfl | hr)
· simp only [cpow_zero, mul_one]
rcases eq_or_lt_of_le ha with (rfl | ha')
· rw [ofReal_zero, zero_mul, zero_cpow hr, zero_mul]
rcases eq_or_lt_of_le hb with (rfl | hb')
· rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]
have ha'' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha'.ne'
have hb'' : (b : ℂ) ≠ 0 := ofReal_ne_zero.mpr hb'.ne'
rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha, add_mul, exp_add, ←
cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']
