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 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( exp ‘ ( 𝑁 · 𝐴 ) ) = ( ( exp ‘ 𝐴 ) ↑ 𝑁 ) )

Proof

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