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+ ) ) )

Metamath Proof Explorer

Theorem cnpart

Proof