Theorem efexpt 7322

Description: Exponential function to a nonnegative integer power. Corollary 15-4.4 of [Gleason] p. 309, restricted to nonnegative integers.

Assertion

Ref	Expression
efexpt	|- ((A e. CC /\ N e. NN0) -> (exp` (N x. A)) = ((exp` A)^N))

Proof of Theorem efexpt

Step	Hyp	Ref	Expression
1		axmulcom 5256	. . . 4 |- ((A e. CC /\ N e. CC) -> (A x. N) = (N x. A))
2		nn0cnt 6064	. . . 4 |- (N e. NN0 -> N e. CC)
3	1, 2	sylan2 451	. . 3 |- ((A e. CC /\ N e. NN0) -> (A x. N) = (N x. A))
4	3	fveq2d 3719	. 2 |- ((A e. CC /\ N e. NN0) -> (exp` (A x. N)) = (exp` (N x. A)))
5		opreq1 3959	. . . . . . . . 9 |- ((exp` (A x. k)) = ((exp` A)^k) -> ((exp` (A x. k)) x. (exp` A)) = (((exp` A)^k) x. (exp` A)))
6	5	adantl 388	. . . . . . . 8 |- (((A e. CC /\ k e. NN0) /\ (exp` (A x. k)) = ((exp` A)^k)) -> ((exp` (A x. k)) x. (exp` A)) = (((exp` A)^k) x. (exp` A)))
7		ax1cn 5249	. . . . . . . . . . . . . 14 |- 1 e. CC
8		axdistr 5259	. . . . . . . . . . . . . 14 |- ((A e. CC /\ k e. CC /\ 1 e. CC) -> (A x. (k + 1)) = ((A x. k) + (A x. 1)))
9	7, 8	mp3an3 903	. . . . . . . . . . . . 13 |- ((A e. CC /\ k e. CC) -> (A x. (k + 1)) = ((A x. k) + (A x. 1)))
10		ax1id 5262	. . . . . . . . . . . . . . 15 |- (A e. CC -> (A x. 1) = A)
11	10	adantr 389	. . . . . . . . . . . . . 14 |- ((A e. CC /\ k e. CC) -> (A x. 1) = A)
12	11	opreq2d 3967	. . . . . . . . . . . . 13 |- ((A e. CC /\ k e. CC) -> ((A x. k) + (A x. 1)) = ((A x. k) + A))
13	9, 12	eqtrd 1504	. . . . . . . . . . . 12 |- ((A e. CC /\ k e. CC) -> (A x. (k + 1)) = ((A x. k) + A))
14		nn0cnt 6064	. . . . . . . . . . . 12 |- (k e. NN0 -> k e. CC)
15	13, 14	sylan2 451	. . . . . . . . . . 11 |- ((A e. CC /\ k e. NN0) -> (A x. (k + 1)) = ((A x. k) + A))
16	15	fveq2d 3719	. . . . . . . . . 10 |- ((A e. CC /\ k e. NN0) -> (exp` (A x. (k + 1))) = (exp` ((A x. k) + A)))
17		efaddt 7317	. . . . . . . . . . 11 |- (((A x. k) e. CC /\ A e. CC) -> (exp` ((A x. k) + A)) = ((exp` (A x. k)) x. (exp` A)))
18		axmulcl 5253	. . . . . . . . . . . 12 |- ((A e. CC /\ k e. CC) -> (A x. k) e. CC)
19	18, 14	sylan2 451	. . . . . . . . . . 11 |- ((A e. CC /\ k e. NN0) -> (A x. k) e. CC)
20		pm3.26 319	. . . . . . . . . . 11 |- ((A e. CC /\ k e. NN0) -> A e. CC)
21	17, 19, 20	sylanc 471	. . . . . . . . . 10 |- ((A e. CC /\ k e. NN0) -> (exp` ((A x. k) + A)) = ((exp` (A x. k)) x. (exp` A)))
22	16, 21	eqtrd 1504	. . . . . . . . 9 |- ((A e. CC /\ k e. NN0) -> (exp` (A x. (k + 1))) = ((exp` (A x. k)) x. (exp` A)))
23	22	adantr 389	. . . . . . . 8 |- (((A e. CC /\ k e. NN0) /\ (exp` (A x. k)) = ((exp` A)^k)) -> (exp` (A x. (k + 1))) = ((exp` (A x. k)) x. (exp` A)))
24		expp1t 6514	. . . . . . . . . 10 |- (((exp` A) e. CC /\ k e. NN0) -> ((exp` A)^(k + 1)) = (((exp` A)^k) x. (exp` A)))
25		efclt 7262	. . . . . . . . . 10 |- (A e. CC -> (exp` A) e. CC)
26	24, 25	sylan 448	. . . . . . . . 9 |- ((A e. CC /\ k e. NN0) -> ((exp` A)^(k + 1)) = (((exp` A)^k) x. (exp` A)))
27	26	adantr 389	. . . . . . . 8 |- (((A e. CC /\ k e. NN0) /\ (exp` (A x. k)) = ((exp` A)^k)) -> ((exp` A)^(k + 1)) = (((exp` A)^k) x. (exp` A)))
28	6, 23, 27	3eqtr4d 1514	. . . . . . 7 |- (((A e. CC /\ k e. NN0) /\ (exp` (A x. k)) = ((exp` A)^k)) -> (exp` (A x. (k + 1))) = ((exp` A)^(k + 1)))
29	28	ex 373	. . . . . 6 |- ((A e. CC /\ k e. NN0) -> ((exp` (A x. k)) = ((exp` A)^k) -> (exp` (A x. (k + 1))) = ((exp` A)^(k + 1))))
30	29	expcom 374	. . . . 5 |- (k e. NN0 -> (A e. CC -> ((exp` (A x. k)) = ((exp` A)^k) -> (exp` (A x. (k + 1))) = ((exp` A)^(k + 1)))))
31	30	a2d 13	. . . 4 |- (k e. NN0 -> ((A e. CC -> (exp` (A x. k)) = ((exp` A)^k)) -> (A e. CC -> (exp` (A x. (k + 1))) = ((exp` A)^(k + 1)))))
32		ef0 7285	. . . . 5 |- (exp` 0) = 1
33		mul01t 5423	. . . . . 6 |- (A e. CC -> (A x. 0) = 0)
34	33	fveq2d 3719	. . . . 5 |- (A e. CC -> (exp` (A x. 0)) = (exp` 0))
35		exp0t 6511	. . . . . 6 |- ((exp` A) e. CC -> ((exp` A)^0) = 1)
36	25, 35	syl 10	. . . . 5 |- (A e. CC -> ((exp` A)^0) = 1)
37	32, 34, 36	3eqtr4a 1529	. . . 4 |- (A e. CC -> (exp` (A x. 0)) = ((exp` A)^0))
38		opreq2 3960	. . . . . . 7 |- (j = 0 -> (A x. j) = (A x. 0))
39	38	fveq2d 3719	. . . . . 6 |- (j = 0 -> (exp` (A x. j)) = (exp` (A x. 0)))
40		opreq2 3960	. . . . . 6 |- (j = 0 -> ((exp` A)^j) = ((exp` A)^0))
41	39, 40	eqeq12d 1486	. . . . 5 |- (j = 0 -> ((exp` (A x. j)) = ((exp` A)^j) <-> (exp` (A x. 0)) = ((exp` A)^0)))
42	41	imbi2d 611	. . . 4 |- (j = 0 -> ((A e. CC -> (exp` (A x. j)) = ((exp` A)^j)) <-> (A e. CC -> (exp` (A x. 0)) = ((exp` A)^0))))
43		opreq2 3960	. . . . . . 7 |- (j = k -> (A x. j) = (A x. k))
44	43	fveq2d 3719	. . . . . 6 |- (j = k -> (exp` (A x. j)) = (exp` (A x. k)))
45		opreq2 3960	. . . . . 6 |- (j = k -> ((exp` A)^j) = ((exp` A)^k))
46	44, 45	eqeq12d 1486	. . . . 5 |- (j = k -> ((exp` (A x. j)) = ((exp` A)^j) <-> (exp` (A x. k)) = ((exp` A)^k)))
47	46	imbi2d 611	. . . 4 |- (j = k -> ((A e. CC -> (exp` (A x. j)) = ((exp` A)^j)) <-> (A e. CC -> (exp` (A x. k)) = ((exp` A)^k))))
48		opreq2 3960	. . . . . . 7 |- (j = (k + 1) -> (A x. j) = (A x. (k + 1)))
49	48	fveq2d 3719	. . . . . 6 |- (j = (k + 1) -> (exp` (A x. j)) = (exp` (A x. (k + 1))))
50		opreq2 3960	. . . . . 6 |- (j = (k + 1) -> ((exp` A)^j) = ((exp` A)^(k + 1)))
51	49, 50	eqeq12d 1486	. . . . 5 |- (j = (k + 1) -> ((exp` (A x. j)) = ((exp` A)^j) <-> (exp` (A x. (k + 1))) = ((exp` A)^(k + 1))))
52	51	imbi2d 611	. . . 4 |- (j = (k + 1) -> ((A e. CC -> (exp` (A x. j)) = ((exp` A)^j)) <-> (A e. CC -> (exp` (A x. (k + 1))) = ((exp` A)^(k + 1)))))
53		opreq2 3960	. . . . . . 7 |- (j = N -> (A x. j) = (A x. N))
54	53	fveq2d 3719	. . . . . 6 |- (j = N -> (exp` (A x. j)) = (exp` (A x. N)))
55		opreq2 3960	. . . . . 6 |- (j = N -> ((exp` A)^j) = ((exp` A)^N))
56	54, 55	eqeq12d 1486	. . . . 5 |- (j = N -> ((exp` (A x. j)) = ((exp` A)^j) <-> (exp` (A x. N)) = ((exp` A)^N)))
57	56	imbi2d 611	. . . 4 |- (j = N -> ((A e. CC -> (exp` (A x. j)) = ((exp