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 )