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