Metamath Proof Explorer

Theorem logi

Description: The natural logarithm of _i . (Contributed by Scott Fenton, 13-Apr-2020)

Ref Expression
Assertion logi 
|- ( log ` _i ) = ( _i x. ( _pi / 2 ) )

Proof

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