English
x^(y+z) = x^y · x^z for ENat.
Русский
x^(y+z) = x^y · x^z для ENat.
LaTeX
$$$ \forall x,y,z \in \mathbb{N}_\infty,\; x^{y+z} = x^y \cdot x^z. $$$
Lean4
theorem epow_add : x ^ (y + z) = x ^ y * x ^ z :=
by
rcases lt_trichotomy x 1 with x_0 | rfl | x_2
· rw [lt_one_iff_eq_zero.1 x_0]
rcases eq_zero_or_pos y with rfl | y_0
· simp only [zero_add, epow_zero, one_mul]
· rw [zero_epow y_0.ne.symm, zero_mul]
exact zero_epow (add_pos_of_pos_of_nonneg y_0 bot_le).ne.symm
· simp only [one_epow, mul_one]
· induction y
· rw [top_add, epow_top x_2, top_mul]
exact one_le_iff_ne_zero.1 (one_le_epow (one_le_iff_ne_zero.1 x_2.le))
induction z
· rw [add_top, epow_top x_2, mul_top]
exact one_le_iff_ne_zero.1 (one_le_epow (one_le_iff_ne_zero.1 x_2.le))
simp only [← Nat.cast_add, epow_natCast, pow_add x]
