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