Metamath Proof Explorer

Theorem logreclem

Description: Symmetry of the natural logarithm range by negation. Lemma for logrec . (Contributed by Saveliy Skresanov, 27-Dec-2016)

Ref Expression
Assertion logreclem 
|- ( ( A e. ran log /\ -. ( Im ` A ) = _pi ) -> -u A e. ran log )

Proof

Step Hyp Ref Expression
1 logrncn 
 |-  ( A e. ran log -> A e. CC )
2 1 adantr 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> A e. CC )
3 2 negcld 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> -u A e. CC )
4 ellogrn 
 |-  ( A e. ran log <-> ( A e. CC /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) )
5 4 biimpi 
 |-  ( A e. ran log -> ( A e. CC /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) )
6 5 simp3d 
 |-  ( A e. ran log -> ( Im ` A ) <_ _pi )
7 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
8 pire 
 |-  _pi e. RR
9 leneg 
 |-  ( ( ( Im ` A ) e. RR /\ _pi e. RR ) -> ( ( Im ` A ) <_ _pi <-> -u _pi <_ -u ( Im ` A ) ) )
10 9 biimpd 
 |-  ( ( ( Im ` A ) e. RR /\ _pi e. RR ) -> ( ( Im ` A ) <_ _pi -> -u _pi <_ -u ( Im ` A ) ) )
11 7 8 10 sylancl 
 |-  ( A e. CC -> ( ( Im ` A ) <_ _pi -> -u _pi <_ -u ( Im ` A ) ) )
12 1 6 11 sylc 
 |-  ( A e. ran log -> -u _pi <_ -u ( Im ` A ) )
13 8 renegcli 
 |-  -u _pi e. RR
14 13 a1i 
 |-  ( A e. CC -> -u _pi e. RR )
15 7 renegcld 
 |-  ( A e. CC -> -u ( Im ` A ) e. RR )
16 14 15 leloed 
 |-  ( A e. CC -> ( -u _pi <_ -u ( Im ` A ) <-> ( -u _pi < -u ( Im ` A ) \/ -u _pi = -u ( Im ` A ) ) ) )
17 16 biimpd 
 |-  ( A e. CC -> ( -u _pi <_ -u ( Im ` A ) -> ( -u _pi < -u ( Im ` A ) \/ -u _pi = -u ( Im ` A ) ) ) )
18 1 12 17 sylc 
 |-  ( A e. ran log -> ( -u _pi < -u ( Im ` A ) \/ -u _pi = -u ( Im ` A ) ) )
19 18 orcomd 
 |-  ( A e. ran log -> ( -u _pi = -u ( Im ` A ) \/ -u _pi < -u ( Im ` A ) ) )
20 19 orcanai 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> -u _pi < -u ( Im ` A ) )
21 5 simp2d 
 |-  ( A e. ran log -> -u _pi < ( Im ` A ) )
22 ltnegcon1 
 |-  ( ( _pi e. RR /\ ( Im ` A ) e. RR ) -> ( -u _pi < ( Im ` A ) <-> -u ( Im ` A ) < _pi ) )
23 22 biimpd 
 |-  ( ( _pi e. RR /\ ( Im ` A ) e. RR ) -> ( -u _pi < ( Im ` A ) -> -u ( Im ` A ) < _pi ) )
24 8 7 23 sylancr 
 |-  ( A e. CC -> ( -u _pi < ( Im ` A ) -> -u ( Im ` A ) < _pi ) )
