Proof of Theorem eflogeq
Step | Hyp | Ref
| Expression |
1 | | efcl 14813 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(exp‘𝐴) ∈
ℂ) |
2 | | efne0 14827 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(exp‘𝐴) ≠
0) |
3 | 1, 2 | logcld 24317 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(log‘(exp‘𝐴))
∈ ℂ) |
4 | | efsub 14830 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(log‘(exp‘𝐴))
∈ ℂ) → (exp‘(𝐴 − (log‘(exp‘𝐴)))) = ((exp‘𝐴) /
(exp‘(log‘(exp‘𝐴))))) |
5 | 3, 4 | mpdan 702 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(exp‘(𝐴 −
(log‘(exp‘𝐴))))
= ((exp‘𝐴) /
(exp‘(log‘(exp‘𝐴))))) |
6 | | eflog 24323 |
. . . . . . . . 9
⊢
(((exp‘𝐴)
∈ ℂ ∧ (exp‘𝐴) ≠ 0) →
(exp‘(log‘(exp‘𝐴))) = (exp‘𝐴)) |
7 | 1, 2, 6 | syl2anc 693 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(exp‘(log‘(exp‘𝐴))) = (exp‘𝐴)) |
8 | 7 | oveq2d 6666 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((exp‘𝐴) /
(exp‘(log‘(exp‘𝐴)))) = ((exp‘𝐴) / (exp‘𝐴))) |
9 | 1, 2 | dividd 10799 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
((exp‘𝐴) /
(exp‘𝐴)) =
1) |
10 | 5, 8, 9 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘(𝐴 −
(log‘(exp‘𝐴))))
= 1) |
11 | | subcl 10280 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(log‘(exp‘𝐴))
∈ ℂ) → (𝐴
− (log‘(exp‘𝐴))) ∈ ℂ) |
12 | 3, 11 | mpdan 702 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐴 −
(log‘(exp‘𝐴)))
∈ ℂ) |
13 | | efeq1 24275 |
. . . . . . 7
⊢ ((𝐴 −
(log‘(exp‘𝐴)))
∈ ℂ → ((exp‘(𝐴 − (log‘(exp‘𝐴)))) = 1 ↔ ((𝐴 −
(log‘(exp‘𝐴)))
/ (i · (2 · π))) ∈ ℤ)) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((exp‘(𝐴 −
(log‘(exp‘𝐴))))
= 1 ↔ ((𝐴 −
(log‘(exp‘𝐴)))
/ (i · (2 · π))) ∈ ℤ)) |
15 | 10, 14 | mpbid 222 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝐴 −
(log‘(exp‘𝐴)))
/ (i · (2 · π))) ∈ ℤ) |
16 | | ax-icn 9995 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
17 | | 2cn 11091 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
18 | | picn 24211 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
19 | 17, 18 | mulcli 10045 |
. . . . . . . . . 10
⊢ (2
· π) ∈ ℂ |
20 | 16, 19 | mulcli 10045 |
. . . . . . . . 9
⊢ (i
· (2 · π)) ∈ ℂ |
21 | 20 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· (2 · π)) ∈ ℂ) |
22 | | ine0 10465 |
. . . . . . . . . 10
⊢ i ≠
0 |
23 | | 2ne0 11113 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
24 | | pire 24210 |
. . . . . . . . . . . 12
⊢ π
∈ ℝ |
25 | | pipos 24212 |
. . . . . . . . . . . 12
⊢ 0 <
π |
26 | 24, 25 | gt0ne0ii 10564 |
. . . . . . . . . . 11
⊢ π ≠
0 |
27 | 17, 18, 23, 26 | mulne0i 10670 |
. . . . . . . . . 10
⊢ (2
· π) ≠ 0 |
28 | 16, 19, 22, 27 | mulne0i 10670 |
. . . . . . . . 9
⊢ (i
· (2 · π)) ≠ 0 |
29 | 28 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (i
· (2 · π)) ≠ 0) |
30 | 12, 21, 29 | divcan2d 10803 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → ((i
· (2 · π)) · ((𝐴 − (log‘(exp‘𝐴))) / (i · (2 ·
π)))) = (𝐴 −
(log‘(exp‘𝐴)))) |
31 | 30 | oveq2d 6666 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((log‘(exp‘𝐴))
+ ((i · (2 · π)) · ((𝐴 − (log‘(exp‘𝐴))) / (i · (2 ·
π))))) = ((log‘(exp‘𝐴)) + (𝐴 − (log‘(exp‘𝐴))))) |
32 | | pncan3 10289 |
. . . . . . 7
⊢
(((log‘(exp‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ ℂ) →
((log‘(exp‘𝐴))
+ (𝐴 −
(log‘(exp‘𝐴))))
= 𝐴) |
33 | 3, 32 | mpancom 703 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
((log‘(exp‘𝐴))
+ (𝐴 −
(log‘(exp‘𝐴))))
= 𝐴) |
34 | 31, 33 | eqtr2d 2657 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 𝐴 = ((log‘(exp‘𝐴)) + ((i · (2 ·
π)) · ((𝐴 −
(log‘(exp‘𝐴)))
/ (i · (2 · π)))))) |
35 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑛 = ((𝐴 − (log‘(exp‘𝐴))) / (i · (2 ·
π))) → ((i · (2 · π)) · 𝑛) = ((i · (2 · π)) ·
((𝐴 −
(log‘(exp‘𝐴)))
/ (i · (2 · π))))) |
36 | 35 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑛 = ((𝐴 − (log‘(exp‘𝐴))) / (i · (2 ·
π))) → ((log‘(exp‘𝐴)) + ((i · (2 · π))
· 𝑛)) =
((log‘(exp‘𝐴))
+ ((i · (2 · π)) · ((𝐴 − (log‘(exp‘𝐴))) / (i · (2 ·
π)))))) |
37 | 36 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑛 = ((𝐴 − (log‘(exp‘𝐴))) / (i · (2 ·
π))) → (𝐴 =
((log‘(exp‘𝐴))
+ ((i · (2 · π)) · 𝑛)) ↔ 𝐴 = ((log‘(exp‘𝐴)) + ((i · (2 · π))
· ((𝐴 −
(log‘(exp‘𝐴)))
/ (i · (2 · π))))))) |
38 | 37 | rspcev 3309 |
. . . . 5
⊢ ((((𝐴 −
(log‘(exp‘𝐴)))
/ (i · (2 · π))) ∈ ℤ ∧ 𝐴 = ((log‘(exp‘𝐴)) + ((i · (2 · π))
· ((𝐴 −
(log‘(exp‘𝐴)))
/ (i · (2 · π)))))) → ∃𝑛 ∈ ℤ 𝐴 = ((log‘(exp‘𝐴)) + ((i · (2 · π))
· 𝑛))) |
39 | 15, 34, 38 | syl2anc 693 |
. . . 4
⊢ (𝐴 ∈ ℂ →
∃𝑛 ∈ ℤ
𝐴 =
((log‘(exp‘𝐴))
+ ((i · (2 · π)) · 𝑛))) |
40 | 39 | 3ad2ant1 1082 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ∃𝑛 ∈ ℤ 𝐴 = ((log‘(exp‘𝐴)) + ((i · (2 ·
π)) · 𝑛))) |
41 | | fveq2 6191 |
. . . . . 6
⊢
((exp‘𝐴) =
𝐵 →
(log‘(exp‘𝐴)) =
(log‘𝐵)) |
42 | 41 | oveq1d 6665 |
. . . . 5
⊢
((exp‘𝐴) =
𝐵 →
((log‘(exp‘𝐴))
+ ((i · (2 · π)) · 𝑛)) = ((log‘𝐵) + ((i · (2 · π)) ·
𝑛))) |
43 | 42 | eqeq2d 2632 |
. . . 4
⊢
((exp‘𝐴) =
𝐵 → (𝐴 = ((log‘(exp‘𝐴)) + ((i · (2 · π))
· 𝑛)) ↔ 𝐴 = ((log‘𝐵) + ((i · (2 · π)) ·
𝑛)))) |
44 | 43 | rexbidv 3052 |
. . 3
⊢
((exp‘𝐴) =
𝐵 → (∃𝑛 ∈ ℤ 𝐴 = ((log‘(exp‘𝐴)) + ((i · (2 ·
π)) · 𝑛)) ↔
∃𝑛 ∈ ℤ
𝐴 = ((log‘𝐵) + ((i · (2 ·
π)) · 𝑛)))) |
45 | 40, 44 | syl5ibcom 235 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) →
((exp‘𝐴) = 𝐵 → ∃𝑛 ∈ ℤ 𝐴 = ((log‘𝐵) + ((i · (2 · π)) ·
𝑛)))) |
46 | | logcl 24315 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (log‘𝐵) ∈
ℂ) |
47 | 46 | 3adant1 1079 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (log‘𝐵) ∈
ℂ) |
48 | 47 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑛 ∈ ℤ) →
(log‘𝐵) ∈
ℂ) |
49 | | zcn 11382 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
50 | 49 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈
ℂ) |
51 | | mulcl 10020 |
. . . . . . 7
⊢ (((i
· (2 · π)) ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((i · (2
· π)) · 𝑛)
∈ ℂ) |
52 | 20, 50, 51 | sylancr 695 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑛 ∈ ℤ) → ((i
· (2 · π)) · 𝑛) ∈ ℂ) |
53 | | efadd 14824 |
. . . . . 6
⊢
(((log‘𝐵)
∈ ℂ ∧ ((i · (2 · π)) · 𝑛) ∈ ℂ) →
(exp‘((log‘𝐵) +
((i · (2 · π)) · 𝑛))) = ((exp‘(log‘𝐵)) · (exp‘((i
· (2 · π)) · 𝑛)))) |
54 | 48, 52, 53 | syl2anc 693 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑛 ∈ ℤ) →
(exp‘((log‘𝐵) +
((i · (2 · π)) · 𝑛))) = ((exp‘(log‘𝐵)) · (exp‘((i
· (2 · π)) · 𝑛)))) |
55 | | eflog 24323 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) →
(exp‘(log‘𝐵)) =
𝐵) |
56 | 55 | 3adant1 1079 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) →
(exp‘(log‘𝐵)) =
𝐵) |
57 | | ef2kpi 24230 |
. . . . . 6
⊢ (𝑛 ∈ ℤ →
(exp‘((i · (2 · π)) · 𝑛)) = 1) |
58 | 56, 57 | oveqan12d 6669 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑛 ∈ ℤ) →
((exp‘(log‘𝐵))
· (exp‘((i · (2 · π)) · 𝑛))) = (𝐵 · 1)) |
59 | | simpl2 1065 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑛 ∈ ℤ) → 𝐵 ∈
ℂ) |
60 | 59 | mulid1d 10057 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑛 ∈ ℤ) → (𝐵 · 1) = 𝐵) |
61 | 54, 58, 60 | 3eqtrd 2660 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑛 ∈ ℤ) →
(exp‘((log‘𝐵) +
((i · (2 · π)) · 𝑛))) = 𝐵) |
62 | | fveq2 6191 |
. . . . 5
⊢ (𝐴 = ((log‘𝐵) + ((i · (2 · π)) ·
𝑛)) → (exp‘𝐴) = (exp‘((log‘𝐵) + ((i · (2 ·
π)) · 𝑛)))) |
63 | 62 | eqeq1d 2624 |
. . . 4
⊢ (𝐴 = ((log‘𝐵) + ((i · (2 · π)) ·
𝑛)) →
((exp‘𝐴) = 𝐵 ↔
(exp‘((log‘𝐵) +
((i · (2 · π)) · 𝑛))) = 𝐵)) |
64 | 61, 63 | syl5ibrcom 237 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑛 ∈ ℤ) → (𝐴 = ((log‘𝐵) + ((i · (2 · π)) ·
𝑛)) → (exp‘𝐴) = 𝐵)) |
65 | 64 | rexlimdva 3031 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (∃𝑛 ∈ ℤ 𝐴 = ((log‘𝐵) + ((i · (2 · π)) ·
𝑛)) → (exp‘𝐴) = 𝐵)) |
66 | 45, 65 | impbid 202 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) →
((exp‘𝐴) = 𝐵 ↔ ∃𝑛 ∈ ℤ 𝐴 = ((log‘𝐵) + ((i · (2 · π)) ·
𝑛)))) |