Step |
Hyp |
Ref |
Expression |
1 |
|
ef11d.a |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
2 |
|
ef11d.b |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
3 |
1 2
|
efsubd |
⊢ ( 𝜑 → ( exp ‘ ( 𝐴 − 𝐵 ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) ) |
4 |
3
|
eqeq1d |
⊢ ( 𝜑 → ( ( exp ‘ ( 𝐴 − 𝐵 ) ) = 1 ↔ ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) = 1 ) ) |
5 |
|
ax-icn |
⊢ i ∈ ℂ |
6 |
5
|
a1i |
⊢ ( 𝜑 → i ∈ ℂ ) |
7 |
|
2cnd |
⊢ ( 𝜑 → 2 ∈ ℂ ) |
8 |
|
picn |
⊢ π ∈ ℂ |
9 |
8
|
a1i |
⊢ ( 𝜑 → π ∈ ℂ ) |
10 |
7 9
|
mulcld |
⊢ ( 𝜑 → ( 2 · π ) ∈ ℂ ) |
11 |
6 10
|
mulcld |
⊢ ( 𝜑 → ( i · ( 2 · π ) ) ∈ ℂ ) |
12 |
1 2
|
subcld |
⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ ) |
13 |
|
ine0 |
⊢ i ≠ 0 |
14 |
13
|
a1i |
⊢ ( 𝜑 → i ≠ 0 ) |
15 |
|
2ne0 |
⊢ 2 ≠ 0 |
16 |
15
|
a1i |
⊢ ( 𝜑 → 2 ≠ 0 ) |
17 |
|
pine0 |
⊢ π ≠ 0 |
18 |
17
|
a1i |
⊢ ( 𝜑 → π ≠ 0 ) |
19 |
7 9 16 18
|
mulne0d |
⊢ ( 𝜑 → ( 2 · π ) ≠ 0 ) |
20 |
6 10 14 19
|
mulne0d |
⊢ ( 𝜑 → ( i · ( 2 · π ) ) ≠ 0 ) |
21 |
11 12 20
|
zdivgd |
⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℤ ( ( i · ( 2 · π ) ) · 𝑛 ) = ( 𝐴 − 𝐵 ) ↔ ( ( 𝐴 − 𝐵 ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) ) |
22 |
|
eqcom |
⊢ ( 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) = 𝐴 ) |
23 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤ ) → 𝐵 ∈ ℂ ) |
24 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤ ) → ( i · ( 2 · π ) ) ∈ ℂ ) |
25 |
|
zcn |
⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ ) |
26 |
25
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℂ ) |
27 |
24 26
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤ ) → ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ ) |
28 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤ ) → 𝐴 ∈ ℂ ) |
29 |
23 27 28
|
addrsub |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤ ) → ( ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) = 𝐴 ↔ ( ( i · ( 2 · π ) ) · 𝑛 ) = ( 𝐴 − 𝐵 ) ) ) |
30 |
22 29
|
bitrid |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤ ) → ( 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ ( ( i · ( 2 · π ) ) · 𝑛 ) = ( 𝐴 − 𝐵 ) ) ) |
31 |
30
|
rexbidva |
⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℤ ( ( i · ( 2 · π ) ) · 𝑛 ) = ( 𝐴 − 𝐵 ) ) ) |
32 |
|
efeq1 |
⊢ ( ( 𝐴 − 𝐵 ) ∈ ℂ → ( ( exp ‘ ( 𝐴 − 𝐵 ) ) = 1 ↔ ( ( 𝐴 − 𝐵 ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) ) |
33 |
12 32
|
syl |
⊢ ( 𝜑 → ( ( exp ‘ ( 𝐴 − 𝐵 ) ) = 1 ↔ ( ( 𝐴 − 𝐵 ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) ) |
34 |
21 31 33
|
3bitr4rd |
⊢ ( 𝜑 → ( ( exp ‘ ( 𝐴 − 𝐵 ) ) = 1 ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) ) |
35 |
1
|
efcld |
⊢ ( 𝜑 → ( exp ‘ 𝐴 ) ∈ ℂ ) |
36 |
2
|
efcld |
⊢ ( 𝜑 → ( exp ‘ 𝐵 ) ∈ ℂ ) |
37 |
2
|
efne0d |
⊢ ( 𝜑 → ( exp ‘ 𝐵 ) ≠ 0 ) |
38 |
35 36 37
|
diveq1ad |
⊢ ( 𝜑 → ( ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) = 1 ↔ ( exp ‘ 𝐴 ) = ( exp ‘ 𝐵 ) ) ) |
39 |
4 34 38
|
3bitr3rd |
⊢ ( 𝜑 → ( ( exp ‘ 𝐴 ) = ( exp ‘ 𝐵 ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) ) |