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	imbitrid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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 · - 𝐴 ) ∉ ℝ+ ) ) )