Metamath Proof Explorer

Theorem cnpart

Description: The specification of restriction to the right half-plane partitions the complex plane without 0 into two disjoint pieces, which are related by a reflection about the origin (under the map x |-> -u x ). (Contributed by Mario Carneiro, 8-Jul-2013)

Ref Expression
Assertion cnpart 
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) <-> -. ( 0 <_ ( Re ` -u A ) /\ ( _i x. -u A ) e/ RR+ ) ) )

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( -u ( _i x. A ) e/ RR+ <-> -. -u ( _i x. A ) e. RR+ )
2 simpr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( Re ` A ) = 0 )
3 0le0 
 |-  0 <_ 0
4 2 3 eqbrtrdi 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( Re ` A ) <_ 0 )
5 4 biantrurd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( -u ( _i x. A ) e/ RR+ <-> ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) ) )
6 1 5 bitr3id 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( -. -u ( _i x. A ) e. RR+ <-> ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) ) )
7 6 con1bid 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( -. ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) <-> -u ( _i x. A ) e. RR+ ) )
8 ax-icn 
 |-  _i e. CC
9 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
10 8 9 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
11 reim0b 
 |-  ( ( _i x. A ) e. CC -> ( ( _i x. A ) e. RR <-> ( Im ` ( _i x. A ) ) = 0 ) )
12 10 11 syl 
 |-  ( A e. CC -> ( ( _i x. A ) e. RR <-> ( Im ` ( _i x. A ) ) = 0 ) )
13 imre 
 |-  ( ( _i x. A ) e. CC -> ( Im ` ( _i x. A ) ) = ( Re ` ( -u _i x. ( _i x. A ) ) ) )
14 10 13 syl 
 |-  ( A e. CC -> ( Im ` ( _i x. A ) ) = ( Re ` ( -u _i x. ( _i x. A ) ) ) )
15 ine0 
 |-  _i =/= 0
16 divrec2 
 |-  ( ( ( _i x. A ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( ( _i x. A ) / _i ) = ( ( 1 / _i ) x. ( _i x. A ) ) )
17 8 15 16 mp3an23 
 |-  ( ( _i x. A ) e. CC -> ( ( _i x. A ) / _i ) = ( ( 1 / _i ) x. ( _i x. A ) ) )
18 10 17 syl 
 |-  ( A e. CC -> ( ( _i x. A ) / _i ) = ( ( 1 / _i ) x. ( _i x. A ) ) )
19 irec 
 |-  ( 1 / _i ) = -u _i
20 19 oveq1i 
 |-  ( ( 1 / _i ) x. ( _i x. A ) ) = ( -u _i x. ( _i x. A ) )
21 18 20 eqtrdi 
 |-  ( A e. CC -> ( ( _i x. A ) / _i ) = ( -u _i x. ( _i x. A ) ) )
22 divcan3 
 |-  ( ( A e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( ( _i x. A ) / _i ) = A )
23 8 15 22 mp3an23 
 |-  ( A e. CC -> ( ( _i x. A ) / _i ) = A )
24 21 23 eqtr3d 
 |-  ( A e. CC -> ( -u _i x. ( _i x. A ) ) = A )
25 24 fveq2d 
 |-  ( A e. CC -> ( Re ` ( -u _i x. ( _i x. A ) ) ) = ( Re ` A ) )
26 14 25 eqtrd 
 |-  ( A e. CC -> ( Im ` ( _i x. A ) ) = ( Re ` A ) )
27 26 eqeq1d 
 |-  ( A e. CC -> ( ( Im ` ( _i x. A ) ) = 0 <-> ( Re ` A ) = 0 ) )
28 12 27 bitrd 
 |-  ( A e. CC -> ( ( _i x. A ) e. RR <-> ( Re ` A ) = 0 ) )
29 28 biimpar 
 |-  ( ( A e. CC /\ ( Re ` A ) = 0 ) -> ( _i x. A ) e. RR )
30 29 adantlr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( _i x. A ) e. RR )
31 mulne0 
 |-  ( ( ( _i e. CC /\ _i =/= 0 ) /\ ( A e. CC /\ A =/= 0 ) ) -> ( _i x. A ) =/= 0 )
32 8 15 31 mpanl12 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( _i x. A ) =/= 0 )
33 32 adantr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( _i x. A ) =/= 0 )
34 rpneg 
 |-  ( ( ( _i x. A ) e. RR /\ ( _i x. A ) =/= 0 ) -> ( ( _i x. A ) e. RR+ <-> -. -u ( _i x. A ) e. RR+ ) )
35 30 33 34 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( ( _i x. A ) e. RR+ <-> -. -u ( _i x. A ) e. RR+ ) )
36 35 con2bid 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( -u ( _i x. A ) e. RR+ <-> -. ( _i x. A ) e. RR+ ) )
37 df-nel 
 |-  ( ( _i x. A ) e/ RR+ <-> -. ( _i x. A ) e. RR+ )
38 36 37 bitr4di 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( -u ( _i x. A ) e. RR+ <-> ( _i x. A ) e/ RR+ ) )
39 3 2 breqtrrid 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> 0 <_ ( Re ` A ) )
40 39 biantrurd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( ( _i x. A ) e/ RR+ <-> ( 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) ) )
41 7 38 40 3bitrrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) = 0 ) -> ( ( 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) <-> -. ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) ) )
42 28 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( _i x. A ) e. RR <-> ( Re ` A ) = 0 ) )
43 42 necon3bbid 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -. ( _i x. A ) e. RR <-> ( Re ` A ) =/= 0 ) )
44 43 biimpar 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> -. ( _i x. A ) e. RR )
45 rpre 
 |-  ( ( _i x. A ) e. RR+ -> ( _i x. A ) e. RR )
