Metamath Proof Explorer

Theorem logimul

Description: Multiplying a number by _i increases the logarithm of the number by _i _pi / 2 . (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion logimul 
|- ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( log ` ( _i x. A ) ) = ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
2 1 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( log ` A ) e. CC )
3 ax-icn 
 |-  _i e. CC
4 halfpire 
 |-  ( _pi / 2 ) e. RR
5 4 recni 
 |-  ( _pi / 2 ) e. CC
6 3 5 mulcli 
 |-  ( _i x. ( _pi / 2 ) ) e. CC
7 efadd 
 |-  ( ( ( log ` A ) e. CC /\ ( _i x. ( _pi / 2 ) ) e. CC ) -> ( exp ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) = ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. ( _pi / 2 ) ) ) ) )
8 2 6 7 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( exp ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) = ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. ( _pi / 2 ) ) ) ) )
9 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
10 9 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( exp ` ( log ` A ) ) = A )
11 efhalfpi 
 |-  ( exp ` ( _i x. ( _pi / 2 ) ) ) = _i
12 11 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( exp ` ( _i x. ( _pi / 2 ) ) ) = _i )
13 10 12 oveq12d 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. ( _pi / 2 ) ) ) ) = ( A x. _i ) )
14 simp1 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> A e. CC )
15 mulcom 
 |-  ( ( A e. CC /\ _i e. CC ) -> ( A x. _i ) = ( _i x. A ) )
16 14 3 15 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( A x. _i ) = ( _i x. A ) )
17 8 13 16 3eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( exp ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) = ( _i x. A ) )
18 17 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( log ` ( exp ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) ) = ( log ` ( _i x. A ) ) )
19 addcl 
 |-  ( ( ( log ` A ) e. CC /\ ( _i x. ( _pi / 2 ) ) e. CC ) -> ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) e. CC )
20 2 6 19 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) e. CC )
21 pire 
 |-  _pi e. RR
22 21 renegcli 
 |-  -u _pi e. RR
23 22 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> -u _pi e. RR )
24 2 imcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( Im ` ( log ` A ) ) e. RR )
25 readdcl 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ ( _pi / 2 ) e. RR ) -> ( ( Im ` ( log ` A ) ) + ( _pi / 2 ) ) e. RR )
26 24 4 25 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( ( Im ` ( log ` A ) ) + ( _pi / 2 ) ) e. RR )
27 logimcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
28 27 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( -u _pi < ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ _pi ) )
29 28 simpld 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> -u _pi < ( Im ` ( log ` A ) ) )
30 pirp 
 |-  _pi e. RR+
31 rphalfcl 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) e. RR+ )
32 30 31 ax-mp 
 |-  ( _pi / 2 ) e. RR+
33 ltaddrp 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ ( _pi / 2 ) e. RR+ ) -> ( Im ` ( log ` A ) ) < ( ( Im ` ( log ` A ) ) + ( _pi / 2 ) ) )
34 24 32 33 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( Im ` ( log ` A ) ) < ( ( Im ` ( log ` A ) ) + ( _pi / 2 ) ) )
35 23 24 26 29 34 lttrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> -u _pi < ( ( Im ` ( log ` A ) ) + ( _pi / 2 ) ) )
36 imadd 
 |-  ( ( ( log ` A ) e. CC /\ ( _i x. ( _pi / 2 ) ) e. CC ) -> ( Im ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) = ( ( Im ` ( log ` A ) ) + ( Im ` ( _i x. ( _pi / 2 ) ) ) ) )
37 2 6 36 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( Im ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) = ( ( Im ` ( log ` A ) ) + ( Im ` ( _i x. ( _pi / 2 ) ) ) ) )
38 reim 
 |-  ( ( _pi / 2 ) e. CC -> ( Re ` ( _pi / 2 ) ) = ( Im ` ( _i x. ( _pi / 2 ) ) ) )
39 5 38 ax-mp 
 |-  ( Re ` ( _pi / 2 ) ) = ( Im ` ( _i x. ( _pi / 2 ) ) )
40 rere 
 |-  ( ( _pi / 2 ) e. RR -> ( Re ` ( _pi / 2 ) ) = ( _pi / 2 ) )
41 4 40 ax-mp 
 |-  ( Re ` ( _pi / 2 ) ) = ( _pi / 2 )
42 39 41 eqtr3i 
 |-  ( Im ` ( _i x. ( _pi / 2 ) ) ) = ( _pi / 2 )
43 42 oveq2i 
 |-  ( ( Im ` ( log ` A ) ) + ( Im ` ( _i x. ( _pi / 2 ) ) ) ) = ( ( Im ` ( log ` A ) ) + ( _pi / 2 ) )
44 37 43 eqtrdi 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( Im ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) = ( ( Im ` ( log ` A ) ) + ( _pi / 2 ) ) )
45 35 44 breqtrrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> -u _pi < ( Im ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) )
46 argrege0 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( Im ` ( log ` A ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
47 4 renegcli 
 |-  -u ( _pi / 2 ) e. RR
48 47 4 elicc2i 
 |-  ( ( Im ` ( log ` A ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( ( Im ` ( log ` A ) ) e. RR /\ -u ( _pi / 2 ) <_ ( Im ` ( log ` A ) ) /\ ( Im ` ( log ` A ) ) <_ ( _pi / 2 ) ) )
49 48 simp3bi 
 |-  ( ( Im ` ( log ` A ) ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( Im ` ( log ` A ) ) <_ ( _pi / 2 ) )
50 46 49 syl 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( Im ` ( log ` A ) ) <_ ( _pi / 2 ) )
51 21 recni 
 |-  _pi e. CC
52 pidiv2halves 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi
53 51 5 5 52 subaddrii 
 |-  ( _pi - ( _pi / 2 ) ) = ( _pi / 2 )
54 50 53 breqtrrdi 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( Im ` ( log ` A ) ) <_ ( _pi - ( _pi / 2 ) ) )
55 4 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( _pi / 2 ) e. RR )
56 21 a1i 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> _pi e. RR )
57 leaddsub 
 |-  ( ( ( Im ` ( log ` A ) ) e. RR /\ ( _pi / 2 ) e. RR /\ _pi e. RR ) -> ( ( ( Im ` ( log ` A ) ) + ( _pi / 2 ) ) <_ _pi <-> ( Im ` ( log ` A ) ) <_ ( _pi - ( _pi / 2 ) ) ) )
58 24 55 56 57 syl3anc 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( ( ( Im ` ( log ` A ) ) + ( _pi / 2 ) ) <_ _pi <-> ( Im ` ( log ` A ) ) <_ ( _pi - ( _pi / 2 ) ) ) )
59 54 58 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( ( Im ` ( log ` A ) ) + ( _pi / 2 ) ) <_ _pi )
60 44 59 eqbrtrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( Im ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) <_ _pi )
61 ellogrn 
 |-  ( ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) e. ran log <-> ( ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) e. CC /\ -u _pi < ( Im ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) /\ ( Im ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) <_ _pi ) )
62 20 45 60 61 syl3anbrc 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) e. ran log )
63 logef 
 |-  ( ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) e. ran log -> ( log ` ( exp ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) ) = ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) )
64 62 63 syl 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( log ` ( exp ` ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) ) ) = ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) )
65 18 64 eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 /\ 0 <_ ( Re ` A ) ) -> ( log ` ( _i x. A ) ) = ( ( log ` A ) + ( _i x. ( _pi / 2 ) ) ) )