English
For integers m,n, if a ≠ 0 or m+n ≠ 0 or m = 0 and n = 0, then a^{m+n} = a^{m} · a^{n}.
Русский
Для целых m,n, при условии a ≠ 0 или m+n ≠ 0 или m = 0 и n = 0, выполняется a^{m+n} = a^{m} · a^{n}.
LaTeX
$$$a \\\\neq 0 \\\\lor (m+n) \\\\neq 0 \\\\lor (m=0 \\\\land n=0) \\\\rightarrow a^{m+n} = a^{m} \\\\cdot a^{n}$$$
Lean4
theorem zpow_add' {m n : ℤ} (h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0) : a ^ (m + n) = a ^ m * a ^ n :=
by
by_cases hm : m = 0
· simp [hm]
by_cases hn : n = 0
· simp [hn]
by_cases ha : a = 0
· subst a
simp only [false_or, not_true, Ne, hm, hn, false_and, or_false] at h
rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
· exact zpow_add₀ ha m n
