This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cxpi11d

Description: _i to the powers of A and B are equal iff A and B are a multiple of 4 apart. EDITORIAL: This theorem may be revised to a more convenient form. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses cxpi11d.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
cxpi11d.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion cxpi11d ( 𝜑 → ( ( i ↑𝑐 𝐴 ) = ( i ↑𝑐 𝐵 ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( 𝐵 + ( 4 · 𝑛 ) ) ) )

Proof

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 · 𝑛 ) ) ) )