English
Let x be a nonnegative extended real number and y, z be real numbers. Then x^(y z) = (x^y)^z.
Русский
Пусть x ∈ ℝ≥0∞ и y, z ∈ ℝ. Тогда x^(y z) = (x^y)^z.
LaTeX
$$$ x^{y z} = (x^{y})^{z} $$$
Lean4
theorem rpow_mul (x : ℝ≥0∞) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z := by
cases x with
| top =>
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;> rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
| coe x =>
by_cases h : x = 0
·
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;> rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos, mul_pos_of_neg_of_neg,
mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
· have : x ^ y ≠ 0 := by simp [h]
simp [← coe_rpow_of_ne_zero, h, this, NNReal.rpow_mul]
