Metamath Proof Explorer

Theorem efexp

Description: The exponential of an integer power. Corollary 15-4.4 of Gleason p. 309, restricted to integers. (Contributed by NM, 13-Jan-2006) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Assertion efexp 
|- ( ( A e. CC /\ N e. ZZ ) -> ( exp ` ( N x. A ) ) = ( ( exp ` A ) ^ N ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( N e. ZZ -> N e. CC )
2 mulcom 
 |-  ( ( A e. CC /\ N e. CC ) -> ( A x. N ) = ( N x. A ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ N e. ZZ ) -> ( A x. N ) = ( N x. A ) )
4 3 fveq2d 
 |-  ( ( A e. CC /\ N e. ZZ ) -> ( exp ` ( A x. N ) ) = ( exp ` ( N x. A ) ) )
5 oveq2 
 |-  ( j = 0 -> ( A x. j ) = ( A x. 0 ) )
6 5 fveq2d 
 |-  ( j = 0 -> ( exp ` ( A x. j ) ) = ( exp ` ( A x. 0 ) ) )
7 oveq2 
 |-  ( j = 0 -> ( ( exp ` A ) ^ j ) = ( ( exp ` A ) ^ 0 ) )
8 6 7 eqeq12d 
 |-  ( j = 0 -> ( ( exp ` ( A x. j ) ) = ( ( exp ` A ) ^ j ) <-> ( exp ` ( A x. 0 ) ) = ( ( exp ` A ) ^ 0 ) ) )
9 oveq2 
 |-  ( j = k -> ( A x. j ) = ( A x. k ) )
10 9 fveq2d 
 |-  ( j = k -> ( exp ` ( A x. j ) ) = ( exp ` ( A x. k ) ) )
11 oveq2 
 |-  ( j = k -> ( ( exp ` A ) ^ j ) = ( ( exp ` A ) ^ k ) )
12 10 11 eqeq12d 
 |-  ( j = k -> ( ( exp ` ( A x. j ) ) = ( ( exp ` A ) ^ j ) <-> ( exp ` ( A x. k ) ) = ( ( exp ` A ) ^ k ) ) )
13 oveq2 
 |-  ( j = ( k + 1 ) -> ( A x. j ) = ( A x. ( k + 1 ) ) )
14 13 fveq2d 
 |-  ( j = ( k + 1 ) -> ( exp ` ( A x. j ) ) = ( exp ` ( A x. ( k + 1 ) ) ) )
15 oveq2 
 |-  ( j = ( k + 1 ) -> ( ( exp ` A ) ^ j ) = ( ( exp ` A ) ^ ( k + 1 ) ) )
16 14 15 eqeq12d 
 |-  ( j = ( k + 1 ) -> ( ( exp ` ( A x. j ) ) = ( ( exp ` A ) ^ j ) <-> ( exp ` ( A x. ( k + 1 ) ) ) = ( ( exp ` A ) ^ ( k + 1 ) ) ) )
17 oveq2 
 |-  ( j = -u k -> ( A x. j ) = ( A x. -u k ) )
18 17 fveq2d 
 |-  ( j = -u k -> ( exp ` ( A x. j ) ) = ( exp ` ( A x. -u k ) ) )
19 oveq2 
 |-  ( j = -u k -> ( ( exp ` A ) ^ j ) = ( ( exp ` A ) ^ -u k ) )
20 18 19 eqeq12d 
 |-  ( j = -u k -> ( ( exp ` ( A x. j ) ) = ( ( exp ` A ) ^ j ) <-> ( exp ` ( A x. -u k ) ) = ( ( exp ` A ) ^ -u k ) ) )
21 oveq2 
 |-  ( j = N -> ( A x. j ) = ( A x. N ) )
22 21 fveq2d 
 |-  ( j = N -> ( exp ` ( A x. j ) ) = ( exp ` ( A x. N ) ) )
23 oveq2 
 |-  ( j = N -> ( ( exp ` A ) ^ j ) = ( ( exp ` A ) ^ N ) )
