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 
|- ( ph -> A e. CC )
cxpi11d.b 
|- ( ph -> B e. CC )
Assertion cxpi11d 
|- ( ph -> ( ( _i ^c A ) = ( _i ^c B ) <-> E. n e. ZZ A = ( B + ( 4 x. n ) ) ) )

Proof

Step Hyp Ref Expression
1 cxpi11d.a 
 |-  ( ph -> A e. CC )
2 cxpi11d.b 
 |-  ( ph -> B e. CC )
3 ax-icn 
 |-  _i e. CC
4 3 a1i 
 |-  ( ph -> _i e. CC )
5 ine0 
 |-  _i =/= 0
6 5 a1i 
 |-  ( ph -> _i =/= 0 )
7 ine1 
 |-  _i =/= 1
8 7 a1i 
 |-  ( ph -> _i =/= 1 )
9 4 1 2 6 8 cxp112d 
 |-  ( ph -> ( ( _i ^c A ) = ( _i ^c B ) <-> E. n e. ZZ A = ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` _i ) ) ) ) )
10 2cn 
 |-  2 e. CC
11 picn 
 |-  _pi e. CC
12 10 11 mulcli 
 |-  ( 2 x. _pi ) e. CC
13 3 12 mulcli 
 |-  ( _i x. ( 2 x. _pi ) ) e. CC
14 13 a1i 
 |-  ( n e. ZZ -> ( _i x. ( 2 x. _pi ) ) e. CC )
15 zcn 
 |-  ( n e. ZZ -> n e. CC )
16 logcl 
 |-  ( ( _i e. CC /\ _i =/= 0 ) -> ( log ` _i ) e. CC )
17 3 5 16 mp2an 
 |-  ( log ` _i ) e. CC
18 17 a1i 
 |-  ( n e. ZZ -> ( log ` _i ) e. CC )
19 logccne0 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ _i =/= 1 ) -> ( log ` _i ) =/= 0 )
20 3 5 7 19 mp3an 
 |-  ( log ` _i ) =/= 0
21 20 a1i 
 |-  ( n e. ZZ -> ( log ` _i ) =/= 0 )
22 14 15 18 21 div23d 
 |-  ( n e. ZZ -> ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` _i ) ) = ( ( ( _i x. ( 2 x. _pi ) ) / ( log ` _i ) ) x. n ) )
23 logi 
 |-  ( log ` _i ) = ( _i x. ( _pi / 2 ) )
24 23 oveq2i 
 |-  ( ( _i x. ( 2 x. _pi ) ) / ( log ` _i ) ) = ( ( _i x. ( 2 x. _pi ) ) / ( _i x. ( _pi / 2 ) ) )
25 12 a1i 
 |-  ( T. -> ( 2 x. _pi ) e. CC )
26 2ne0 
 |-  2 =/= 0
27 11 10 26 divcli 
 |-  ( _pi / 2 ) e. CC
28 27 a1i 
 |-  ( T. -> ( _pi / 2 ) e. CC )
29 3 a1i 
 |-  ( T. -> _i e. CC )
30 pine0 
 |-  _pi =/= 0
31 11 10 30 26 divne0i 
 |-  ( _pi / 2 ) =/= 0
32 31 a1i 
 |-  ( T. -> ( _pi / 2 ) =/= 0 )
33 5 a1i 
 |-  ( T. -> _i =/= 0 )
34 25 28 29 32 33 divcan5d 
 |-  ( T. -> ( ( _i x. ( 2 x. _pi ) ) / ( _i x. ( _pi / 2 ) ) ) = ( ( 2 x. _pi ) / ( _pi / 2 ) ) )
35 34 mptru 
 |-  ( ( _i x. ( 2 x. _pi ) ) / ( _i x. ( _pi / 2 ) ) ) = ( ( 2 x. _pi ) / ( _pi / 2 ) )
36 10 11 27 31 divassi 
 |-  ( ( 2 x. _pi ) / ( _pi / 2 ) ) = ( 2 x. ( _pi / ( _pi / 2 ) ) )
37 11 a1i 
 |-  ( T. -> _pi e. CC )
38 2cnd 
 |-  ( T. -> 2 e. CC )
39 30 a1i 
 |-  ( T. -> _pi =/= 0 )
40 26 a1i 
 |-  ( T. -> 2 =/= 0 )
41 37 38 39 40 ddcand 
 |-  ( T. -> ( _pi / ( _pi / 2 ) ) = 2 )
42 41 mptru 
 |-  ( _pi / ( _pi / 2 ) ) = 2
43 42 oveq2i 
 |-  ( 2 x. ( _pi / ( _pi / 2 ) ) ) = ( 2 x. 2 )
44 2t2e4 
 |-  ( 2 x. 2 ) = 4
45 36 43 44 3eqtri 
 |-  ( ( 2 x. _pi ) / ( _pi / 2 ) ) = 4
46 24 35 45 3eqtri 
 |-  ( ( _i x. ( 2 x. _pi ) ) / ( log ` _i ) ) = 4
47 46 oveq1i 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) / ( log ` _i ) ) x. n ) = ( 4 x. n )
48 22 47 eqtrdi 
 |-  ( n e. ZZ -> ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` _i ) ) = ( 4 x. n ) )
49 48 oveq2d 
 |-  ( n e. ZZ -> ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` _i ) ) ) = ( B + ( 4 x. n ) ) )
50 49 eqeq2d 
 |-  ( n e. ZZ -> ( A = ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` _i ) ) ) <-> A = ( B + ( 4 x. n ) ) ) )
51 50 rexbiia 
 |-  ( E. n e. ZZ A = ( B + ( ( ( _i x. ( 2 x. _pi ) ) x. n ) / ( log ` _i ) ) ) <-> E. n e. ZZ A = ( B + ( 4 x. n ) ) )
52 9 51 bitrdi 
 |-  ( ph -> ( ( _i ^c A ) = ( _i ^c B ) <-> E. n e. ZZ A = ( B + ( 4 x. n ) ) ) )