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 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ↔ ¬ ( 0 ≤ ( ℜ ‘ - 𝐴 ) ∧ ( i · - 𝐴 ) ∉ ℝ+ ) ) )

Proof

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