Theorem expaddt 6527

Description: Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135.

Assertion

Ref	Expression
expaddt	|- ((A e. CC /\ M e. NN0 /\ N e. NN0) -> (A^(M + N)) = ((A^M) x. (A^N)))

Proof of Theorem expaddt

Step	Hyp	Ref	Expression
1		opreq2 3954	. . . . . . . 8 |- (j = 0 -> (M + j) = (M + 0))
2	1	opreq2d 3961	. . . . . . 7 |- (j = 0 -> (A^(M + j)) = (A^(M + 0)))
3		opreq2 3954	. . . . . . . 8 |- (j = 0 -> (A^j) = (A^0))
4	3	opreq2d 3961	. . . . . . 7 |- (j = 0 -> ((A^M) x. (A^j)) = ((A^M) x. (A^0)))
5	2, 4	eqeq12d 1481	. . . . . 6 |- (j = 0 -> ((A^(M + j)) = ((A^M) x. (A^j)) <-> (A^(M + 0)) = ((A^M) x. (A^0))))
6	5	imbi2d 610	. . . . 5 |- (j = 0 -> (((A e. CC /\ M e. NN0) -> (A^(M + j)) = ((A^M) x. (A^j))) <-> ((A e. CC /\ M e. NN0) -> (A^(M + 0)) = ((A^M) x. (A^0)))))
7		opreq2 3954	. . . . . . . 8 |- (j = k -> (M + j) = (M + k))
8	7	opreq2d 3961	. . . . . . 7 |- (j = k -> (A^(M + j)) = (A^(M + k)))
9		opreq2 3954	. . . . . . . 8 |- (j = k -> (A^j) = (A^k))
10	9	opreq2d 3961	. . . . . . 7 |- (j = k -> ((A^M) x. (A^j)) = ((A^M) x. (A^k)))
11	8, 10	eqeq12d 1481	. . . . . 6 |- (j = k -> ((A^(M + j)) = ((A^M) x. (A^j)) <-> (A^(M + k)) = ((A^M) x. (A^k))))
12	11	imbi2d 610	. . . . 5 |- (j = k -> (((A e. CC /\ M e. NN0) -> (A^(M + j)) = ((A^M) x. (A^j))) <-> ((A e. CC /\ M e. NN0) -> (A^(M + k)) = ((A^M) x. (A^k)))))
13		opreq2 3954	. . . . . . . 8 |- (j = (k + 1) -> (M + j) = (M + (k + 1)))
14	13	opreq2d 3961	. . . . . . 7 |- (j = (k + 1) -> (A^(M + j)) = (A^(M + (k + 1))))
15		opreq2 3954	. . . . . . . 8 |- (j = (k + 1) -> (A^j) = (A^(k + 1)))
16	15	opreq2d 3961	. . . . . . 7 |- (j = (k + 1) -> ((A^M) x. (A^j)) = ((A^M) x. (A^(k + 1))))
17	14, 16	eqeq12d 1481	. . . . . 6 |- (j = (k + 1) -> ((A^(M + j)) = ((A^M) x. (A^j)) <-> (A^(M + (k + 1))) = ((A^M) x. (A^(k + 1)))))
18	17	imbi2d 610	. . . . 5 |- (j = (k + 1) -> (((A e. CC /\ M e. NN0) -> (A^(M + j)) = ((A^M) x. (A^j))) <-> ((A e. CC /\ M e. NN0) -> (A^(M + (k + 1))) = ((A^M) x. (A^(k + 1))))))
19		opreq2 3954	. . . . . . . 8 |- (j = N -> (M + j) = (M + N))
20	19	opreq2d 3961	. . . . . . 7 |- (j = N -> (A^(M + j)) = (A^(M + N)))
21		opreq2 3954	. . . . . . . 8 |- (j = N -> (A^j) = (A^N))
22	21	opreq2d 3961	. . . . . . 7 |- (j = N -> ((A^M) x. (A^j)) = ((A^M) x. (A^N)))
23	20, 22	eqeq12d 1481	. . . . . 6 |- (j = N -> ((A^(M + j)) = ((A^M) x. (A^j)) <-> (A^(M + N)) = ((A^M) x. (A^N))))
24	23	imbi2d 610	. . . . 5 |- (j = N -> (((A e. CC /\ M e. NN0) -> (A^(M + j)) = ((A^M) x. (A^j))) <-> ((A e. CC /\ M e. NN0) -> (A^(M + N)) = ((A^M) x. (A^N)))))
25		expclt 6513	. . . . . . 7 |- ((A e. CC /\ M e. NN0) -> (A^M) e. CC)
26		ax1id 5254	. . . . . . 7 |- ((A^M) e. CC -> ((A^M) x. 1) = (A^M))
27	25, 26	syl 10	. . . . . 6 |- ((A e. CC /\ M e. NN0) -> ((A^M) x. 1) = (A^M))
28		exp0t 6503	. . . . . . . 8 |- (A e. CC -> (A^0) = 1)
29	28	adantr 389	. . . . . . 7 |- ((A e. CC /\ M e. NN0) -> (A^0) = 1)
30	29	opreq2d 3961	. . . . . 6 |- ((A e. CC /\ M e. NN0) -> ((A^M) x. (A^0)) = ((A^M) x. 1))
31		nn0cnt 6056	. . . . . . . . 9 |- (M e. NN0 -> M e. CC)
32		ax0id 5253	. . . . . . . . 9 |- (M e. CC -> (M + 0) = M)
33	31, 32	syl 10	. . . . . . . 8 |- (M e. NN0 -> (M + 0) = M)
34	33	adantl 388	. . . . . . 7 |- ((A e. CC /\ M e. NN0) -> (M + 0) = M)
35	34	opreq2d 3961	. . . . . 6 |- ((A e. CC /\ M e. NN0) -> (A^(M + 0)) = (A^M))
36	27, 30, 35	3eqtr4rd 1510	. . . . 5 |- ((A e. CC /\ M e. NN0) -> (A^(M + 0)) = ((A^M) x. (A^0)))
37		ax1cn 5241	. . . . . . . . . . . . . 14 |- 1 e. CC
38		axaddass 5249	. . . . . . . . . . . . . 14 |- ((M e. CC /\ k e. CC /\ 1 e. CC) -> ((M + k) + 1) = (M + (k + 1)))
39	37, 38	mp3an3 902	. . . . . . . . . . . . 13 |- ((M e. CC /\ k e. CC) -> ((M + k) + 1) = (M + (k + 1)))
40		nn0cnt 6056	. . . . . . . . . . . . 13 |- (k e. NN0 -> k e. CC)
41	39, 31, 40	syl2an 454	. . . . . . . . . . . 12 |- ((M e. NN0 /\ k e. NN0) -> ((M + k) + 1) = (M + (k + 1)))
42	41	adantll 392	. . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> ((M + k) + 1) = (M + (k + 1)))
43	42	opreq2d 3961	. . . . . . . . . 10 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^((M + k) + 1)) = (A^(M + (k + 1))))
44		expp1t 6506	. . . . . . . . . . 11 |- ((A e. CC /\ (M + k) e. NN0) -> (A^((M + k) + 1)) = ((A^(M + k)) x. A))
45		simpll 412	. . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> A e. CC)
46		nn0addclt 6067	. . . . . . . . . . . 12 |- ((M e. NN0 /\ k e. NN0) -> (M + k) e. NN0)
47	46	adantll 392	. . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (M + k) e. NN0)
48	44, 45, 47	sylanc 471	. . . . . . . . . 10 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^((M + k) + 1)) = ((A^(M + k)) x. A))
49	43, 48	eqtr3d 1501	. . . . . . . . 9 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^(M + (k + 1))) = ((A^(M + k)) x. A))
50		expp1t 6506	. . . . . . . . . . . 12 |- ((A e. CC /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
51	50	adantlr 393	. . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
52	51	opreq2d 3961	. . . . . . . . . 10 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> ((A^M) x. (A^(k + 1))) = ((A^M) x. ((A^k) x. A)))
53		axmulass 5250	. . . . . . . . . . 11 |- (((A^M) e. CC /\ (A^k) e. CC /\ A e. CC) -> (((A^M) x. (A^k)) x. A) = ((A^M) x. ((A^k) x. A)))
54	25	adantr 389	. . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^M) e. CC)
55		expclt 6513	. . . . . . . . . . . 12 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
56	55	adantlr 393	. . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^k) e. CC)
57	53, 54, 56, 45	syl3anc 856	. . . . . . . . . 10 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (((A^M) x. (A^k)) x. A) = ((A^M) x. ((A^k) x. A)))
58	52, 57	eqtr4d 1502	. . . . . . . . 9 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> ((A^M) x. (A^(