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 φ A
cxpi11d.b φ B
Assertion cxpi11d φ i A = i B n A = B + 4 n

Proof

Step Hyp Ref Expression
1 cxpi11d.a φ A
2 cxpi11d.b φ 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 A = i B n A = B + i 2 π n log i
10 2cn 2
11 picn π
12 10 11 mulcli 2 π
13 3 12 mulcli i 2 π
14 13 a1i n i 2 π
15 zcn n n
16 logcl i i 0 log i
17 3 5 16 mp2an log i
18 17 a1i n log i
19 logccne0 i i 0 i 1 log i 0
20 3 5 7 19 mp3an log i 0
21 20 a1i n log i 0
22 14 15 18 21 div23d n i 2 π n log i = i 2 π log i n
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 n = 4 n
48 22 47 eqtrdi n i 2 π n log i = 4 n
49 48 oveq2d n B + i 2 π n log i = B + 4 n
50 49 eqeq2d n A = B + i 2 π n log i A = B + 4 n
51 50 rexbiia n A = B + i 2 π n log i n A = B + 4 n
52 9 51 bitrdi φ i A = i B n A = B + 4 n