Metamath Proof Explorer

Theorem lognegb

Description: If a number has imaginary part equal to _pi , then it is on the negative real axis and vice-versa. (Contributed by Mario Carneiro, 23-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 logneg 
 |-  ( -u A e. RR+ -> ( log ` -u -u A ) = ( ( log ` -u A ) + ( _i x. _pi ) ) )
2 1 fveq2d 
 |-  ( -u A e. RR+ -> ( Im ` ( log ` -u -u A ) ) = ( Im ` ( ( log ` -u A ) + ( _i x. _pi ) ) ) )
3 relogcl 
 |-  ( -u A e. RR+ -> ( log ` -u A ) e. RR )
4 pire 
 |-  _pi e. RR
5 crim 
 |-  ( ( ( log ` -u A ) e. RR /\ _pi e. RR ) -> ( Im ` ( ( log ` -u A ) + ( _i x. _pi ) ) ) = _pi )
6 3 4 5 sylancl 
 |-  ( -u A e. RR+ -> ( Im ` ( ( log ` -u A ) + ( _i x. _pi ) ) ) = _pi )
7 2 6 eqtrd 
 |-  ( -u A e. RR+ -> ( Im ` ( log ` -u -u A ) ) = _pi )
8 negneg 
 |-  ( A e. CC -> -u -u A = A )
9 8 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u -u A = A )
10 9 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` -u -u A ) = ( log ` A ) )
11 10 fveqeq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( Im ` ( log ` -u -u A ) ) = _pi <-> ( Im ` ( log ` A ) ) = _pi ) )
12 7 11 syl5ib 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u A e. RR+ -> ( Im ` ( log ` A ) ) = _pi ) )
13 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
14 13 replimd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) = ( ( Re ` ( log ` A ) ) + ( _i x. ( Im ` ( log ` A ) ) ) ) )
15 14 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = ( exp ` ( ( Re ` ( log ` A ) ) + ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
16 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
17 13 recld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) e. RR )
18 17 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Re ` ( log ` A ) ) e. CC )
19 ax-icn 
 |-  _i e. CC
20 13 imcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Im ` ( log ` A ) ) e. RR )
21 20 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( Im ` ( log ` A ) ) e. CC )
22 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` ( log ` A ) ) e. CC ) -> ( _i x. ( Im ` ( log ` A ) ) ) e. CC )
23 19 21 22 sylancr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( _i x. ( Im ` ( log ` A ) ) ) e. CC )
24 efadd 
 |-  ( ( ( Re ` ( log ` A ) ) e. CC /\ ( _i x. ( Im ` ( log ` A ) ) ) e. CC ) -> ( exp ` ( ( Re ` ( log ` A ) ) + ( _i x. ( Im ` ( log ` A ) ) ) ) ) = ( ( exp ` ( Re ` ( log ` A ) ) ) x. ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
25 18 23 24 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( ( Re ` ( log ` A ) ) + ( _i x. ( Im ` ( log ` A ) ) ) ) ) = ( ( exp ` ( Re ` ( log ` A ) ) ) x. ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
26 15 16 25 3eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> A = ( ( exp ` ( Re ` ( log ` A ) ) ) x. ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
27 oveq2 
 |-  ( ( Im ` ( log ` A ) ) = _pi -> ( _i x. ( Im ` ( log ` A ) ) ) = ( _i x. _pi ) )
28 27 fveq2d 
 |-  ( ( Im ` ( log ` A ) ) = _pi -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( exp ` ( _i x. _pi ) ) )
29 efipi 
 |-  ( exp ` ( _i x. _pi ) ) = -u 1
30 28 29 eqtrdi 
 |-  ( ( Im ` ( log ` A ) ) = _pi -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = -u 1 )
31 30 oveq2d 
 |-  ( ( Im ` ( log ` A ) ) = _pi -> ( ( exp ` ( Re ` ( log ` A ) ) ) x. ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) = ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) )
32 31 eqeq2d 
 |-  ( ( Im ` ( log ` A ) ) = _pi -> ( A = ( ( exp ` ( Re ` ( log ` A ) ) ) x. ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ) <-> A = ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) ) )
33 26 32 syl5ibcom 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( Im ` ( log ` A ) ) = _pi -> A = ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) ) )
34 17 rpefcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( Re ` ( log ` A ) ) ) e. RR+ )
35 34 rpcnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( Re ` ( log ` A ) ) ) e. CC )
36 neg1cn 
 |-  -u 1 e. CC
37 mulcom 
 |-  ( ( ( exp ` ( Re ` ( log ` A ) ) ) e. CC /\ -u 1 e. CC ) -> ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) = ( -u 1 x. ( exp ` ( Re ` ( log ` A ) ) ) ) )
38 35 36 37 sylancl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) = ( -u 1 x. ( exp ` ( Re ` ( log ` A ) ) ) ) )
39 35 mulm1d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u 1 x. ( exp ` ( Re ` ( log ` A ) ) ) ) = -u ( exp ` ( Re ` ( log ` A ) ) ) )
40 38 39 eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) = -u ( exp ` ( Re ` ( log ` A ) ) ) )
41 40 negeqd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) = -u -u ( exp ` ( Re ` ( log ` A ) ) ) )
42 35 negnegd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u -u ( exp ` ( Re ` ( log ` A ) ) ) = ( exp ` ( Re ` ( log ` A ) ) ) )
43 41 42 eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) = ( exp ` ( Re ` ( log ` A ) ) ) )
44 43 34 eqeltrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> -u ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) e. RR+ )
45 negeq 
 |-  ( A = ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) -> -u A = -u ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) )
46 45 eleq1d 
 |-  ( A = ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) -> ( -u A e. RR+ <-> -u ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) e. RR+ ) )
47 44 46 syl5ibrcom 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( A = ( ( exp ` ( Re ` ( log ` A ) ) ) x. -u 1 ) -> -u A e. RR+ ) )
48 33 47 syld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( Im ` ( log ` A ) ) = _pi -> -u A e. RR+ ) )
49 12 48 impbid 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -u A e. RR+ <-> ( Im ` ( log ` A ) ) = _pi ) )