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