Metamath Proof Explorer

Theorem logimclad

Description: The imaginary part of the logarithm is in ( -upi (,] pi ) . Alternate form of logimcld . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses logimcld.1 
|- ( ph -> X e. CC )
logimcld.2 
|- ( ph -> X =/= 0 )
Assertion logimclad 
|- ( ph -> ( Im ` ( log ` X ) ) e. ( -u _pi (,] _pi ) )

Proof

Step Hyp Ref Expression
1 logimcld.1 
 |-  ( ph -> X e. CC )
2 logimcld.2 
 |-  ( ph -> X =/= 0 )
3 1 2 logcld 
 |-  ( ph -> ( log ` X ) e. CC )
4 3 imcld 
 |-  ( ph -> ( Im ` ( log ` X ) ) e. RR )
5 1 2 logimcld 
 |-  ( ph -> ( -u _pi < ( Im ` ( log ` X ) ) /\ ( Im ` ( log ` X ) ) <_ _pi ) )
6 5 simpld 
 |-  ( ph -> -u _pi < ( Im ` ( log ` X ) ) )
7 5 simprd 
 |-  ( ph -> ( Im ` ( log ` X ) ) <_ _pi )
8 pire 
 |-  _pi e. RR
9 8 renegcli 
 |-  -u _pi e. RR
10 9 rexri 
 |-  -u _pi e. RR*
11 elioc2 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> ( ( Im ` ( log ` X ) ) e. ( -u _pi (,] _pi ) <-> ( ( Im ` ( log ` X ) ) e. RR /\ -u _pi < ( Im ` ( log ` X ) ) /\ ( Im ` ( log ` X ) ) <_ _pi ) ) )
12 10 8 11 mp2an 
 |-  ( ( Im ` ( log ` X ) ) e. ( -u _pi (,] _pi ) <-> ( ( Im ` ( log ` X ) ) e. RR /\ -u _pi < ( Im ` ( log ` X ) ) /\ ( Im ` ( log ` X ) ) <_ _pi ) )
13 4 6 7 12 syl3anbrc 
 |-  ( ph -> ( Im ` ( log ` X ) ) e. ( -u _pi (,] _pi ) )