Step |
Hyp |
Ref |
Expression |
1 |
|
cxpi11d.a |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
2 |
|
cxpi11d.b |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
3 |
|
ax-icn |
⊢ i ∈ ℂ |
4 |
3
|
a1i |
⊢ ( 𝜑 → i ∈ ℂ ) |
5 |
|
ine0 |
⊢ i ≠ 0 |
6 |
5
|
a1i |
⊢ ( 𝜑 → i ≠ 0 ) |
7 |
|
ine1 |
⊢ i ≠ 1 |
8 |
7
|
a1i |
⊢ ( 𝜑 → i ≠ 1 ) |
9 |
4 1 2 6 8
|
cxp112d |
⊢ ( 𝜑 → ( ( i ↑𝑐 𝐴 ) = ( i ↑𝑐 𝐵 ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ i ) ) ) ) ) |
10 |
|
2cn |
⊢ 2 ∈ ℂ |
11 |
|
picn |
⊢ π ∈ ℂ |
12 |
10 11
|
mulcli |
⊢ ( 2 · π ) ∈ ℂ |
13 |
3 12
|
mulcli |
⊢ ( i · ( 2 · π ) ) ∈ ℂ |
14 |
13
|
a1i |
⊢ ( 𝑛 ∈ ℤ → ( i · ( 2 · π ) ) ∈ ℂ ) |
15 |
|
zcn |
⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ ) |
16 |
|
logcl |
⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ) → ( log ‘ i ) ∈ ℂ ) |
17 |
3 5 16
|
mp2an |
⊢ ( log ‘ i ) ∈ ℂ |
18 |
17
|
a1i |
⊢ ( 𝑛 ∈ ℤ → ( log ‘ i ) ∈ ℂ ) |
19 |
|
logccne0 |
⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ i ≠ 1 ) → ( log ‘ i ) ≠ 0 ) |
20 |
3 5 7 19
|
mp3an |
⊢ ( log ‘ i ) ≠ 0 |
21 |
20
|
a1i |
⊢ ( 𝑛 ∈ ℤ → ( log ‘ i ) ≠ 0 ) |
22 |
14 15 18 21
|
div23d |
⊢ ( 𝑛 ∈ ℤ → ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ i ) ) = ( ( ( i · ( 2 · π ) ) / ( log ‘ i ) ) · 𝑛 ) ) |
23 |
|
logi |
⊢ ( log ‘ i ) = ( i · ( π / 2 ) ) |
24 |
23
|
oveq2i |
⊢ ( ( i · ( 2 · π ) ) / ( log ‘ i ) ) = ( ( i · ( 2 · π ) ) / ( i · ( π / 2 ) ) ) |
25 |
12
|
a1i |
⊢ ( ⊤ → ( 2 · π ) ∈ ℂ ) |
26 |
|
2ne0 |
⊢ 2 ≠ 0 |
27 |
11 10 26
|
divcli |
⊢ ( π / 2 ) ∈ ℂ |
28 |
27
|
a1i |
⊢ ( ⊤ → ( π / 2 ) ∈ ℂ ) |
29 |
3
|
a1i |
⊢ ( ⊤ → i ∈ ℂ ) |
30 |
|
pine0 |
⊢ π ≠ 0 |
31 |
11 10 30 26
|
divne0i |
⊢ ( π / 2 ) ≠ 0 |
32 |
31
|
a1i |
⊢ ( ⊤ → ( π / 2 ) ≠ 0 ) |
33 |
5
|
a1i |
⊢ ( ⊤ → i ≠ 0 ) |
34 |
25 28 29 32 33
|
divcan5d |
⊢ ( ⊤ → ( ( i · ( 2 · π ) ) / ( i · ( π / 2 ) ) ) = ( ( 2 · π ) / ( π / 2 ) ) ) |
35 |
34
|
mptru |
⊢ ( ( i · ( 2 · π ) ) / ( i · ( π / 2 ) ) ) = ( ( 2 · π ) / ( π / 2 ) ) |
36 |
10 11 27 31
|
divassi |
⊢ ( ( 2 · π ) / ( π / 2 ) ) = ( 2 · ( π / ( π / 2 ) ) ) |
37 |
11
|
a1i |
⊢ ( ⊤ → π ∈ ℂ ) |
38 |
|
2cnd |
⊢ ( ⊤ → 2 ∈ ℂ ) |
39 |
30
|
a1i |
⊢ ( ⊤ → π ≠ 0 ) |
40 |
26
|
a1i |
⊢ ( ⊤ → 2 ≠ 0 ) |
41 |
37 38 39 40
|
ddcand |
⊢ ( ⊤ → ( π / ( π / 2 ) ) = 2 ) |
42 |
41
|
mptru |
⊢ ( π / ( π / 2 ) ) = 2 |
43 |
42
|
oveq2i |
⊢ ( 2 · ( π / ( π / 2 ) ) ) = ( 2 · 2 ) |
44 |
|
2t2e4 |
⊢ ( 2 · 2 ) = 4 |
45 |
36 43 44
|
3eqtri |
⊢ ( ( 2 · π ) / ( π / 2 ) ) = 4 |
46 |
24 35 45
|
3eqtri |
⊢ ( ( i · ( 2 · π ) ) / ( log ‘ i ) ) = 4 |
47 |
46
|
oveq1i |
⊢ ( ( ( i · ( 2 · π ) ) / ( log ‘ i ) ) · 𝑛 ) = ( 4 · 𝑛 ) |
48 |
22 47
|
eqtrdi |
⊢ ( 𝑛 ∈ ℤ → ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ i ) ) = ( 4 · 𝑛 ) ) |
49 |
48
|
oveq2d |
⊢ ( 𝑛 ∈ ℤ → ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ i ) ) ) = ( 𝐵 + ( 4 · 𝑛 ) ) ) |
50 |
49
|
eqeq2d |
⊢ ( 𝑛 ∈ ℤ → ( 𝐴 = ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ i ) ) ) ↔ 𝐴 = ( 𝐵 + ( 4 · 𝑛 ) ) ) ) |
51 |
50
|
rexbiia |
⊢ ( ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( ( ( i · ( 2 · π ) ) · 𝑛 ) / ( log ‘ i ) ) ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( 4 · 𝑛 ) ) ) |
52 |
9 51
|
bitrdi |
⊢ ( 𝜑 → ( ( i ↑𝑐 𝐴 ) = ( i ↑𝑐 𝐵 ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( 4 · 𝑛 ) ) ) ) |