Theorem expadd

Description: Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of Gleason p. 135. (Contributed by NM, 30-Nov-2004)

	Ref	Expression
Assertion	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$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢j=0\to M+j=M+0$$
2	1	oveq2d	$$⊢j=0\to A^{M+j}=A^{M+0}$$
3		oveq2	$$⊢j=0\to A^j=A^0$$
4	3	oveq2d	$$⊢j=0\to A^M{A}^j=A^M{A}^0$$
5	2 4	eqeq12d	$$⊢j=0\to \left(A^{M+j}=A^M{A}^j\leftrightarrow A^{M+0}=A^M{A}^0\right)$$
6	5	imbi2d	$$⊢j=0\to \left(\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+j}=A^M{A}^j\right)\leftrightarrow \left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+0}=A^M{A}^0\right)\right)$$
7		oveq2	$$⊢j=k\to M+j=M+k$$
8	7	oveq2d	$$⊢j=k\to A^{M+j}=A^{M+k}$$
9		oveq2	$$⊢j=k\to A^j=A^k$$
10	9	oveq2d	$$⊢j=k\to A^M{A}^j=A^M{A}^k$$
11	8 10	eqeq12d	$$⊢j=k\to \left(A^{M+j}=A^M{A}^j\leftrightarrow A^{M+k}=A^M{A}^k\right)$$
12	11	imbi2d	$$⊢j=k\to \left(\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+j}=A^M{A}^j\right)\leftrightarrow \left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+k}=A^M{A}^k\right)\right)$$
13		oveq2	$$⊢j=k+1\to M+j=M+k+1$$
14	13	oveq2d	$$⊢j=k+1\to A^{M+j}=A^{M+k+1}$$
15		oveq2	$$⊢j=k+1\to A^j=A^{k+1}$$
16	15	oveq2d	$$⊢j=k+1\to A^M{A}^j=A^M{A}^{k+1}$$
17	14 16	eqeq12d	$$⊢j=k+1\to \left(A^{M+j}=A^M{A}^j\leftrightarrow A^{M+k+1}=A^M{A}^{k+1}\right)$$
18	17	imbi2d	$$⊢j=k+1\to \left(\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+j}=A^M{A}^j\right)\leftrightarrow \left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+k+1}=A^M{A}^{k+1}\right)\right)$$
19		oveq2	$$⊢j=N\to M+j=M+N$$
20	19	oveq2d	$$⊢j=N\to A^{M+j}=A^{M+N}$$
21		oveq2	$$⊢j=N\to A^j=A^N$$
22	21	oveq2d	$$⊢j=N\to A^M{A}^j=A^M{A}^N$$
23	20 22	eqeq12d	$$⊢j=N\to \left(A^{M+j}=A^M{A}^j\leftrightarrow A^{M+N}=A^M{A}^N\right)$$
24	23	imbi2d	$$⊢j=N\to \left(\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+j}=A^M{A}^j\right)\leftrightarrow \left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+N}=A^M{A}^N\right)\right)$$
25		nn0cn	$$⊢M\in {\mathbb{N}}_0\to M\in ℂ$$
26	25	addridd	$$⊢M\in {\mathbb{N}}_0\to M+0=M$$
27	26	adantl	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to M+0=M$$
28	27	oveq2d	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+0}=A^M$$
29		expcl	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^M\in ℂ$$
30	29	mulridd	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^M\cdot 1=A^M$$
31	28 30	eqtr4d	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+0}=A^M\cdot 1$$
32		exp0	$$⊢A\in ℂ\to A^0=1$$
33	32	adantr	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^0=1$$
34	33	oveq2d	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^M{A}^0=A^M\cdot 1$$
35	31 34	eqtr4d	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+0}=A^M{A}^0$$
36		oveq1	$$⊢A^{M+k}=A^M{A}^k\to A^{M+k}A=A^M{A}^{k}A$$
37		nn0cn	$$⊢k\in {\mathbb{N}}_0\to k\in ℂ$$
38		ax-1cn	$$⊢1\in ℂ$$
39		addass	$$⊢\left(M\in ℂ\wedge k\in ℂ\wedge 1\in ℂ\right)\to M+k+1=M+k+1$$
40	38 39	mp3an3	$$⊢\left(M\in ℂ\wedge k\in ℂ\right)\to M+k+1=M+k+1$$
41	25 37 40	syl2an	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to M+k+1=M+k+1$$
42	41	adantll	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to M+k+1=M+k+1$$
43	42	oveq2d	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to A^{M+k+1}=A^{M+k+1}$$
44		simpll	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to A\in ℂ$$
45		nn0addcl	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{N}}_0\right)\to M+k\in {\mathbb{N}}_0$$
46	45	adantll	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to M+k\in {\mathbb{N}}_0$$
47		expp1	$$⊢\left(A\in ℂ\wedge M+k\in {\mathbb{N}}_0\right)\to A^{M+k+1}=A^{M+k}A$$
48	44 46 47	syl2anc	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to A^{M+k+1}=A^{M+k}A$$
49	43 48	eqtr3d	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to A^{M+k+1}=A^{M+k}A$$
50		expp1	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A^{k+1}=A^{k}A$$
51	50	adantlr	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to A^{k+1}=A^{k}A$$
52	51	oveq2d	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to A^M{A}^{k+1}=A^M{A}^{k}A$$
53	29	adantr	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to A^M\in ℂ$$
54		expcl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℂ$$
55	54	adantlr	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℂ$$
56	53 55 44	mulassd	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to A^M{A}^{k}A=A^M{A}^{k}A$$
57	52 56	eqtr4d	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to A^M{A}^{k+1}=A^M{A}^{k}A$$
58	49 57	eqeq12d	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to \left(A^{M+k+1}=A^M{A}^{k+1}\leftrightarrow A^{M+k}A=A^M{A}^{k}A\right)$$
59	36 58	imbitrrid	$$⊢\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\wedge k\in {\mathbb{N}}_0\right)\to \left(A^{M+k}=A^M{A}^k\to A^{M+k+1}=A^M{A}^{k+1}\right)$$
60	59	expcom	$$⊢k\in {\mathbb{N}}_0\to \left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to \left(A^{M+k}=A^M{A}^k\to A^{M+k+1}=A^M{A}^{k+1}\right)\right)$$
61	60	a2d	$$⊢k\in {\mathbb{N}}_0\to \left(\left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+k}=A^M{A}^k\right)\to \left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+k+1}=A^M{A}^{k+1}\right)\right)$$
62	6 12 18 24 35 61	nn0ind	$$⊢N\in {\mathbb{N}}_0\to \left(\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to A^{M+N}=A^M{A}^N\right)$$
63	62	expdcom	$$⊢A\in ℂ\to \left(M\in {\mathbb{N}}_0\to \left(N\in {\mathbb{N}}_0\to A^{M+N}=A^M{A}^N\right)\right)$$
64	63	3imp	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to A^{M+N}=A^M{A}^N$$