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 \in ℂ \land A \neq 0) \to ((0 \leq ℜ (A) \land i A \notin ℝ^{+}) \leftrightarrow \neg (0 \leq ℜ (- A) \land i (- A) \notin ℝ^{+}))$

Proof

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

Metamath Proof Explorer

Theorem cnpart

Proof