HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem efexpt 7314
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
StepHypRef Expression
1 axmulcom 5248 . . . 4 |- ((A e. CC /\ N e. CC) -> (A x. N) = (N x. A))
2 nn0cnt 6056 . . . 4 |- (N e. NN0 -> N e. CC)
31, 2sylan2 451 . . 3 |- ((A e. CC /\ N e. NN0) -> (A x. N) = (N x. A))
43fveq2d 3713 . 2 |- ((A e. CC /\ N e. NN0) -> (exp` (A x. N)) = (exp` (N x. A)))
5 opreq1 3953 . . . . . . . . 9 |- ((exp` (A x. k)) = ((exp` A)^k) -> ((exp` (A x. k)) x. (exp` A)) = (((exp` A)^k) x. (exp` A)))
65adantl 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 5241 . . . . . . . . . . . . . 14 |- 1 e. CC
8 axdistr 5251 . . . . . . . . . . . . . 14 |- ((A e. CC /\ k e. CC /\ 1 e. CC) -> (A x. (k + 1)) = ((A x. k) + (A x. 1)))
97, 8mp3an3 902 . . . . . . . . . . . . 13 |- ((A e. CC /\ k e. CC) -> (A x. (k + 1)) = ((A x. k) + (A x. 1)))
10 ax1id 5254 . . . . . . . . . . . . . . 15 |- (A e. CC -> (A x. 1) = A)
1110adantr 389 . . . . . . . . . . . . . 14 |- ((A e. CC /\ k e. CC) -> (A x. 1) = A)
1211opreq2d 3961 . . . . . . . . . . . . 13 |- ((A e. CC /\ k e. CC) -> ((A x. k) + (A x. 1)) = ((A x. k) + A))
139, 12eqtrd 1499 . . . . . . . . . . . 12 |- ((A e. CC /\ k e. CC) -> (A x. (k + 1)) = ((A x. k) + A))
14 nn0cnt 6056 . . . . . . . . . . . 12 |- (k e. NN0 -> k e. CC)
1513, 14sylan2 451 . . . . . . . . . . 11 |- ((A e. CC /\ k e. NN0) -> (A x. (k + 1)) = ((A x. k) + A))
1615fveq2d 3713 . . . . . . . . . 10 |- ((A e. CC /\ k e. NN0) -> (exp` (A x. (k + 1))) = (exp` ((A x. k) + A)))
17 efaddt 7309 . . . . . . . . . . 11 |- (((A x. k) e. CC /\ A e. CC) -> (exp` ((A x. k) + A)) = ((exp` (A x. k)) x. (exp` A)))
18 axmulcl 5245 . . . . . . . . . . . 12 |- ((A e. CC /\ k e. CC) -> (A x. k) e. CC)
1918, 14sylan2 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)
2117, 19, 20sylanc 471 . . . . . . . . . 10 |- ((A e. CC /\ k e. NN0) -> (exp` ((A x. k) + A)) = ((exp` (A x. k)) x. (exp` A)))
2216, 21eqtrd 1499 . . . . . . . . 9 |- ((A e. CC /\ k e. NN0) -> (exp` (A x. (k + 1))) = ((exp` (A x. k)) x. (exp` A)))
2322adantr 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 6506 . . . . . . . . . 10 |- (((exp` A) e. CC /\ k e. NN0) -> ((exp` A)^(k + 1)) = (((exp` A)^k) x. (exp` A)))
25 efclt 7254 . . . . . . . . . 10 |- (A e. CC -> (exp` A) e. CC)
2624, 25sylan 448 . . . . . . . . 9 |- ((A e. CC /\ k e. NN0) -> ((exp` A)^(k + 1)) = (((exp` A)^k) x. (exp` A)))
2726adantr 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)))
286, 23, 273eqtr4d 1509 . . . . . . 7 |- (((A e. CC /\ k e. NN0) /\ (exp` (A x. k)) = ((exp` A)^k)) -> (exp` (A x. (k + 1))) = ((exp` A)^(k + 1)))
2928ex 373 . . . . . 6 |- ((A e. CC /\ k e. NN0) -> ((exp` (A x. k)) = ((exp` A)^k) -> (exp` (A x. (k + 1))) = ((exp` A)^(k + 1))))
3029expcom 374 . . . . 5 |- (k e. NN0 -> (A e. CC -> ((exp` (A x. k)) = ((exp` A)^k) -> (exp` (A x. (k + 1))) = ((exp` A)^(k + 1)))))
3130a2d 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 7277 . . . . 5 |- (exp` 0) = 1
33 mul01t 5415 . . . . . 6 |- (A e. CC -> (A x. 0) = 0)
3433fveq2d 3713 . . . . 5 |- (A e. CC -> (exp` (A x. 0)) = (exp` 0))
35 exp0t 6503 . . . . . 6 |- ((exp` A) e. CC -> ((exp` A)^0) = 1)
3625, 35syl 10 . . . . 5 |- (A e. CC -> ((exp` A)^0) = 1)
3732, 34, 363eqtr4a 1524 . . . 4 |- (A e. CC -> (exp` (A x. 0)) = ((exp` A)^0))
38 opreq2 3954 . . . . . . 7 |- (j = 0 -> (A x. j) = (A x. 0))
3938fveq2d 3713 . . . . . 6 |- (j = 0 -> (exp` (A x. j)) = (exp` (A x. 0)))
40 opreq2 3954 . . . . . 6 |- (j = 0 -> ((exp` A)^j) = ((exp` A)^0))
4139, 40eqeq12d 1481 . . . . 5 |- (j = 0 -> ((exp` (A x. j)) = ((exp` A)^j) <-> (exp` (A x. 0)) = ((exp` A)^0)))
4241imbi2d 610 . . . 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 3954 . . . . . . 7 |- (j = k -> (A x. j) = (A x. k))
4443fveq2d 3713 . . . . . 6 |- (j = k -> (exp` (A x. j)) = (exp` (A x. k)))
45 opreq2 3954 . . . . . 6 |- (j = k -> ((exp` A)^j) = ((exp` A)^k))
4644, 45eqeq12d 1481 . . . . 5 |- (j = k -> ((exp` (A x. j)) = ((exp` A)^j) <-> (exp` (A x. k)) = ((exp` A)^k)))
4746imbi2d 610 . . . 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 3954 . . . . . . 7 |- (j = (k + 1) -> (A x. j) = (A x. (k + 1)))
4948fveq2d 3713 . . . . . 6 |- (j = (k + 1) -> (exp` (A x. j)) = (exp` (A x. (k + 1))))
50 opreq2 3954 . . . . . 6 |- (j = (k + 1) -> ((exp` A)^j) = ((exp` A)^(k + 1)))
5149, 50eqeq12d 1481 . . . . 5 |- (j = (k + 1) -> ((exp` (A x. j)) = ((exp` A)^j) <-> (exp` (A x. (k + 1))) = ((exp` A)^(k + 1))))
5251imbi2d 610 . . . 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 3954 . . . . . . 7 |- (j = N -> (A x. j) = (A x. N))
5453fveq2d 3713 . . . . . 6 |- (j = N -> (exp` (A x. j)) = (exp` (A x. N)))
55 opreq2 3954 . . . . . 6 |- (j = N -> ((exp` A)^j) = ((exp` A)^N))
5654, 55eqeq12d 1481 . . . . 5 |- (j = N -> ((exp` (A x. j)) = ((exp` A)^j) <-> (exp` (A x. N)) = ((exp` A)^N)))
5756imbi2d 610 . . . 4 |- (j = N -> ((A e. CC -> (exp` (A x. j)) = ((exp