Metamath Proof Explorer

Theorem logimcl

Description: Closure of the imaginary part of the logarithm function. (Contributed by Mario Carneiro, 23-Sep-2014) (Revised by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion logimcl 
|- ( ( A e. CC /\ A =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )

Proof

Step Hyp Ref Expression
1 logrncl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. ran log )
2 ellogrn 
 |-  ( ( log ` A ) e. ran log <-> ( ( log ` A ) e. CC /\ -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
3 1 2 sylib 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( log ` A ) e. CC /\ -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
4 3simpc 
 |-  ( ( ( log ` A ) e. CC /\ -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
5 3 4 syl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )