rpow_add' — Mathlib

English

If x ≥ 0 and y+z ≠ 0, then x^{y+z} = x^y x^z.

Русский

Если x ≥ 0 и y+z ≠ 0, то x^{y+z} = x^y x^z.

LaTeX

$$$\\forall x \\in \\mathbb{R}, x \\ge 0 \\Rightarrow \\forall y,z \\in \\mathbb{R}, y+z \\neq 0 \\Rightarrow x^{(y+z)} = x^y x^z$$$

Lean4

theorem rpow_add' (hx : 0 ≤ x) (h : y + z ≠ 0) : x ^ (y + z) = x ^ y * x ^ z :=
  by
  rcases hx.eq_or_lt with (rfl | pos)
  · rw [zero_rpow h, zero_eq_mul]
    have : y ≠ 0 ∨ z ≠ 0 := not_and_or.1 fun ⟨hy, hz⟩ => h <| hy.symm ▸ hz.symm ▸ zero_add 0
    exact this.imp zero_rpow zero_rpow
  · exact rpow_add pos _ _

Похожие утверждения