Step | Hyp | Ref
| Expression |
1 | | zcn 9217 |
. . . 4
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
2 | | mulcom 7903 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝐴 · 𝑁) = (𝑁 · 𝐴)) |
3 | 1, 2 | sylan2 284 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (𝐴 · 𝑁) = (𝑁 · 𝐴)) |
4 | 3 | fveq2d 5500 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) →
(exp‘(𝐴 ·
𝑁)) = (exp‘(𝑁 · 𝐴))) |
5 | | oveq2 5861 |
. . . . . 6
⊢ (𝑗 = 0 → (𝐴 · 𝑗) = (𝐴 · 0)) |
6 | 5 | fveq2d 5500 |
. . . . 5
⊢ (𝑗 = 0 → (exp‘(𝐴 · 𝑗)) = (exp‘(𝐴 · 0))) |
7 | | oveq2 5861 |
. . . . 5
⊢ (𝑗 = 0 → ((exp‘𝐴)↑𝑗) = ((exp‘𝐴)↑0)) |
8 | 6, 7 | eqeq12d 2185 |
. . . 4
⊢ (𝑗 = 0 → ((exp‘(𝐴 · 𝑗)) = ((exp‘𝐴)↑𝑗) ↔ (exp‘(𝐴 · 0)) = ((exp‘𝐴)↑0))) |
9 | | oveq2 5861 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝐴 · 𝑗) = (𝐴 · 𝑘)) |
10 | 9 | fveq2d 5500 |
. . . . 5
⊢ (𝑗 = 𝑘 → (exp‘(𝐴 · 𝑗)) = (exp‘(𝐴 · 𝑘))) |
11 | | oveq2 5861 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((exp‘𝐴)↑𝑗) = ((exp‘𝐴)↑𝑘)) |
12 | 10, 11 | eqeq12d 2185 |
. . . 4
⊢ (𝑗 = 𝑘 → ((exp‘(𝐴 · 𝑗)) = ((exp‘𝐴)↑𝑗) ↔ (exp‘(𝐴 · 𝑘)) = ((exp‘𝐴)↑𝑘))) |
13 | | oveq2 5861 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝐴 · 𝑗) = (𝐴 · (𝑘 + 1))) |
14 | 13 | fveq2d 5500 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (exp‘(𝐴 · 𝑗)) = (exp‘(𝐴 · (𝑘 + 1)))) |
15 | | oveq2 5861 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((exp‘𝐴)↑𝑗) = ((exp‘𝐴)↑(𝑘 + 1))) |
16 | 14, 15 | eqeq12d 2185 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → ((exp‘(𝐴 · 𝑗)) = ((exp‘𝐴)↑𝑗) ↔ (exp‘(𝐴 · (𝑘 + 1))) = ((exp‘𝐴)↑(𝑘 + 1)))) |
17 | | oveq2 5861 |
. . . . . 6
⊢ (𝑗 = -𝑘 → (𝐴 · 𝑗) = (𝐴 · -𝑘)) |
18 | 17 | fveq2d 5500 |
. . . . 5
⊢ (𝑗 = -𝑘 → (exp‘(𝐴 · 𝑗)) = (exp‘(𝐴 · -𝑘))) |
19 | | oveq2 5861 |
. . . . 5
⊢ (𝑗 = -𝑘 → ((exp‘𝐴)↑𝑗) = ((exp‘𝐴)↑-𝑘)) |
20 | 18, 19 | eqeq12d 2185 |
. . . 4
⊢ (𝑗 = -𝑘 → ((exp‘(𝐴 · 𝑗)) = ((exp‘𝐴)↑𝑗) ↔ (exp‘(𝐴 · -𝑘)) = ((exp‘𝐴)↑-𝑘))) |
21 | | oveq2 5861 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝐴 · 𝑗) = (𝐴 · 𝑁)) |
22 | 21 | fveq2d 5500 |
. . . . 5
⊢ (𝑗 = 𝑁 → (exp‘(𝐴 · 𝑗)) = (exp‘(𝐴 · 𝑁))) |
23 | | oveq2 5861 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((exp‘𝐴)↑𝑗) = ((exp‘𝐴)↑𝑁)) |
24 | 22, 23 | eqeq12d 2185 |
. . . 4
⊢ (𝑗 = 𝑁 → ((exp‘(𝐴 · 𝑗)) = ((exp‘𝐴)↑𝑗) ↔ (exp‘(𝐴 · 𝑁)) = ((exp‘𝐴)↑𝑁))) |
25 | | ef0 11635 |
. . . . 5
⊢
(exp‘0) = 1 |
26 | | mul01 8308 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) =
0) |
27 | 26 | fveq2d 5500 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(exp‘(𝐴 · 0))
= (exp‘0)) |
28 | | efcl 11627 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘𝐴) ∈
ℂ) |
29 | 28 | exp0d 10603 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((exp‘𝐴)↑0) =
1) |
30 | 25, 27, 29 | 3eqtr4a 2229 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(exp‘(𝐴 · 0))
= ((exp‘𝐴)↑0)) |
31 | | oveq1 5860 |
. . . . . . 7
⊢
((exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘) → ((exp‘(𝐴 · 𝑘)) · (exp‘𝐴)) = (((exp‘𝐴)↑𝑘) · (exp‘𝐴))) |
32 | 31 | adantl 275 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘)) → ((exp‘(𝐴 · 𝑘)) · (exp‘𝐴)) = (((exp‘𝐴)↑𝑘) · (exp‘𝐴))) |
33 | | nn0cn 9145 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
34 | | ax-1cn 7867 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
35 | | adddi 7906 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 ·
(𝑘 + 1)) = ((𝐴 · 𝑘) + (𝐴 · 1))) |
36 | 34, 35 | mp3an3 1321 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · (𝑘 + 1)) = ((𝐴 · 𝑘) + (𝐴 · 1))) |
37 | | mulid1 7917 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) |
38 | 37 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · 1) = 𝐴) |
39 | 38 | oveq2d 5869 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝐴 · 𝑘) + (𝐴 · 1)) = ((𝐴 · 𝑘) + 𝐴)) |
40 | 36, 39 | eqtrd 2203 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · (𝑘 + 1)) = ((𝐴 · 𝑘) + 𝐴)) |
41 | 33, 40 | sylan2 284 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴 · (𝑘 + 1)) = ((𝐴 · 𝑘) + 𝐴)) |
42 | 41 | fveq2d 5500 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (exp‘(𝐴
· (𝑘 + 1))) =
(exp‘((𝐴 ·
𝑘) + 𝐴))) |
43 | | mulcl 7901 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · 𝑘) ∈ ℂ) |
44 | 33, 43 | sylan2 284 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴 · 𝑘) ∈
ℂ) |
45 | | simpl 108 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
46 | | efadd 11638 |
. . . . . . . . 9
⊢ (((𝐴 · 𝑘) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (exp‘((𝐴 · 𝑘) + 𝐴)) = ((exp‘(𝐴 · 𝑘)) · (exp‘𝐴))) |
47 | 44, 45, 46 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (exp‘((𝐴
· 𝑘) + 𝐴)) = ((exp‘(𝐴 · 𝑘)) · (exp‘𝐴))) |
48 | 42, 47 | eqtrd 2203 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (exp‘(𝐴
· (𝑘 + 1))) =
((exp‘(𝐴 ·
𝑘)) ·
(exp‘𝐴))) |
49 | 48 | adantr 274 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘)) → (exp‘(𝐴 · (𝑘 + 1))) = ((exp‘(𝐴 · 𝑘)) · (exp‘𝐴))) |
50 | | expp1 10483 |
. . . . . . . 8
⊢
(((exp‘𝐴)
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((exp‘𝐴)↑(𝑘 + 1)) = (((exp‘𝐴)↑𝑘) · (exp‘𝐴))) |
51 | 28, 50 | sylan 281 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((exp‘𝐴)↑(𝑘 + 1)) = (((exp‘𝐴)↑𝑘) · (exp‘𝐴))) |
52 | 51 | adantr 274 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘)) → ((exp‘𝐴)↑(𝑘 + 1)) = (((exp‘𝐴)↑𝑘) · (exp‘𝐴))) |
53 | 32, 49, 52 | 3eqtr4d 2213 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘)) → (exp‘(𝐴 · (𝑘 + 1))) = ((exp‘𝐴)↑(𝑘 + 1))) |
54 | 53 | exp31 362 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℕ0
→ ((exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘) → (exp‘(𝐴 · (𝑘 + 1))) = ((exp‘𝐴)↑(𝑘 + 1))))) |
55 | | oveq2 5861 |
. . . . . 6
⊢
((exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘) → (1 / (exp‘(𝐴 · 𝑘))) = (1 / ((exp‘𝐴)↑𝑘))) |
56 | | nncn 8886 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
57 | | mulneg2 8315 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · -𝑘) = -(𝐴 · 𝑘)) |
58 | 56, 57 | sylan2 284 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) → (𝐴 · -𝑘) = -(𝐴 · 𝑘)) |
59 | 58 | fveq2d 5500 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
(exp‘(𝐴 ·
-𝑘)) = (exp‘-(𝐴 · 𝑘))) |
60 | 56, 43 | sylan2 284 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) → (𝐴 · 𝑘) ∈ ℂ) |
61 | | efneg 11642 |
. . . . . . . . 9
⊢ ((𝐴 · 𝑘) ∈ ℂ → (exp‘-(𝐴 · 𝑘)) = (1 / (exp‘(𝐴 · 𝑘)))) |
62 | 60, 61 | syl 14 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
(exp‘-(𝐴 ·
𝑘)) = (1 /
(exp‘(𝐴 ·
𝑘)))) |
63 | 59, 62 | eqtrd 2203 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
(exp‘(𝐴 ·
-𝑘)) = (1 /
(exp‘(𝐴 ·
𝑘)))) |
64 | | efap0 11640 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(exp‘𝐴) #
0) |
65 | | nnnn0 9142 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
66 | | expnegap0 10484 |
. . . . . . . 8
⊢
(((exp‘𝐴)
∈ ℂ ∧ (exp‘𝐴) # 0 ∧ 𝑘 ∈ ℕ0) →
((exp‘𝐴)↑-𝑘) = (1 / ((exp‘𝐴)↑𝑘))) |
67 | 28, 64, 65, 66 | syl2an3an 1293 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
((exp‘𝐴)↑-𝑘) = (1 / ((exp‘𝐴)↑𝑘))) |
68 | 63, 67 | eqeq12d 2185 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
((exp‘(𝐴 ·
-𝑘)) = ((exp‘𝐴)↑-𝑘) ↔ (1 / (exp‘(𝐴 · 𝑘))) = (1 / ((exp‘𝐴)↑𝑘)))) |
69 | 55, 68 | syl5ibr 155 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
((exp‘(𝐴 ·
𝑘)) = ((exp‘𝐴)↑𝑘) → (exp‘(𝐴 · -𝑘)) = ((exp‘𝐴)↑-𝑘))) |
70 | 69 | ex 114 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℕ →
((exp‘(𝐴 ·
𝑘)) = ((exp‘𝐴)↑𝑘) → (exp‘(𝐴 · -𝑘)) = ((exp‘𝐴)↑-𝑘)))) |
71 | 8, 12, 16, 20, 24, 30, 54, 70 | zindd 9330 |
. . 3
⊢ (𝐴 ∈ ℂ → (𝑁 ∈ ℤ →
(exp‘(𝐴 ·
𝑁)) = ((exp‘𝐴)↑𝑁))) |
72 | 71 | imp 123 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) →
(exp‘(𝐴 ·
𝑁)) = ((exp‘𝐴)↑𝑁)) |
73 | 4, 72 | eqtr3d 2205 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) →
(exp‘(𝑁 ·
𝐴)) = ((exp‘𝐴)↑𝑁)) |