Theorem mulexpt 6525

Description: Natural number exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents.

Assertion

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

Proof of Theorem mulexpt

Step	Hyp	Ref	Expression
1		opreq2 3954	. . . . . . 7 |- (j = 0 -> ((A x. B)^j) = ((A x. B)^0))
2		opreq2 3954	. . . . . . . 8 |- (j = 0 -> (A^j) = (A^0))
3		opreq2 3954	. . . . . . . 8 |- (j = 0 -> (B^j) = (B^0))
4	2, 3	opreq12d 3963	. . . . . . 7 |- (j = 0 -> ((A^j) x. (B^j)) = ((A^0) x. (B^0)))
5	1, 4	eqeq12d 1481	. . . . . 6 |- (j = 0 -> (((A x. B)^j) = ((A^j) x. (B^j)) <-> ((A x. B)^0) = ((A^0) x. (B^0))))
6	5	imbi2d 610	. . . . 5 |- (j = 0 -> (((A e. CC /\ B e. CC) -> ((A x. B)^j) = ((A^j) x. (B^j))) <-> ((A e. CC /\ B e. CC) -> ((A x. B)^0) = ((A^0) x. (B^0)))))
7		opreq2 3954	. . . . . . 7 |- (j = k -> ((A x. B)^j) = ((A x. B)^k))
8		opreq2 3954	. . . . . . . 8 |- (j = k -> (A^j) = (A^k))
9		opreq2 3954	. . . . . . . 8 |- (j = k -> (B^j) = (B^k))
10	8, 9	opreq12d 3963	. . . . . . 7 |- (j = k -> ((A^j) x. (B^j)) = ((A^k) x. (B^k)))
11	7, 10	eqeq12d 1481	. . . . . 6 |- (j = k -> (((A x. B)^j) = ((A^j) x. (B^j)) <-> ((A x. B)^k) = ((A^k) x. (B^k))))
12	11	imbi2d 610	. . . . 5 |- (j = k -> (((A e. CC /\ B e. CC) -> ((A x. B)^j) = ((A^j) x. (B^j))) <-> ((A e. CC /\ B e. CC) -> ((A x. B)^k) = ((A^k) x. (B^k)))))
13		opreq2 3954	. . . . . . 7 |- (j = (k + 1) -> ((A x. B)^j) = ((A x. B)^(k + 1)))
14		opreq2 3954	. . . . . . . 8 |- (j = (k + 1) -> (A^j) = (A^(k + 1)))
15		opreq2 3954	. . . . . . . 8 |- (j = (k + 1) -> (B^j) = (B^(k + 1)))
16	14, 15	opreq12d 3963	. . . . . . 7 |- (j = (k + 1) -> ((A^j) x. (B^j)) = ((A^(k + 1)) x. (B^(k + 1))))
17	13, 16	eqeq12d 1481	. . . . . 6 |- (j = (k + 1) -> (((A x. B)^j) = ((A^j) x. (B^j)) <-> ((A x. B)^(k + 1)) = ((A^(k + 1)) x. (B^(k + 1)))))
18	17	imbi2d 610	. . . . 5 |- (j = (k + 1) -> (((A e. CC /\ B e. CC) -> ((A x. B)^j) = ((A^j) x. (B^j))) <-> ((A e. CC /\ B e. CC) -> ((A x. B)^(k + 1)) = ((A^(k + 1)) x. (B^(k + 1))))))
19		opreq2 3954	. . . . . . 7 |- (j = N -> ((A x. B)^j) = ((A x. B)^N))
20		opreq2 3954	. . . . . . . 8 |- (j = N -> (A^j) = (A^N))
21		opreq2 3954	. . . . . . . 8 |- (j = N -> (B^j) = (B^N))
22	20, 21	opreq12d 3963	. . . . . . 7 |- (j = N -> ((A^j) x. (B^j)) = ((A^N) x. (B^N)))
23	19, 22	eqeq12d 1481	. . . . . 6 |- (j = N -> (((A x. B)^j) = ((A^j) x. (B^j)) <-> ((A x. B)^N) = ((A^N) x. (B^N))))
24	23	imbi2d 610	. . . . 5 |- (j = N -> (((A e. CC /\ B e. CC) -> ((A x. B)^j) = ((A^j) x. (B^j))) <-> ((A e. CC /\ B e. CC) -> ((A x. B)^N) = ((A^N) x. (B^N)))))
25		axmulcl 5245	. . . . . . 7 |- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)
26		exp0t 6503	. . . . . . 7 |- ((A x. B) e. CC -> ((A x. B)^0) = 1)
27	25, 26	syl 10	. . . . . 6 |- ((A e. CC /\ B e. CC) -> ((A x. B)^0) = 1)
28		exp0t 6503	. . . . . . . 8 |- (A e. CC -> (A^0) = 1)
29		exp0t 6503	. . . . . . . 8 |- (B e. CC -> (B^0) = 1)
30	28, 29	opreqan12d 3964	. . . . . . 7 |- ((A e. CC /\ B e. CC) -> ((A^0) x. (B^0)) = (1 x. 1))
31		ax1cn 5241	. . . . . . . 8 |- 1 e. CC
32	31	mulid1 5304	. . . . . . 7 |- (1 x. 1) = 1
33	30, 32	syl6eq 1515	. . . . . 6 |- ((A e. CC /\ B e. CC) -> ((A^0) x. (B^0)) = 1)
34	27, 33	eqtr4d 1502	. . . . 5 |- ((A e. CC /\ B e. CC) -> ((A x. B)^0) = ((A^0) x. (B^0)))
35		expp1t 6506	. . . . . . . . . . 11 |- (((A x. B) e. CC /\ k e. NN0) -> ((A x. B)^(k + 1)) = (((A x. B)^k) x. (A x. B)))
36	35, 25	sylan 448	. . . . . . . . . 10 |- (((A e. CC /\ B e. CC) /\ k e. NN0) -> ((A x. B)^(k + 1)) = (((A x. B)^k) x. (A x. B)))
37	36	adantr 389	. . . . . . . . 9 |- ((((A e. CC /\ B e. CC) /\ k e. NN0) /\ ((A x. B)^k) = ((A^k) x. (B^k))) -> ((A x. B)^(k + 1)) = (((A x. B)^k) x. (A x. B)))
38		opreq1 3953	. . . . . . . . . 10 |- (((A x. B)^k) = ((A^k) x. (B^k)) -> (((A x. B)^k) x. (A x. B)) = (((A^k) x. (B^k)) x. (A x. B)))
39	38	adantl 388	. . . . . . . . 9 |- ((((A e. CC /\ B e. CC) /\ k e. NN0) /\ ((A x. B)^k) = ((A^k) x. (B^k))) -> (((A x. B)^k) x. (A x. B)) = (((A^k) x. (B^k)) x. (A x. B)))
40		mul4t 5392	. . . . . . . . . . . 12 |- ((((A^k) e. CC /\ (B^k) e. CC) /\ (A e. CC /\ B e. CC)) -> (((A^k) x. (B^k)) x. (A x. B)) = (((A^k) x. A) x. ((B^k) x. B)))
41		expclt 6513	. . . . . . . . . . . . . 14 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
42		expclt 6513	. . . . . . . . . . . . . 14 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
43	41, 42	anim12i 333	. . . . . . . . . . . . 13 |- (((A e. CC /\ k e. NN0) /\ (B e. CC /\ k e. NN0)) -> ((A^k) e. CC /\ (B^k) e. CC))
44	43	anandirs 512	. . . . . . . . . . . 12 |- (((A e. CC /\ B e. CC) /\ k e. NN0) -> ((A^k) e. CC /\ (B^k) e. CC))
45		pm3.26 319	. . . . . . . . . . . 12 |- (((A e. CC /\ B e. CC) /\ k e. NN0) -> (A e. CC /\ B e. CC))
46	40, 44, 45	sylanc 471	. . . . . . . . . . 11 |- (((A e. CC /\ B e. CC) /\ k e. NN0) -> (((A^k) x. (B^k)) x. (A x. B)) = (((A^k) x. A) x. ((B^k) x. B)))
47		expp1t 6506	. . . . . . . . . . . . 13 |- ((A e. CC /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
48	47	adantlr 393	. . . . . . . . . . . 12 |- (((A e. CC /\ B e. CC) /\ k e. NN0) -> (A^(k + 1)) = ((A^k) x. A))
49		expp1t 6506	. . . . . . . . . . . . 13 |- ((B e. CC /\ k e. NN0) -> (B^(k + 1)) = ((B^k) x. B))
50	49	adantll 392	. . . . . . . . . . . 12 |- (((A e. CC /\ B e. CC) /\ k e. NN0) -> (B^(k + 1)) = ((B^k) x. B))
51	48, 50	opreq12d 3963	. . . . . . . . . . 11 |- (((A e. CC /\ B e. CC) /\ k e. NN0) -> ((A^(k + 1)) x. (B^(k + 1))) = (((A^k) x. A) x. ((B^k) x. B)))
52	46, 51	eqtr4d 1502	. . . . . . . . . 10 |- (((A e. CC /\ B e. CC) /\ k