25 1 21 24 sylc 
 |-  ( A e. ran log -> -u ( Im ` A ) < _pi )
26 25 adantr 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> -u ( Im ` A ) < _pi )
27 ltle 
 |-  ( ( -u ( Im ` A ) e. RR /\ _pi e. RR ) -> ( -u ( Im ` A ) < _pi -> -u ( Im ` A ) <_ _pi ) )
28 15 8 27 sylancl 
 |-  ( A e. CC -> ( -u ( Im ` A ) < _pi -> -u ( Im ` A ) <_ _pi ) )
29 1 28 syl 
 |-  ( A e. ran log -> ( -u ( Im ` A ) < _pi -> -u ( Im ` A ) <_ _pi ) )
30 29 adantr 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( -u ( Im ` A ) < _pi -> -u ( Im ` A ) <_ _pi ) )
31 26 30 mpd 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> -u ( Im ` A ) <_ _pi )
32 imneg 
 |-  ( A e. CC -> ( Im ` -u A ) = -u ( Im ` A ) )
33 32 breq2d 
 |-  ( A e. CC -> ( -u _pi < ( Im ` -u A ) <-> -u _pi < -u ( Im ` A ) ) )
34 2 33 syl 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( -u _pi < ( Im ` -u A ) <-> -u _pi < -u ( Im ` A ) ) )
35 32 breq1d 
 |-  ( A e. CC -> ( ( Im ` -u A ) <_ _pi <-> -u ( Im ` A ) <_ _pi ) )
36 2 35 syl 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( ( Im ` -u A ) <_ _pi <-> -u ( Im ` A ) <_ _pi ) )
37 34 36 anbi12d 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( ( -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) <-> ( -u _pi < -u ( Im ` A ) /\ -u ( Im ` A ) <_ _pi ) ) )
38 20 31 37 mpbir2and 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) )
39 3anass 
 |-  ( ( -u A e. CC /\ -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) <-> ( -u A e. CC /\ ( -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) ) )
40 3 38 39 sylanbrc 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> ( -u A e. CC /\ -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) )
41 ellogrn 
 |-  ( -u A e. ran log <-> ( -u A e. CC /\ -u _pi < ( Im ` -u A ) /\ ( Im ` -u A ) <_ _pi ) )
42 40 41 sylibr 
 |-  ( ( A e. ran log /\ -. -u _pi = -u ( Im ` A ) ) -> -u A e. ran log )
43 42 ex 
 |-  ( A e. ran log -> ( -. -u _pi = -u ( Im ` A ) -> -u A e. ran log ) )
44 43 orrd 
 |-  ( A e. ran log -> ( -u _pi = -u ( Im ` A ) \/ -u A e. ran log ) )
45 recn 
 |-  ( _pi e. RR -> _pi e. CC )
46 recn 
 |-  ( ( Im ` A ) e. RR -> ( Im ` A ) e. CC )
47 45 46 anim12i 
 |-  ( ( _pi e. RR /\ ( Im ` A ) e. RR ) -> ( _pi e. CC /\ ( Im ` A ) e. CC ) )
48 8 7 47 sylancr 
 |-  ( A e. CC -> ( _pi e. CC /\ ( Im ` A ) e. CC ) )
49 1 48 syl 
 |-  ( A e. ran log -> ( _pi e. CC /\ ( Im ` A ) e. CC ) )
50 neg11 
 |-  ( ( _pi e. CC /\ ( Im ` A ) e. CC ) -> ( -u _pi = -u ( Im ` A ) <-> _pi = ( Im ` A ) ) )
51 eqcom 
 |-  ( _pi = ( Im ` A ) <-> ( Im ` A ) = _pi )
52 50 51 bitrdi 
 |-  ( ( _pi e. CC /\ ( Im ` A ) e. CC ) -> ( -u _pi = -u ( Im ` A ) <-> ( Im ` A ) = _pi ) )
53 49 52 syl 
 |-  ( A e. ran log -> ( -u _pi = -u ( Im ` A ) <-> ( Im ` A ) = _pi ) )
54 53 orbi1d 
 |-  ( A e. ran log -> ( ( -u _pi = -u ( Im ` A ) \/ -u A e. ran log ) <-> ( ( Im ` A ) = _pi \/ -u A e. ran log ) ) )
55 44 54 mpbid 
 |-  ( A e. ran log -> ( ( Im ` A ) = _pi \/ -u A e. ran log ) )
56 55 orcanai 
 |-  ( ( A e. ran log /\ -. ( Im ` A ) = _pi ) -> -u A e. ran log )