Step |
Hyp |
Ref |
Expression |
1 |
|
efcl |
⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ ) |
2 |
|
efne0 |
⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ≠ 0 ) |
3 |
1 2
|
logcld |
⊢ ( 𝐴 ∈ ℂ → ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ ) |
4 |
|
efsub |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ ) → ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) ) ) |
5 |
3 4
|
mpdan |
⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) ) ) |
6 |
|
eflog |
⊢ ( ( ( exp ‘ 𝐴 ) ∈ ℂ ∧ ( exp ‘ 𝐴 ) ≠ 0 ) → ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) = ( exp ‘ 𝐴 ) ) |
7 |
1 2 6
|
syl2anc |
⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) = ( exp ‘ 𝐴 ) ) |
8 |
7
|
oveq2d |
⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) / ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐴 ) ) ) |
9 |
1 2
|
dividd |
⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐴 ) ) = 1 ) |
10 |
5 8 9
|
3eqtrd |
⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 1 ) |
11 |
|
subcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ ) → ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ∈ ℂ ) |
12 |
3 11
|
mpdan |
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ∈ ℂ ) |
13 |
|
efeq1 |
⊢ ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ∈ ℂ → ( ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 1 ↔ ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) ) |
14 |
12 13
|
syl |
⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 1 ↔ ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) ) |
15 |
10 14
|
mpbid |
⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) |
16 |
|
ax-icn |
⊢ i ∈ ℂ |
17 |
|
2cn |
⊢ 2 ∈ ℂ |
18 |
|
picn |
⊢ π ∈ ℂ |
19 |
17 18
|
mulcli |
⊢ ( 2 · π ) ∈ ℂ |
20 |
16 19
|
mulcli |
⊢ ( i · ( 2 · π ) ) ∈ ℂ |
21 |
20
|
a1i |
⊢ ( 𝐴 ∈ ℂ → ( i · ( 2 · π ) ) ∈ ℂ ) |
22 |
|
ine0 |
⊢ i ≠ 0 |
23 |
|
2ne0 |
⊢ 2 ≠ 0 |
24 |
|
pire |
⊢ π ∈ ℝ |
25 |
|
pipos |
⊢ 0 < π |
26 |
24 25
|
gt0ne0ii |
⊢ π ≠ 0 |
27 |
17 18 23 26
|
mulne0i |
⊢ ( 2 · π ) ≠ 0 |
28 |
16 19 22 27
|
mulne0i |
⊢ ( i · ( 2 · π ) ) ≠ 0 |
29 |
28
|
a1i |
⊢ ( 𝐴 ∈ ℂ → ( i · ( 2 · π ) ) ≠ 0 ) |
30 |
12 21 29
|
divcan2d |
⊢ ( 𝐴 ∈ ℂ → ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) = ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) |
31 |
30
|
oveq2d |
⊢ ( 𝐴 ∈ ℂ → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) ) |
32 |
|
pncan3 |
⊢ ( ( ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 𝐴 ) |
33 |
3 32
|
mpancom |
⊢ ( 𝐴 ∈ ℂ → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 𝐴 ) |
34 |
31 33
|
eqtr2d |
⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) ) |
35 |
|
oveq2 |
⊢ ( 𝑛 = ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) → ( ( i · ( 2 · π ) ) · 𝑛 ) = ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) |
36 |
35
|
oveq2d |
⊢ ( 𝑛 = ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) ) |
37 |
36
|
rspceeqv |
⊢ ( ( ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ∧ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) ) → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) |
38 |
15 34 37
|
syl2anc |
⊢ ( 𝐴 ∈ ℂ → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) |
39 |
38
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) |
40 |
|
fveq2 |
⊢ ( ( exp ‘ 𝐴 ) = 𝐵 → ( log ‘ ( exp ‘ 𝐴 ) ) = ( log ‘ 𝐵 ) ) |
41 |
40
|
oveq1d |
⊢ ( ( exp ‘ 𝐴 ) = 𝐵 → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) |
42 |
41
|
eqeq2d |
⊢ ( ( exp ‘ 𝐴 ) = 𝐵 → ( 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) ) |
43 |
42
|
rexbidv |
⊢ ( ( exp ‘ 𝐴 ) = 𝐵 → ( ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) ) |
44 |
39 43
|
syl5ibcom |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( exp ‘ 𝐴 ) = 𝐵 → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) ) |
45 |
|
logcl |
⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ ) |
46 |
45
|
3adant1 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ ) |
47 |
|
zcn |
⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ ) |
48 |
47
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℂ ) |
49 |
|
mulcl |
⊢ ( ( ( i · ( 2 · π ) ) ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ ) |
50 |
20 48 49
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ ) |
51 |
|
efadd |
⊢ ( ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = ( ( exp ‘ ( log ‘ 𝐵 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) ) |
52 |
46 50 51
|
syl2an2r |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = ( ( exp ‘ ( log ‘ 𝐵 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) ) |
53 |
|
eflog |
⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 ) |
54 |
53
|
3adant1 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 ) |
55 |
|
ef2kpi |
⊢ ( 𝑛 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) = 1 ) |
56 |
54 55
|
oveqan12d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( ( exp ‘ ( log ‘ 𝐵 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = ( 𝐵 · 1 ) ) |
57 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → 𝐵 ∈ ℂ ) |
58 |
57
|
mulid1d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( 𝐵 · 1 ) = 𝐵 ) |
59 |
52 56 58
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = 𝐵 ) |
60 |
|
fveqeq2 |
⊢ ( 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) → ( ( exp ‘ 𝐴 ) = 𝐵 ↔ ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = 𝐵 ) ) |
61 |
59 60
|
syl5ibrcom |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) → ( exp ‘ 𝐴 ) = 𝐵 ) ) |
62 |
61
|
rexlimdva |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) → ( exp ‘ 𝐴 ) = 𝐵 ) ) |
63 |
44 62
|
impbid |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( exp ‘ 𝐴 ) = 𝐵 ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) ) |