# 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 ) ) )`
` |-  ( ( ( 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`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) )`