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 · - 𝐴 ) ∉ ℝ+ ) ) )