English
Let x ≥ 0. For all real y and z, x^y · x^z ≤ x^(y+z). The inequality is always true; equality can occur for x > 0 by the usual real-power law.
Русский
Пусть x ≥ 0. Для любых вещественных y и z выполнено неравенство x^y · x^z ≤ x^(y+z). Неравенство всегда верно; при x > 0 равенство достигается по обычному закону степеней.
LaTeX
$$$x \ge 0 \Rightarrow \forall y,z \in \mathbb{R},\ x^{y} \cdot x^{z} \le x^{y+z}$$$
Lean4
/-- For `0 ≤ x`, the only problematic case in the equality `x ^ y * x ^ z = x ^ (y + z)` is for
`x = 0` and `y + z = 0`, where the right-hand side is `1` while the left-hand side can vanish.
The inequality is always true, though, and given in this lemma. -/
theorem le_rpow_add {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ y * x ^ z ≤ x ^ (y + z) :=
by
rcases le_iff_eq_or_lt.1 hx with (H | pos)
· by_cases h : y + z = 0
· simp only [H.symm, h, rpow_zero]
calc
(0 : ℝ) ^ y * 0 ^ z ≤ 1 * 1 :=
mul_le_mul (zero_rpow_le_one y) (zero_rpow_le_one z) (zero_rpow_nonneg z) zero_le_one
_ = 1 := by simp
· simp [rpow_add', ← H, h]
· simp [rpow_add pos]
