| Step |
Hyp |
Ref |
Expression |
| 1 |
|
efhalfpi |
|- ( exp ` ( _i x. ( _pi / 2 ) ) ) = _i |
| 2 |
|
ax-icn |
|- _i e. CC |
| 3 |
|
ine0 |
|- _i =/= 0 |
| 4 |
|
halfpire |
|- ( _pi / 2 ) e. RR |
| 5 |
4
|
recni |
|- ( _pi / 2 ) e. CC |
| 6 |
2 5
|
mulcli |
|- ( _i x. ( _pi / 2 ) ) e. CC |
| 7 |
|
pipos |
|- 0 < _pi |
| 8 |
|
pire |
|- _pi e. RR |
| 9 |
|
lt0neg2 |
|- ( _pi e. RR -> ( 0 < _pi <-> -u _pi < 0 ) ) |
| 10 |
8 9
|
ax-mp |
|- ( 0 < _pi <-> -u _pi < 0 ) |
| 11 |
7 10
|
mpbi |
|- -u _pi < 0 |
| 12 |
|
halfpos2 |
|- ( _pi e. RR -> ( 0 < _pi <-> 0 < ( _pi / 2 ) ) ) |
| 13 |
8 12
|
ax-mp |
|- ( 0 < _pi <-> 0 < ( _pi / 2 ) ) |
| 14 |
7 13
|
mpbi |
|- 0 < ( _pi / 2 ) |
| 15 |
8
|
renegcli |
|- -u _pi e. RR |
| 16 |
|
0re |
|- 0 e. RR |
| 17 |
15 16 4
|
lttri |
|- ( ( -u _pi < 0 /\ 0 < ( _pi / 2 ) ) -> -u _pi < ( _pi / 2 ) ) |
| 18 |
11 14 17
|
mp2an |
|- -u _pi < ( _pi / 2 ) |
| 19 |
|
reim |
|- ( ( _pi / 2 ) e. CC -> ( Re ` ( _pi / 2 ) ) = ( Im ` ( _i x. ( _pi / 2 ) ) ) ) |
| 20 |
5 19
|
ax-mp |
|- ( Re ` ( _pi / 2 ) ) = ( Im ` ( _i x. ( _pi / 2 ) ) ) |
| 21 |
|
rere |
|- ( ( _pi / 2 ) e. RR -> ( Re ` ( _pi / 2 ) ) = ( _pi / 2 ) ) |
| 22 |
4 21
|
ax-mp |
|- ( Re ` ( _pi / 2 ) ) = ( _pi / 2 ) |
| 23 |
20 22
|
eqtr3i |
|- ( Im ` ( _i x. ( _pi / 2 ) ) ) = ( _pi / 2 ) |
| 24 |
18 23
|
breqtrri |
|- -u _pi < ( Im ` ( _i x. ( _pi / 2 ) ) ) |
| 25 |
8
|
a1i |
|- ( T. -> _pi e. RR ) |
| 26 |
25 25
|
ltaddposd |
|- ( T. -> ( 0 < _pi <-> _pi < ( _pi + _pi ) ) ) |
| 27 |
7 26
|
mpbii |
|- ( T. -> _pi < ( _pi + _pi ) ) |
| 28 |
|
picn |
|- _pi e. CC |
| 29 |
28
|
times2i |
|- ( _pi x. 2 ) = ( _pi + _pi ) |
| 30 |
27 29
|
breqtrrdi |
|- ( T. -> _pi < ( _pi x. 2 ) ) |
| 31 |
|
2rp |
|- 2 e. RR+ |
| 32 |
31
|
a1i |
|- ( T. -> 2 e. RR+ ) |
| 33 |
25 25 32
|
ltdivmul2d |
|- ( T. -> ( ( _pi / 2 ) < _pi <-> _pi < ( _pi x. 2 ) ) ) |
| 34 |
30 33
|
mpbird |
|- ( T. -> ( _pi / 2 ) < _pi ) |
| 35 |
34
|
mptru |
|- ( _pi / 2 ) < _pi |
| 36 |
4 8 35
|
ltleii |
|- ( _pi / 2 ) <_ _pi |
| 37 |
23 36
|
eqbrtri |
|- ( Im ` ( _i x. ( _pi / 2 ) ) ) <_ _pi |
| 38 |
|
ellogrn |
|- ( ( _i x. ( _pi / 2 ) ) e. ran log <-> ( ( _i x. ( _pi / 2 ) ) e. CC /\ -u _pi < ( Im ` ( _i x. ( _pi / 2 ) ) ) /\ ( Im ` ( _i x. ( _pi / 2 ) ) ) <_ _pi ) ) |
| 39 |
6 24 37 38
|
mpbir3an |
|- ( _i x. ( _pi / 2 ) ) e. ran log |
| 40 |
|
logeftb |
|- ( ( _i e. CC /\ _i =/= 0 /\ ( _i x. ( _pi / 2 ) ) e. ran log ) -> ( ( log ` _i ) = ( _i x. ( _pi / 2 ) ) <-> ( exp ` ( _i x. ( _pi / 2 ) ) ) = _i ) ) |
| 41 |
2 3 39 40
|
mp3an |
|- ( ( log ` _i ) = ( _i x. ( _pi / 2 ) ) <-> ( exp ` ( _i x. ( _pi / 2 ) ) ) = _i ) |
| 42 |
1 41
|
mpbir |
|- ( log ` _i ) = ( _i x. ( _pi / 2 ) ) |