46 44 45 nsyl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> -. ( _i x. A ) e. RR+ )
47 46 37 sylibr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( _i x. A ) e/ RR+ )
48 47 biantrud 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( 0 <_ ( Re ` A ) <-> ( 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) ) )
49 simpr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( Re ` A ) =/= 0 )
50 49 biantrud 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( 0 <_ ( Re ` A ) <-> ( 0 <_ ( Re ` A ) /\ ( Re ` A ) =/= 0 ) ) )
51 0re 
 |-  0 e. RR
52 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
53 ltlen 
 |-  ( ( 0 e. RR /\ ( Re ` A ) e. RR ) -> ( 0 < ( Re ` A ) <-> ( 0 <_ ( Re ` A ) /\ ( Re ` A ) =/= 0 ) ) )
54 ltnle 
 |-  ( ( 0 e. RR /\ ( Re ` A ) e. RR ) -> ( 0 < ( Re ` A ) <-> -. ( Re ` A ) <_ 0 ) )
55 53 54 bitr3d 
 |-  ( ( 0 e. RR /\ ( Re ` A ) e. RR ) -> ( ( 0 <_ ( Re ` A ) /\ ( Re ` A ) =/= 0 ) <-> -. ( Re ` A ) <_ 0 ) )
56 51 52 55 sylancr 
 |-  ( A e. CC -> ( ( 0 <_ ( Re ` A ) /\ ( Re ` A ) =/= 0 ) <-> -. ( Re ` A ) <_ 0 ) )
57 56 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( ( 0 <_ ( Re ` A ) /\ ( Re ` A ) =/= 0 ) <-> -. ( Re ` A ) <_ 0 ) )
58 50 57 bitrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( 0 <_ ( Re ` A ) <-> -. ( Re ` A ) <_ 0 ) )
59 48 58 bitr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( ( 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) <-> -. ( Re ` A ) <_ 0 ) )
60 renegcl 
 |-  ( -u ( _i x. A ) e. RR -> -u -u ( _i x. A ) e. RR )
61 10 negnegd 
 |-  ( A e. CC -> -u -u ( _i x. A ) = ( _i x. A ) )
62 61 eleq1d 
 |-  ( A e. CC -> ( -u -u ( _i x. A ) e. RR <-> ( _i x. A ) e. RR ) )
63 62 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( -u -u ( _i x. A ) e. RR <-> ( _i x. A ) e. RR ) )
64 60 63 imbitrid 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( -u ( _i x. A ) e. RR -> ( _i x. A ) e. RR ) )
65 44 64 mtod 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> -. -u ( _i x. A ) e. RR )
66 rpre 
 |-  ( -u ( _i x. A ) e. RR+ -> -u ( _i x. A ) e. RR )
67 65 66 nsyl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> -. -u ( _i x. A ) e. RR+ )
68 67 1 sylibr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> -u ( _i x. A ) e/ RR+ )
69 68 biantrud 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( ( Re ` A ) <_ 0 <-> ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) ) )
70 69 notbid 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( -. ( Re ` A ) <_ 0 <-> -. ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) ) )
71 59 70 bitrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( Re ` A ) =/= 0 ) -> ( ( 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) <-> -. ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) ) )
72 41 71 pm2.61dane 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) <-> -. ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) ) )
73 reneg 
 |-  ( A e. CC -> ( Re ` -u A ) = -u ( Re ` A ) )
74 73 breq2d 
 |-  ( A e. CC -> ( 0 <_ ( Re ` -u A ) <-> 0 <_ -u ( Re ` A ) ) )
75 52 le0neg1d 
 |-  ( A e. CC -> ( ( Re ` A ) <_ 0 <-> 0 <_ -u ( Re ` A ) ) )
76 74 75 bitr4d 
 |-  ( A e. CC -> ( 0 <_ ( Re ` -u A ) <-> ( Re ` A ) <_ 0 ) )
77 mulneg2 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) )
78 8 77 mpan 
 |-  ( A e. CC -> ( _i x. -u A ) = -u ( _i x. A ) )
79 neleq1 
 |-  ( ( _i x. -u A ) = -u ( _i x. A ) -> ( ( _i x. -u A ) e/ RR+ <-> -u ( _i x. A ) e/ RR+ ) )
80 78 79 syl 
 |-  ( A e. CC -> ( ( _i x. -u A ) e/ RR+ <-> -u ( _i x. A ) e/ RR+ ) )
81 76 80 anbi12d 
 |-  ( A e. CC -> ( ( 0 <_ ( Re ` -u A ) /\ ( _i x. -u A ) e/ RR+ ) <-> ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) ) )
82 81 notbid 
 |-  ( A e. CC -> ( -. ( 0 <_ ( Re ` -u A ) /\ ( _i x. -u A ) e/ RR+ ) <-> -. ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) ) )
83 82 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( -. ( 0 <_ ( Re ` -u A ) /\ ( _i x. -u A ) e/ RR+ ) <-> -. ( ( Re ` A ) <_ 0 /\ -u ( _i x. A ) e/ RR+ ) ) )
84 72 83 bitr4d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) <-> -. ( 0 <_ ( Re ` -u A ) /\ ( _i x. -u A ) e/ RR+ ) ) )