24 22 23 eqeq12d 
 |-  ( j = N -> ( ( exp ` ( A x. j ) ) = ( ( exp ` A ) ^ j ) <-> ( exp ` ( A x. N ) ) = ( ( exp ` A ) ^ N ) ) )
25 ef0 
 |-  ( exp ` 0 ) = 1
26 mul01 
 |-  ( A e. CC -> ( A x. 0 ) = 0 )
27 26 fveq2d 
 |-  ( A e. CC -> ( exp ` ( A x. 0 ) ) = ( exp ` 0 ) )
28 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
29 28 exp0d 
 |-  ( A e. CC -> ( ( exp ` A ) ^ 0 ) = 1 )
30 25 27 29 3eqtr4a 
 |-  ( A e. CC -> ( exp ` ( A x. 0 ) ) = ( ( exp ` A ) ^ 0 ) )
31 oveq1 
 |-  ( ( exp ` ( A x. k ) ) = ( ( exp ` A ) ^ k ) -> ( ( exp ` ( A x. k ) ) x. ( exp ` A ) ) = ( ( ( exp ` A ) ^ k ) x. ( exp ` A ) ) )
32 31 adantl 
 |-  ( ( ( 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 ) ) )
33 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
34 ax-1cn 
 |-  1 e. CC
35 adddi 
 |-  ( ( A e. CC /\ k e. CC /\ 1 e. CC ) -> ( A x. ( k + 1 ) ) = ( ( A x. k ) + ( A x. 1 ) ) )
36 34 35 mp3an3 
 |-  ( ( A e. CC /\ k e. CC ) -> ( A x. ( k + 1 ) ) = ( ( A x. k ) + ( A x. 1 ) ) )
37 mulid1 
 |-  ( A e. CC -> ( A x. 1 ) = A )
38 37 adantr 
 |-  ( ( A e. CC /\ k e. CC ) -> ( A x. 1 ) = A )
39 38 oveq2d 
 |-  ( ( A e. CC /\ k e. CC ) -> ( ( A x. k ) + ( A x. 1 ) ) = ( ( A x. k ) + A ) )
40 36 39 eqtrd 
 |-  ( ( A e. CC /\ k e. CC ) -> ( A x. ( k + 1 ) ) = ( ( A x. k ) + A ) )
41 33 40 sylan2 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A x. ( k + 1 ) ) = ( ( A x. k ) + A ) )
42 41 fveq2d 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( exp ` ( A x. ( k + 1 ) ) ) = ( exp ` ( ( A x. k ) + A ) ) )
43 mulcl 
 |-  ( ( A e. CC /\ k e. CC ) -> ( A x. k ) e. CC )
