Theorem expaddd

Description: Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of Gleason p. 135. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	expcld.1	$$⊢\phi \to A\in ℂ$$
	expcld.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	expaddd.2	$$⊢\phi \to M\in {\mathbb{N}}_0$$
Assertion	expaddd	$$⊢\phi \to A^{M+N}=A^M{A}^N$$

Proof

Step	Hyp	Ref	Expression
1		expcld.1	$$⊢\phi \to A\in ℂ$$
2		expcld.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
3		expaddd.2	$$⊢\phi \to M\in {\mathbb{N}}_0$$
4		expadd	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to A^{M+N}=A^M{A}^N$$
5	1 3 2 4	syl3anc	$$⊢\phi \to A^{M+N}=A^M{A}^N$$