Theorem expaddt 4698

Description: Sum of exponents law for natural number exponentiation.

Assertion

Ref	Expression
expaddt	|- ((A e. CC /\ B e. NN /\ C e. NN) -> (A^(B + C)) = ((A^B) x. (A^C)))

Proof of Theorem expaddt

Step	Hyp	Ref	Expression
1		opreq2 3007	. . . . . . . 8 |- (x = 1 -> (B + x) = (B + 1))
2	1	opreq2d 3013	. . . . . . 7 |- (x = 1 -> (A^(B + x)) = (A^(B + 1)))
3		opreq2 3007	. . . . . . . 8 |- (x = 1 -> (A^x) = (A^1))
4	3	opreq2d 3013	. . . . . . 7 |- (x = 1 -> ((A^B) x. (A^x)) = ((A^B) x. (A^1)))
5	2, 4	cleq12d 1115	. . . . . 6 |- (x = 1 -> ((A^(B + x)) = ((A^B) x. (A^x)) <-> (A^(B + 1)) = ((A^B) x. (A^1))))
6	5	imbi2d 464	. . . . 5 |- (x = 1 -> (((A e. CC /\ B e. NN) -> (A^(B + x)) = ((A^B) x. (A^x))) <-> ((A e. CC /\ B e. NN) -> (A^(B + 1)) = ((A^B) x. (A^1)))))
7		opreq2 3007	. . . . . . . 8 |- (x = y -> (B + x) = (B + y))
8	7	opreq2d 3013	. . . . . . 7 |- (x = y -> (A^(B + x)) = (A^(B + y)))
9		opreq2 3007	. . . . . . . 8 |- (x = y -> (A^x) = (A^y))
10	9	opreq2d 3013	. . . . . . 7 |- (x = y -> ((A^B) x. (A^x)) = ((A^B) x. (A^y)))
11	8, 10	cleq12d 1115	. . . . . 6 |- (x = y -> ((A^(B + x)) = ((A^B) x. (A^x)) <-> (A^(B + y)) = ((A^B) x. (A^y))))
12	11	imbi2d 464	. . . . 5 |- (x = y -> (((A e. CC /\ B e. NN) -> (A^(B + x)) = ((A^B) x. (A^x))) <-> ((A e. CC /\ B e. NN) -> (A^(B + y)) = ((A^B) x. (A^y)))))
13		opreq2 3007	. . . . . . . 8 |- (x = (y + 1) -> (B + x) = (B + (y + 1)))
14	13	opreq2d 3013	. . . . . . 7 |- (x = (y + 1) -> (A^(B + x)) = (A^(B + (y + 1))))
15		opreq2 3007	. . . . . . . 8 |- (x = (y + 1) -> (A^x) = (A^(y + 1)))
16	15	opreq2d 3013	. . . . . . 7 |- (x = (y + 1) -> ((A^B) x. (A^x)) = ((A^B) x. (A^(y + 1))))
17	14, 16	cleq12d 1115	. . . . . 6 |- (x = (y + 1) -> ((A^(B + x)) = ((A^B) x. (A^x)) <-> (A^(B + (y + 1))) = ((A^B) x. (A^(y + 1)))))
18	17	imbi2d 464	. . . . 5 |- (x = (y + 1) -> (((A e. CC /\ B e. NN) -> (A^(B + x)) = ((A^B) x. (A^x))) <-> ((A e. CC /\ B e. NN) -> (A^(B + (y + 1))) = ((A^B) x. (A^(y + 1))))))
19		opreq2 3007	. . . . . . . 8 |- (x = C -> (B + x) = (B + C))
20	19	opreq2d 3013	. . . . . . 7 |- (x = C -> (A^(B + x)) = (A^(B + C)))
21		opreq2 3007	. . . . . . . 8 |- (x = C -> (A^x) = (A^C))
22	21	opreq2d 3013	. . . . . . 7 |- (x = C -> ((A^B) x. (A^x)) = ((A^B) x. (A^C)))
23	20, 22	cleq12d 1115	. . . . . 6 |- (x = C -> ((A^(B + x)) = ((A^B) x. (A^x)) <-> (A^(B + C)) = ((A^B) x. (A^C))))
24	23	imbi2d 464	. . . . 5 |- (x = C -> (((A e. CC /\ B e. NN) -> (A^(B + x)) = ((A^B) x. (A^x))) <-> ((A e. CC /\ B e. NN) -> (A^(B + C)) = ((A^B) x. (A^C)))))
25		expp1t 4678	. . . . . 6 |- ((A e. CC /\ B e. NN) -> (A^(B + 1)) = ((A^B) x. A))
26		exp1t 4679	. . . . . . . 8 |- (A e. CC -> (A^1) = A)
27	26	adantr 306	. . . . . . 7 |- ((A e. CC /\ B e. NN) -> (A^1) = A)
28	27	opreq2d 3013	. . . . . 6 |- ((A e. CC /\ B e. NN) -> ((A^B) x. (A^1)) = ((A^B) x. A))
29	25, 28	eqtr4d 1131	. . . . 5 |- ((A e. CC /\ B e. NN) -> (A^(B + 1)) = ((A^B) x. (A^1)))
30		1cn 4101	. . . . . . . . . . . . . . 15 |- 1 e. CC
31		axaddass 4072	. . . . . . . . . . . . . . 15 |- ((B e. CC /\ y e. CC /\ 1 e. CC) -> ((B + y) + 1) = (B + (y + 1)))
32	30, 31	mp3an3 641	. . . . . . . . . . . . . 14 |- ((B e. CC /\ y e. CC) -> ((B + y) + 1) = (B + (y + 1)))
33		nncnt 4428	. . . . . . . . . . . . . 14 |- (B e. NN -> B e. CC)
34		nncnt 4428	. . . . . . . . . . . . . 14 |- (y e. NN -> y e. CC)
35	32, 33, 34	syl2an 349	. . . . . . . . . . . . 13 |- ((B e. NN /\ y e. NN) -> ((B + y) + 1) = (B + (y + 1)))
36	35	adantll 309	. . . . . . . . . . . 12 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> ((B + y) + 1) = (B + (y + 1)))
37	36	opreq2d 3013	. . . . . . . . . . 11 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> (A^((B + y) + 1)) = (A^(B + (y + 1))))
38		expp1t 4678	. . . . . . . . . . . 12 |- ((A e. CC /\ (B + y) e. NN) -> (A^((B + y) + 1)) = ((A^(B + y)) x. A))
39		pm3.26 256	. . . . . . . . . . . . 13 |- ((A e. CC /\ B e. NN) -> A e. CC)
40	39	adantr 306	. . . . . . . . . . . 12 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> A e. CC)
41		nnaddclt 4436	. . . . . . . . . . . . 13 |- ((B e. NN /\ y e. NN) -> (B + y) e. NN)
42	41	adantll 309	. . . . . . . . . . . 12 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> (B + y) e. NN)
43	38, 40, 42	sylanc 361	. . . . . . . . . . 11 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> (A^((B + y) + 1)) = ((A^(B + y)) x. A))
44	37, 43	eqtr3d 1130	. . . . . . . . . 10 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> (A^(B + (y + 1))) = ((A^(B + y)) x. A))
45		expp1t 4678	. . . . . . . . . . . . 13 |- ((A e. CC /\ y e. NN) -> (A^(y + 1)) = ((A^y) x. A))
46	45	adantlr 310	. . . . . . . . . . . 12 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> (A^(y + 1)) = ((A^y) x. A))
47	46	opreq2d 3013	. . . . . . . . . . 11 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> ((A^B) x. (A^(y + 1))) = ((A^B) x. ((A^y) x. A)))
48		axmulass 4073	. . . . . . . . . . . 12 |- (((A^B) e. CC /\ (A^y) e. CC /\ A e. CC) -> (((A^B) x. (A^y)) x. A) = ((A^B) x. ((A^y) x. A)))
49		expclt 4696	. . . . . . . . . . . . 13 |- ((A e. CC /\ B e. NN) -> (A^B) e. CC)
50	49	adantr 306	. . . . . . . . . . . 12 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> (A^B) e. CC)
51		expclt 4696	. . . . . . . . . . . . 13 |- ((A e. CC /\ y e. NN) -> (A^y) e. CC)
52	51	adantlr 310	. . . . . . . . . . . 12 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> (A^y) e. CC)
53	48, 50, 52, 40	syl3anc 629	. . . . . . . . . . 11 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> (((A^B) x. (A^y)) x. A) = ((A^B) x. ((A^y) x. A)))
54	47, 53	eqtr4d 1131	. . . . . . . . . 10 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> ((A^B) x. (A^(y + 1))) = (((A^B) x. (A^y)) x. A))
55	44, 54	cleq12d 1115	. . . . . . . . 9 |- (((A e. CC /\ B e. NN) /\ y e. NN) -> ((A^(B + (y + 1))) = ((A^B) x. (A^(y + 1))) <-> ((A^(B + y)) x. A) = (((A^B) x. (A^y)) x. A)))
56		opreq1 3006	. . . . . . . . 9 |- ((A^(B + y)) = ((A^B) x. (A^y)) -> ((A^(B + y)) x. A) = (((A^B