Theorem expmult 6597

Description: Product of exponents law for natural number exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents.

Assertion

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

Proof of Theorem expmult

Step	Hyp	Ref	Expression
1		opreq2 3969	. . . . . . . 8 |- (j = 0 -> (M x. j) = (M x. 0))
2	1	opreq2d 3976	. . . . . . 7 |- (j = 0 -> (A^(M x. j)) = (A^(M x. 0)))
3		opreq2 3969	. . . . . . 7 |- (j = 0 -> ((A^M)^j) = ((A^M)^0))
4	2, 3	eqeq12d 1489	. . . . . 6 |- (j = 0 -> ((A^(M x. j)) = ((A^M)^j) <-> (A^(M x. 0)) = ((A^M)^0)))
5	4	imbi2d 612	. . . . 5 |- (j = 0 -> (((A e. CC /\ M e. NN0) -> (A^(M x. j)) = ((A^M)^j)) <-> ((A e. CC /\ M e. NN0) -> (A^(M x. 0)) = ((A^M)^0))))
6		opreq2 3969	. . . . . . . 8 |- (j = k -> (M x. j) = (M x. k))
7	6	opreq2d 3976	. . . . . . 7 |- (j = k -> (A^(M x. j)) = (A^(M x. k)))
8		opreq2 3969	. . . . . . 7 |- (j = k -> ((A^M)^j) = ((A^M)^k))
9	7, 8	eqeq12d 1489	. . . . . 6 |- (j = k -> ((A^(M x. j)) = ((A^M)^j) <-> (A^(M x. k)) = ((A^M)^k)))
10	9	imbi2d 612	. . . . 5 |- (j = k -> (((A e. CC /\ M e. NN0) -> (A^(M x. j)) = ((A^M)^j)) <-> ((A e. CC /\ M e. NN0) -> (A^(M x. k)) = ((A^M)^k))))
11		opreq2 3969	. . . . . . . 8 |- (j = (k + 1) -> (M x. j) = (M x. (k + 1)))
12	11	opreq2d 3976	. . . . . . 7 |- (j = (k + 1) -> (A^(M x. j)) = (A^(M x. (k + 1))))
13		opreq2 3969	. . . . . . 7 |- (j = (k + 1) -> ((A^M)^j) = ((A^M)^(k + 1)))
14	12, 13	eqeq12d 1489	. . . . . 6 |- (j = (k + 1) -> ((A^(M x. j)) = ((A^M)^j) <-> (A^(M x. (k + 1))) = ((A^M)^(k + 1))))
15	14	imbi2d 612	. . . . 5 |- (j = (k + 1) -> (((A e. CC /\ M e. NN0) -> (A^(M x. j)) = ((A^M)^j)) <-> ((A e. CC /\ M e. NN0) -> (A^(M x. (k + 1))) = ((A^M)^(k + 1)))))
16		opreq2 3969	. . . . . . . 8 |- (j = N -> (M x. j) = (M x. N))
17	16	opreq2d 3976	. . . . . . 7 |- (j = N -> (A^(M x. j)) = (A^(M x. N)))
18		opreq2 3969	. . . . . . 7 |- (j = N -> ((A^M)^j) = ((A^M)^N))
19	17, 18	eqeq12d 1489	. . . . . 6 |- (j = N -> ((A^(M x. j)) = ((A^M)^j) <-> (A^(M x. N)) = ((A^M)^N)))
20	19	imbi2d 612	. . . . 5 |- (j = N -> (((A e. CC /\ M e. NN0) -> (A^(M x. j)) = ((A^M)^j)) <-> ((A e. CC /\ M e. NN0) -> (A^(M x. N)) = ((A^M)^N))))
21		nn0cnt 6109	. . . . . . . . 9 |- (M e. NN0 -> M e. CC)
22		mul01t 5443	. . . . . . . . 9 |- (M e. CC -> (M x. 0) = 0)
23	21, 22	syl 10	. . . . . . . 8 |- (M e. NN0 -> (M x. 0) = 0)
24	23	opreq2d 3976	. . . . . . 7 |- (M e. NN0 -> (A^(M x. 0)) = (A^0))
25		exp0t 6571	. . . . . . 7 |- (A e. CC -> (A^0) = 1)
26	24, 25	sylan9eqr 1529	. . . . . 6 |- ((A e. CC /\ M e. NN0) -> (A^(M x. 0)) = 1)
27		expclt 6581	. . . . . . 7 |- ((A e. CC /\ M e. NN0) -> (A^M) e. CC)
28		exp0t 6571	. . . . . . 7 |- ((A^M) e. CC -> ((A^M)^0) = 1)
29	27, 28	syl 10	. . . . . 6 |- ((A e. CC /\ M e. NN0) -> ((A^M)^0) = 1)
30	26, 29	eqtr4d 1510	. . . . 5 |- ((A e. CC /\ M e. NN0) -> (A^(M x. 0)) = ((A^M)^0))
31		ax1cn 5269	. . . . . . . . . . . . . . 15 |- 1 e. CC
32		axdistr 5279	. . . . . . . . . . . . . . 15 |- ((M e. CC /\ k e. CC /\ 1 e. CC) -> (M x. (k + 1)) = ((M x. k) + (M x. 1)))
33	31, 32	mp3an3 905	. . . . . . . . . . . . . 14 |- ((M e. CC /\ k e. CC) -> (M x. (k + 1)) = ((M x. k) + (M x. 1)))
34		ax1id 5282	. . . . . . . . . . . . . . . 16 |- (M e. CC -> (M x. 1) = M)
35	34	adantr 389	. . . . . . . . . . . . . . 15 |- ((M e. CC /\ k e. CC) -> (M x. 1) = M)
36	35	opreq2d 3976	. . . . . . . . . . . . . 14 |- ((M e. CC /\ k e. CC) -> ((M x. k) + (M x. 1)) = ((M x. k) + M))
37	33, 36	eqtrd 1507	. . . . . . . . . . . . 13 |- ((M e. CC /\ k e. CC) -> (M x. (k + 1)) = ((M x. k) + M))
38		nn0cnt 6109	. . . . . . . . . . . . 13 |- (k e. NN0 -> k e. CC)
39	37, 21, 38	syl2an 454	. . . . . . . . . . . 12 |- ((M e. NN0 /\ k e. NN0) -> (M x. (k + 1)) = ((M x. k) + M))
40	39	adantll 392	. . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (M x. (k + 1)) = ((M x. k) + M))
41	40	opreq2d 3976	. . . . . . . . . 10 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^(M x. (k + 1))) = (A^((M x. k) + M)))
42		expaddt 6596	. . . . . . . . . . 11 |- ((A e. CC /\ (M x. k) e. NN0 /\ M e. NN0) -> (A^((M x. k) + M)) = ((A^(M x. k)) x. (A^M)))
43		simpll 412	. . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> A e. CC)
44		nn0mulclt 6123	. . . . . . . . . . . 12 |- ((M e. NN0 /\ k e. NN0) -> (M x. k) e. NN0)
45	44	adantll 392	. . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (M x. k) e. NN0)
46		simplr 413	. . . . . . . . . . 11 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> M e. NN0)
47	42, 43, 45, 46	syl3anc 858	. . . . . . . . . 10 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^((M x. k) + M)) = ((A^(M x. k)) x. (A^M)))
48	41, 47	eqtrd 1507	. . . . . . . . 9 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> (A^(M x. (k + 1))) = ((A^(M x. k)) x. (A^M)))
49		expp1t 6574	. . . . . . . . . 10 |- (((A^M) e. CC /\ k e. NN0) -> ((A^M)^(k + 1)) = (((A^M)^k) x. (A^M)))
50	49, 27	sylan 448	. . . . . . . . 9 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> ((A^M)^(k + 1)) = (((A^M)^k) x. (A^M)))
51	48, 50	eqeq12d 1489	. . . . . . . 8 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> ((A^(M x. (k + 1))) = ((A^M)^(k + 1)) <-> ((A^(M x. k)) x. (A^M)) = (((A^M)^k) x. (A^M))))
52		opreq1 3968	. . . . . . . 8 |- ((A^(M x. k)) = ((A^M)^k) -> ((A^(M x. k)) x. (A^M)) = (((A^M)^k) x. (A^M)))
53	51, 52	syl5bir 210	. . . . . . 7 |- (((A e. CC /\ M e. NN0) /\ k e. NN0) -> ((A^(M x. k)) = ((A^M)^k) -> (A^(M x. (k + 1))) = ((A^M)^(k + 1))))
54	53	expcom 374	. . . . . 6 |- (k e. NN0 -> ((A e. CC /\ M e. NN0) -> ((A^(M x. k)) = ((A^M)^k) -> (A^(M x. (k + 1))) = ((A^M)^(k + 1)))))
55	54	a2d 13	. . . . 5 |- (k e. NN0 -> (((A e. CC /\ M e. NN0) -> (A^(M x. k)) = ((A^M)^k)) -> ((A e. CC /\ M e. NN0) -> (A^(M x. (k + 1))) = ((A^M)^(k + 1)))