Metamath Proof Explorer

Theorem abslogimle

Description: The imaginary part of the logarithm function has absolute value less than pi. (Contributed by Mario Carneiro, 3-Jul-2017)

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

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 1 a1i 
 |-  ( ( A e. CC /\ A =/= 0 ) -> _pi e. RR )
3 2 renegcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u _pi e. RR )
4 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
5 4 imcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Im ` ( log ` A ) ) e. RR )
6 logimcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
7 6 simpld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u _pi < ( Im ` ( log ` A ) ) )
8 3 5 7 ltled 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u _pi <_ ( Im ` ( log ` A ) ) )
9 6 simprd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Im ` ( log ` A ) ) <_ _pi )
10 5 2 absled 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` ( Im ` ( log ` A ) ) ) <_ _pi <-> ( -u _pi <_ ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) ) )
11 8 9 10 mpbir2and 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( Im ` ( log ` A ) ) ) <_ _pi )