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 ‘ 𝐴 ) ↑ 𝑁 ) )