44 33 43 sylan2 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A x. k ) e. CC )
45 simpl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> A e. CC )
46 efadd 
 |-  ( ( ( A x. k ) e. CC /\ A e. CC ) -> ( exp ` ( ( A x. k ) + A ) ) = ( ( exp ` ( A x. k ) ) x. ( exp ` A ) ) )
47 44 45 46 syl2anc 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( exp ` ( ( A x. k ) + A ) ) = ( ( exp ` ( A x. k ) ) x. ( exp ` A ) ) )
48 42 47 eqtrd 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( exp ` ( A x. ( k + 1 ) ) ) = ( ( exp ` ( A x. k ) ) x. ( exp ` A ) ) )
49 48 adantr 
 |-  ( ( ( 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 ) ) )
50 expp1 
 |-  ( ( ( exp ` A ) e. CC /\ k e. NN0 ) -> ( ( exp ` A ) ^ ( k + 1 ) ) = ( ( ( exp ` A ) ^ k ) x. ( exp ` A ) ) )
51 28 50 sylan 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( exp ` A ) ^ ( k + 1 ) ) = ( ( ( exp ` A ) ^ k ) x. ( exp ` A ) ) )
52 51 adantr 
 |-  ( ( ( A e. CC /\ k e. NN0 ) /\ ( exp ` ( A x. k ) ) = ( ( exp ` A ) ^ k ) ) -> ( ( exp ` A ) ^ ( k + 1 ) ) = ( ( ( exp ` A ) ^ k ) x. ( exp ` A ) ) )
53 32 49 52 3eqtr4d 
 |-  ( ( ( A e. CC /\ k e. NN0 ) /\ ( exp ` ( A x. k ) ) = ( ( exp ` A ) ^ k ) ) -> ( exp ` ( A x. ( k + 1 ) ) ) = ( ( exp ` A ) ^ ( k + 1 ) ) )
54 53 exp31 
 |-  ( A e. CC -> ( k e. NN0 -> ( ( exp ` ( A x. k ) ) = ( ( exp ` A ) ^ k ) -> ( exp ` ( A x. ( k + 1 ) ) ) = ( ( exp ` A ) ^ ( k + 1 ) ) ) ) )
55 oveq2 
 |-  ( ( exp ` ( A x. k ) ) = ( ( exp ` A ) ^ k ) -> ( 1 / ( exp ` ( A x. k ) ) ) = ( 1 / ( ( exp ` A ) ^ k ) ) )
56 nncn 
 |-  ( k e. NN -> k e. CC )
57 mulneg2 
 |-  ( ( A e. CC /\ k e. CC ) -> ( A x. -u k ) = -u ( A x. k ) )
58 56 57 sylan2 
 |-  ( ( A e. CC /\ k e. NN ) -> ( A x. -u k ) = -u ( A x. k ) )
59 58 fveq2d 
 |-  ( ( A e. CC /\ k e. NN ) -> ( exp ` ( A x. -u k ) ) = ( exp ` -u ( A x. k ) ) )
60 56 43 sylan2 
 |-  ( ( A e. CC /\ k e. NN ) -> ( A x. k ) e. CC )
61 efneg 
 |-  ( ( A x. k ) e. CC -> ( exp ` -u ( A x. k ) ) = ( 1 / ( exp ` ( A x. k ) ) ) )
62 60 61 syl 
 |-  ( ( A e. CC /\ k e. NN ) -> ( exp ` -u ( A x. k ) ) = ( 1 / ( exp ` ( A x. k ) ) ) )
63 59 62 eqtrd 
 |-  ( ( A e. CC /\ k e. NN ) -> ( exp ` ( A x. -u k ) ) = ( 1 / ( exp ` ( A x. k ) ) ) )
64 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
65 expneg 
 |-  ( ( ( exp ` A ) e. CC /\ k e. NN0 ) -> ( ( exp ` A ) ^ -u k ) = ( 1 / ( ( exp ` A ) ^ k ) ) )
66 28 64 65 syl2an 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( exp ` A ) ^ -u k ) = ( 1 / ( ( exp ` A ) ^ k ) ) )
67 63 66 eqeq12d 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( exp ` ( A x. -u k ) ) = ( ( exp ` A ) ^ -u k ) <-> ( 1 / ( exp ` ( A x. k ) ) ) = ( 1 / ( ( exp ` A ) ^ k ) ) ) )
68 55 67 syl5ibr 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( exp ` ( A x. k ) ) = ( ( exp ` A ) ^ k ) -> ( exp ` ( A x. -u k ) ) = ( ( exp ` A ) ^ -u k ) ) )
69 68 ex 
 |-  ( A e. CC -> ( k e. NN -> ( ( exp ` ( A x. k ) ) = ( ( exp ` A ) ^ k ) -> ( exp ` ( A x. -u k ) ) = ( ( exp ` A ) ^ -u k ) ) ) )
70 8 12 16 20 24 30 54 69 zindd 
 |-  ( A e. CC -> ( N e. ZZ -> ( exp ` ( A x. N ) ) = ( ( exp ` A ) ^ N ) ) )
71 70 imp 
 |-  ( ( A e. CC /\ N e. ZZ ) -> ( exp ` ( A x. N ) ) = ( ( exp ` A ) ^ N ) )
72 4 71 eqtr3d 
 |-  ( ( A e. CC /\ N e. ZZ ) -> ( exp ` ( N x. A ) ) = ( ( exp ` A ) ^ N ) )