# 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 ${⊢}\left({A}\in ℂ\wedge {N}\in ℤ\right)\to {\mathrm{e}}^{{N}{A}}={{\mathrm{e}}^{{A}}}^{{N}}$

### Proof

Step Hyp Ref Expression
1 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
2 mulcom ${⊢}\left({A}\in ℂ\wedge {N}\in ℂ\right)\to {A}\cdot {N}={N}{A}$
3 1 2 sylan2 ${⊢}\left({A}\in ℂ\wedge {N}\in ℤ\right)\to {A}\cdot {N}={N}{A}$
4 3 fveq2d ${⊢}\left({A}\in ℂ\wedge {N}\in ℤ\right)\to {\mathrm{e}}^{{A}\cdot {N}}={\mathrm{e}}^{{N}{A}}$
5 oveq2 ${⊢}{j}=0\to {A}{j}={A}\cdot 0$
6 5 fveq2d ${⊢}{j}=0\to {\mathrm{e}}^{{A}{j}}={\mathrm{e}}^{{A}\cdot 0}$
7 oveq2 ${⊢}{j}=0\to {{\mathrm{e}}^{{A}}}^{{j}}={{\mathrm{e}}^{{A}}}^{0}$
8 6 7 eqeq12d ${⊢}{j}=0\to \left({\mathrm{e}}^{{A}{j}}={{\mathrm{e}}^{{A}}}^{{j}}↔{\mathrm{e}}^{{A}\cdot 0}={{\mathrm{e}}^{{A}}}^{0}\right)$
9 oveq2 ${⊢}{j}={k}\to {A}{j}={A}{k}$
10 9 fveq2d ${⊢}{j}={k}\to {\mathrm{e}}^{{A}{j}}={\mathrm{e}}^{{A}{k}}$
11 oveq2 ${⊢}{j}={k}\to {{\mathrm{e}}^{{A}}}^{{j}}={{\mathrm{e}}^{{A}}}^{{k}}$
12 10 11 eqeq12d ${⊢}{j}={k}\to \left({\mathrm{e}}^{{A}{j}}={{\mathrm{e}}^{{A}}}^{{j}}↔{\mathrm{e}}^{{A}{k}}={{\mathrm{e}}^{{A}}}^{{k}}\right)$
13 oveq2 ${⊢}{j}={k}+1\to {A}{j}={A}\left({k}+1\right)$
14 13 fveq2d ${⊢}{j}={k}+1\to {\mathrm{e}}^{{A}{j}}={\mathrm{e}}^{{A}\left({k}+1\right)}$
15 oveq2 ${⊢}{j}={k}+1\to {{\mathrm{e}}^{{A}}}^{{j}}={{\mathrm{e}}^{{A}}}^{{k}+1}$
16 14 15 eqeq12d ${⊢}{j}={k}+1\to \left({\mathrm{e}}^{{A}{j}}={{\mathrm{e}}^{{A}}}^{{j}}↔{\mathrm{e}}^{{A}\left({k}+1\right)}={{\mathrm{e}}^{{A}}}^{{k}+1}\right)$
17 oveq2 ${⊢}{j}=-{k}\to {A}{j}={A}\left(-{k}\right)$
18 17 fveq2d ${⊢}{j}=-{k}\to {\mathrm{e}}^{{A}{j}}={\mathrm{e}}^{{A}\left(-{k}\right)}$
19 oveq2 ${⊢}{j}=-{k}\to {{\mathrm{e}}^{{A}}}^{{j}}={{\mathrm{e}}^{{A}}}^{-{k}}$
20 18 19 eqeq12d ${⊢}{j}=-{k}\to \left({\mathrm{e}}^{{A}{j}}={{\mathrm{e}}^{{A}}}^{{j}}↔{\mathrm{e}}^{{A}\left(-{k}\right)}={{\mathrm{e}}^{{A}}}^{-{k}}\right)$
21 oveq2 ${⊢}{j}={N}\to {A}{j}={A}\cdot {N}$
22 21 fveq2d ${⊢}{j}={N}\to {\mathrm{e}}^{{A}{j}}={\mathrm{e}}^{{A}\cdot {N}}$
23 oveq2 ${⊢}{j}={N}\to {{\mathrm{e}}^{{A}}}^{{j}}={{\mathrm{e}}^{{A}}}^{{N}}$
24 22 23 eqeq12d ${⊢}{j}={N}\to \left({\mathrm{e}}^{{A}{j}}={{\mathrm{e}}^{{A}}}^{{j}}↔{\mathrm{e}}^{{A}\cdot {N}}={{\mathrm{e}}^{{A}}}^{{N}}\right)$
25 ef0 ${⊢}{\mathrm{e}}^{0}=1$
26 mul01 ${⊢}{A}\in ℂ\to {A}\cdot 0=0$
27 26 fveq2d ${⊢}{A}\in ℂ\to {\mathrm{e}}^{{A}\cdot 0}={\mathrm{e}}^{0}$
28 efcl ${⊢}{A}\in ℂ\to {\mathrm{e}}^{{A}}\in ℂ$
29 28 exp0d ${⊢}{A}\in ℂ\to {{\mathrm{e}}^{{A}}}^{0}=1$
30 25 27 29 3eqtr4a ${⊢}{A}\in ℂ\to {\mathrm{e}}^{{A}\cdot 0}={{\mathrm{e}}^{{A}}}^{0}$
31 oveq1 ${⊢}{\mathrm{e}}^{{A}{k}}={{\mathrm{e}}^{{A}}}^{{k}}\to {\mathrm{e}}^{{A}{k}}{\mathrm{e}}^{{A}}={{\mathrm{e}}^{{A}}}^{{k}}{\mathrm{e}}^{{A}}$
32 31 adantl ${⊢}\left(\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\wedge {\mathrm{e}}^{{A}{k}}={{\mathrm{e}}^{{A}}}^{{k}}\right)\to {\mathrm{e}}^{{A}{k}}{\mathrm{e}}^{{A}}={{\mathrm{e}}^{{A}}}^{{k}}{\mathrm{e}}^{{A}}$
33 nn0cn ${⊢}{k}\in {ℕ}_{0}\to {k}\in ℂ$
34 ax-1cn ${⊢}1\in ℂ$
35 adddi ${⊢}\left({A}\in ℂ\wedge {k}\in ℂ\wedge 1\in ℂ\right)\to {A}\left({k}+1\right)={A}{k}+{A}\cdot 1$
36 34 35 mp3an3 ${⊢}\left({A}\in ℂ\wedge {k}\in ℂ\right)\to {A}\left({k}+1\right)={A}{k}+{A}\cdot 1$
37 mulid1 ${⊢}{A}\in ℂ\to {A}\cdot 1={A}$
38 37 adantr ${⊢}\left({A}\in ℂ\wedge {k}\in ℂ\right)\to {A}\cdot 1={A}$
39 38 oveq2d ${⊢}\left({A}\in ℂ\wedge {k}\in ℂ\right)\to {A}{k}+{A}\cdot 1={A}{k}+{A}$
40 36 39 eqtrd ${⊢}\left({A}\in ℂ\wedge {k}\in ℂ\right)\to {A}\left({k}+1\right)={A}{k}+{A}$
41 33 40 sylan2 ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {A}\left({k}+1\right)={A}{k}+{A}$
42 41 fveq2d ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{e}}^{{A}\left({k}+1\right)}={\mathrm{e}}^{{A}{k}+{A}}$
43 mulcl ${⊢}\left({A}\in ℂ\wedge {k}\in ℂ\right)\to {A}{k}\in ℂ$
44 33 43 sylan2 ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {A}{k}\in ℂ$
45 simpl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {A}\in ℂ$
46 efadd ${⊢}\left({A}{k}\in ℂ\wedge {A}\in ℂ\right)\to {\mathrm{e}}^{{A}{k}+{A}}={\mathrm{e}}^{{A}{k}}{\mathrm{e}}^{{A}}$
47 44 45 46 syl2anc ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{e}}^{{A}{k}+{A}}={\mathrm{e}}^{{A}{k}}{\mathrm{e}}^{{A}}$
48 42 47 eqtrd ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{e}}^{{A}\left({k}+1\right)}={\mathrm{e}}^{{A}{k}}{\mathrm{e}}^{{A}}$
49 48 adantr ${⊢}\left(\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\wedge {\mathrm{e}}^{{A}{k}}={{\mathrm{e}}^{{A}}}^{{k}}\right)\to {\mathrm{e}}^{{A}\left({k}+1\right)}={\mathrm{e}}^{{A}{k}}{\mathrm{e}}^{{A}}$
50 expp1 ${⊢}\left({\mathrm{e}}^{{A}}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{\mathrm{e}}^{{A}}}^{{k}+1}={{\mathrm{e}}^{{A}}}^{{k}}{\mathrm{e}}^{{A}}$
51 28 50 sylan ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{\mathrm{e}}^{{A}}}^{{k}+1}={{\mathrm{e}}^{{A}}}^{{k}}{\mathrm{e}}^{{A}}$
52 51 adantr ${⊢}\left(\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\wedge {\mathrm{e}}^{{A}{k}}={{\mathrm{e}}^{{A}}}^{{k}}\right)\to {{\mathrm{e}}^{{A}}}^{{k}+1}={{\mathrm{e}}^{{A}}}^{{k}}{\mathrm{e}}^{{A}}$
53 32 49 52 3eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\wedge {\mathrm{e}}^{{A}{k}}={{\mathrm{e}}^{{A}}}^{{k}}\right)\to {\mathrm{e}}^{{A}\left({k}+1\right)}={{\mathrm{e}}^{{A}}}^{{k}+1}$
54 53 exp31 ${⊢}{A}\in ℂ\to \left({k}\in {ℕ}_{0}\to \left({\mathrm{e}}^{{A}{k}}={{\mathrm{e}}^{{A}}}^{{k}}\to {\mathrm{e}}^{{A}\left({k}+1\right)}={{\mathrm{e}}^{{A}}}^{{k}+1}\right)\right)$
55 oveq2 ${⊢}{\mathrm{e}}^{{A}{k}}={{\mathrm{e}}^{{A}}}^{{k}}\to \frac{1}{{\mathrm{e}}^{{A}{k}}}=\frac{1}{{{\mathrm{e}}^{{A}}}^{{k}}}$
56 nncn ${⊢}{k}\in ℕ\to {k}\in ℂ$
57 mulneg2 ${⊢}\left({A}\in ℂ\wedge {k}\in ℂ\right)\to {A}\left(-{k}\right)=-{A}{k}$
58 56 57 sylan2 ${⊢}\left({A}\in ℂ\wedge {k}\in ℕ\right)\to {A}\left(-{k}\right)=-{A}{k}$
59 58 fveq2d ${⊢}\left({A}\in ℂ\wedge {k}\in ℕ\right)\to {\mathrm{e}}^{{A}\left(-{k}\right)}={\mathrm{e}}^{-{A}{k}}$
60 56 43 sylan2 ${⊢}\left({A}\in ℂ\wedge {k}\in ℕ\right)\to {A}{k}\in ℂ$
61 efneg ${⊢}{A}{k}\in ℂ\to {\mathrm{e}}^{-{A}{k}}=\frac{1}{{\mathrm{e}}^{{A}{k}}}$
62 60 61 syl ${⊢}\left({A}\in ℂ\wedge {k}\in ℕ\right)\to {\mathrm{e}}^{-{A}{k}}=\frac{1}{{\mathrm{e}}^{{A}{k}}}$
63 59 62 eqtrd ${⊢}\left({A}\in ℂ\wedge {k}\in ℕ\right)\to {\mathrm{e}}^{{A}\left(-{k}\right)}=\frac{1}{{\mathrm{e}}^{{A}{k}}}$
64 nnnn0 ${⊢}{k}\in ℕ\to {k}\in {ℕ}_{0}$
65 expneg ${⊢}\left({\mathrm{e}}^{{A}}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{\mathrm{e}}^{{A}}}^{-{k}}=\frac{1}{{{\mathrm{e}}^{{A}}}^{{k}}}$
66 28 64 65 syl2an ${⊢}\left({A}\in ℂ\wedge {k}\in ℕ\right)\to {{\mathrm{e}}^{{A}}}^{-{k}}=\frac{1}{{{\mathrm{e}}^{{A}}}^{{k}}}$
67 63 66 eqeq12d ${⊢}\left({A}\in ℂ\wedge {k}\in ℕ\right)\to \left({\mathrm{e}}^{{A}\left(-{k}\right)}={{\mathrm{e}}^{{A}}}^{-{k}}↔\frac{1}{{\mathrm{e}}^{{A}{k}}}=\frac{1}{{{\mathrm{e}}^{{A}}}^{{k}}}\right)$
68 55 67 syl5ibr ${⊢}\left({A}\in ℂ\wedge {k}\in ℕ\right)\to \left({\mathrm{e}}^{{A}{k}}={{\mathrm{e}}^{{A}}}^{{k}}\to {\mathrm{e}}^{{A}\left(-{k}\right)}={{\mathrm{e}}^{{A}}}^{-{k}}\right)$
69 68 ex ${⊢}{A}\in ℂ\to \left({k}\in ℕ\to \left({\mathrm{e}}^{{A}{k}}={{\mathrm{e}}^{{A}}}^{{k}}\to {\mathrm{e}}^{{A}\left(-{k}\right)}={{\mathrm{e}}^{{A}}}^{-{k}}\right)\right)$
70 8 12 16 20 24 30 54 69 zindd ${⊢}{A}\in ℂ\to \left({N}\in ℤ\to {\mathrm{e}}^{{A}\cdot {N}}={{\mathrm{e}}^{{A}}}^{{N}}\right)$
71 70 imp ${⊢}\left({A}\in ℂ\wedge {N}\in ℤ\right)\to {\mathrm{e}}^{{A}\cdot {N}}={{\mathrm{e}}^{{A}}}^{{N}}$
72 4 71 eqtr3d ${⊢}\left({A}\in ℂ\wedge {N}\in ℤ\right)\to {\mathrm{e}}^{{N}{A}}={{\mathrm{e}}^{{A}}}^{{N}}$