Metamath Proof Explorer

Theorem abslogle

Description: Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017)

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

Proof

Step Hyp Ref Expression
1 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
2 1 abscld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( log ` A ) ) e. RR )
3 absrpcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
4 relogcl 
 |-  ( ( abs ` A ) e. RR+ -> ( log ` ( abs ` A ) ) e. RR )
5 3 4 syl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` ( abs ` A ) ) e. RR )
6 5 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` ( abs ` A ) ) e. CC )
7 6 abscld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( log ` ( abs ` A ) ) ) e. RR )
8 1 imcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Im ` ( log ` A ) ) e. RR )
9 8 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Im ` ( log ` A ) ) e. CC )
10 9 abscld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( Im ` ( log ` A ) ) ) e. RR )
11 7 10 readdcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` ( log ` ( abs ` A ) ) ) + ( abs ` ( Im ` ( log ` A ) ) ) ) e. RR )
12 pire 
 |-  _pi e. RR
13 12 a1i 
 |-  ( ( A e. CC /\ A =/= 0 ) -> _pi e. RR )
14 7 13 readdcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` ( log ` ( abs ` A ) ) ) + _pi ) e. RR )
15 1 recld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) e. RR )
16 15 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) e. CC )
17 ax-icn 
 |-  _i e. CC
18 17 a1i 
 |-  ( ( A e. CC /\ A =/= 0 ) -> _i e. CC )
19 18 9 mulcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( _i x. ( Im ` ( log ` A ) ) ) e. CC )
20 16 19 abstrid 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( ( Re ` ( log ` A ) ) + ( _i x. ( Im ` ( log ` A ) ) ) ) ) <_ ( ( abs ` ( Re ` ( log ` A ) ) ) + ( abs ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
21 1 replimd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) = ( ( Re ` ( log ` A ) ) + ( _i x. ( Im ` ( log ` A ) ) ) ) )
22 21 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( log ` A ) ) = ( abs ` ( ( Re ` ( log ` A ) ) + ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
23 relog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) = ( log ` ( abs ` A ) ) )
24 23 eqcomd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` ( abs ` A ) ) = ( Re ` ( log ` A ) ) )
25 24 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( log ` ( abs ` A ) ) ) = ( abs ` ( Re ` ( log ` A ) ) ) )
26 18 9 absmuld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( ( abs ` _i ) x. ( abs ` ( Im ` ( log ` A ) ) ) ) )
27 absi 
 |-  ( abs ` _i ) = 1
28 27 oveq1i 
 |-  ( ( abs ` _i ) x. ( abs ` ( Im ` ( log ` A ) ) ) ) = ( 1 x. ( abs ` ( Im ` ( log ` A ) ) ) )
29 10 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( Im ` ( log ` A ) ) ) e. CC )
30 29 mullidd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 x. ( abs ` ( Im ` ( log ` A ) ) ) ) = ( abs ` ( Im ` ( log ` A ) ) ) )
31 28 30 eqtrid 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` _i ) x. ( abs ` ( Im ` ( log ` A ) ) ) ) = ( abs ` ( Im ` ( log ` A ) ) ) )
32 26 31 eqtr2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( Im ` ( log ` A ) ) ) = ( abs ` ( _i x. ( Im ` ( log ` A ) ) ) ) )
33 25 32 oveq12d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` ( log ` ( abs ` A ) ) ) + ( abs ` ( Im ` ( log ` A ) ) ) ) = ( ( abs ` ( Re ` ( log ` A ) ) ) + ( abs ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
34 20 22 33 3brtr4d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( log ` A ) ) <_ ( ( abs ` ( log ` ( abs ` A ) ) ) + ( abs ` ( Im ` ( log ` A ) ) ) ) )
35 abslogimle 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( Im ` ( log ` A ) ) ) <_ _pi )
36 10 13 7 35 leadd2dd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` ( log ` ( abs ` A ) ) ) + ( abs ` ( Im ` ( log ` A ) ) ) ) <_ ( ( abs ` ( log ` ( abs ` A ) ) ) + _pi ) )
37 2 11 14 34 36 letrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` ( log ` A ) ) <_ ( ( abs ` ( log ` ( abs ` A ) ) ) + _pi ) )