brbtwn2 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > brbtwn2		Structured version Unicode version

Theorem brbtwn2 23884

Description: Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.)

**Assertion**
Ref	Expression
brbtwn2	$/\$ $/\$ $/\$

Distinct variable groups:

Proof of Theorem brbtwn2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		brbtwn 23878	. 2 $/\$ $/\$
2		fveere 23880	. . . . . . . . . 10 $/\$
3	2	3ad2antl2 1159	. . . . . . . . 9 $/\$ $/\$ $/\$
4		fveere 23880	. . . . . . . . . 10 $/\$
5	4	3ad2antl3 1160	. . . . . . . . 9 $/\$ $/\$ $/\$
6	3, 5	jca 532	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7		resubcl 9879	. . . . . . . . . . . . . . 15 $/\$
8	7	3adant3 1016	. . . . . . . . . . . . . 14 $/\$ $/\$
9	8	recnd 9618	. . . . . . . . . . . . 13 $/\$ $/\$
10	9	sqvald 12271	. . . . . . . . . . . 12 $/\$ $/\$
11	10	oveq2d 6298	. . . . . . . . . . 11 $/\$ $/\$
12		0re 9592	. . . . . . . . . . . . . . . 16
13		1re 9591	. . . . . . . . . . . . . . . 16
14	12, 13	elicc2i 11586	. . . . . . . . . . . . . . 15 $/\$ $/\$
15	14	simp1bi 1011	. . . . . . . . . . . . . 14
16	15	recnd 9618	. . . . . . . . . . . . 13
17	16	3ad2ant3 1019	. . . . . . . . . . . 12 $/\$ $/\$
18		resubcl 9879	. . . . . . . . . . . . . . . 16 $/\$
19	13, 15, 18	sylancr 663	. . . . . . . . . . . . . . 15
20	19	3ad2ant3 1019	. . . . . . . . . . . . . 14 $/\$ $/\$
21	20	recnd 9618	. . . . . . . . . . . . 13 $/\$ $/\$
22	21	negcld 9913	. . . . . . . . . . . 12 $/\$ $/\$
23	17, 9, 22, 9	mul4d 9787	. . . . . . . . . . 11 $/\$ $/\$
24		recn 9578	. . . . . . . . . . . . . . 15
25	24	3ad2ant1 1017	. . . . . . . . . . . . . 14 $/\$ $/\$
26		recn 9578	. . . . . . . . . . . . . . 15
27	26	3ad2ant2 1018	. . . . . . . . . . . . . 14 $/\$ $/\$
28	17, 25, 27	subdid 10008	. . . . . . . . . . . . 13 $/\$ $/\$
29		ax-1cn 9546	. . . . . . . . . . . . . . . . 17
30		subdir 9987	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
31	29, 30	mp3an1 1311	. . . . . . . . . . . . . . . 16 $/\$
32	21, 25, 31	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$
33		nncan 9844	. . . . . . . . . . . . . . . . 17 $/\$
34	29, 17, 33	sylancr 663	. . . . . . . . . . . . . . . 16 $/\$ $/\$
35	34	oveq1d 6297	. . . . . . . . . . . . . . 15 $/\$ $/\$
36	25	mulid2d 9610	. . . . . . . . . . . . . . . 16 $/\$ $/\$
37	36	oveq1d 6297	. . . . . . . . . . . . . . 15 $/\$ $/\$
38	32, 35, 37	3eqtr3d 2516	. . . . . . . . . . . . . 14 $/\$ $/\$
39	38	oveq1d 6297	. . . . . . . . . . . . 13 $/\$ $/\$
40		simp1 996	. . . . . . . . . . . . . . . 16 $/\$ $/\$
41	20, 40	remulcld 9620	. . . . . . . . . . . . . . 15 $/\$ $/\$
42	41	recnd 9618	. . . . . . . . . . . . . 14 $/\$ $/\$
43	15	3ad2ant3 1019	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44		simp2 997	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	43, 44	remulcld 9620	. . . . . . . . . . . . . . 15 $/\$ $/\$
46	45	recnd 9618	. . . . . . . . . . . . . 14 $/\$ $/\$
47	25, 42, 46	subsub4d 9957	. . . . . . . . . . . . 13 $/\$ $/\$
48	28, 39, 47	3eqtrd 2512	. . . . . . . . . . . 12 $/\$ $/\$
49	21, 9	mulneg1d 10005	. . . . . . . . . . . . 13 $/\$ $/\$
50	21, 25, 27	subdid 10008	. . . . . . . . . . . . . . 15 $/\$ $/\$
51		subdir 9987	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
52	29, 51	mp3an1 1311	. . . . . . . . . . . . . . . . . 18 $/\$
53	17, 27, 52	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
54	27	mulid2d 9610	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
55	54	oveq1d 6297	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
56	53, 55	eqtrd 2508	. . . . . . . . . . . . . . . 16 $/\$ $/\$
57	56	oveq2d 6298	. . . . . . . . . . . . . . 15 $/\$ $/\$
58	42, 27, 46	subsub3d 9956	. . . . . . . . . . . . . . 15 $/\$ $/\$
59	50, 57, 58	3eqtrd 2512	. . . . . . . . . . . . . 14 $/\$ $/\$
60	59	negeqd 9810	. . . . . . . . . . . . 13 $/\$ $/\$
61	41, 45	readdcld 9619	. . . . . . . . . . . . . . 15 $/\$ $/\$
62	61	recnd 9618	. . . . . . . . . . . . . 14 $/\$ $/\$
63	62, 27	negsubdi2d 9942	. . . . . . . . . . . . 13 $/\$ $/\$
64	49, 60, 63	3eqtrd 2512	. . . . . . . . . . . 12 $/\$ $/\$
65	48, 64	oveq12d 6300	. . . . . . . . . . 11 $/\$ $/\$
66	11, 23, 65	3eqtr2rd 2515	. . . . . . . . . 10 $/\$ $/\$
67	17, 21	mulneg2d 10006	. . . . . . . . . . . . 13 $/\$ $/\$
68	67	oveq1d 6297	. . . . . . . . . . . 12 $/\$ $/\$
69	43, 20	remulcld 9620	. . . . . . . . . . . . . 14 $/\$ $/\$
70	69	recnd 9618	. . . . . . . . . . . . 13 $/\$ $/\$
71	8	resqcld 12300	. . . . . . . . . . . . . 14 $/\$ $/\$
72	71	recnd 9618	. . . . . . . . . . . . 13 $/\$ $/\$
73	70, 72	mulneg1d 10005	. . . . . . . . . . . 12 $/\$ $/\$
74	68, 73	eqtrd 2508	. . . . . . . . . . 11 $/\$ $/\$
75	14	simp2bi 1012	. . . . . . . . . . . . . . 15
76	14	simp3bi 1013	. . . . . . . . . . . . . . . 16
77		subge0 10061	. . . . . . . . . . . . . . . . 17 $/\$
78	13, 15, 77	sylancr 663	. . . . . . . . . . . . . . . 16
79	76, 78	mpbird 232	. . . . . . . . . . . . . . 15
80	15, 19, 75, 79	mulge0d 10125	. . . . . . . . . . . . . 14
81	80	3ad2ant3 1019	. . . . . . . . . . . . 13 $/\$ $/\$
82	8	sqge0d 12301	. . . . . . . . . . . . 13 $/\$ $/\$
83	69, 71, 81, 82	mulge0d 10125	. . . . . . . . . . . 12 $/\$ $/\$
84	69, 71	remulcld 9620	. . . . . . . . . . . . 13 $/\$ $/\$
85	84	le0neg2d 10121	. . . . . . . . . . . 12 $/\$ $/\$
86	83, 85	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$
87	74, 86	eqbrtrd 4467	. . . . . . . . . 10 $/\$ $/\$
88	66, 87	eqbrtrd 4467	. . . . . . . . 9 $/\$ $/\$
89	88	3expa 1196	. . . . . . . 8 $/\$ $/\$
90	6, 89	sylan 471	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
91	90	an32s 802	. . . . . 6 $/\$ $/\$ $/\$ $/\$
92	91	ralrimiva 2878	. . . . 5 $/\$ $/\$ $/\$
93		fveecn 23881	. . . . . . . . . . . 12 $/\$
94		fveecn 23881	. . . . . . . . . . . 12 $/\$
95	93, 94	anim12i 566	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
96	95	anandirs 829	. . . . . . . . . 10 $/\$ $/\$ $/\$
97		fveecn 23881	. . . . . . . . . . . 12 $/\$
98		fveecn 23881	. . . . . . . . . . . 12 $/\$
99	97, 98	anim12i 566	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
100	99	anandirs 829	. . . . . . . . . 10 $/\$ $/\$ $/\$
101	96, 100	anim12dan 835	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	3adantl1 1152	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		subcl 9815	. . . . . . . . . . . . . 14 $/\$
104	103	3ad2ant1 1017	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
105		subcl 9815	. . . . . . . . . . . . . . 15 $/\$
106	105	ancoms 453	. . . . . . . . . . . . . 14 $/\$
107	106	3ad2ant2 1018	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	104, 107	mulcomd 9613	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
109		simp2r 1023	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
110		simp2l 1022	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
111		simp1l 1020	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
112		simp1r 1021	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
113		mulsub2 9996	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
114	109, 110, 111, 112, 113	syl22anc 1229	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
115	108, 114	eqtrd 2508	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 6298	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
117		simp3 998	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
118		subcl 9815	. . . . . . . . . . . . . 14 $/\$
119	29, 118	mpan 670	. . . . . . . . . . . . 13
120	119	3ad2ant3 1019	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
121	117, 120, 104, 107	mul4d 9787	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
122	117, 111, 112	subdid 10008	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
123	120, 111, 31	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	29, 33	mpan 670	. . . . . . . . . . . . . . . . 17
125	124	3ad2ant3 1019	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
126	125	oveq1d 6297	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
127	111	mulid2d 9610	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
128	127	oveq1d 6297	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
129	123, 126, 128	3eqtr3d 2516	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
130	129	oveq1d 6297	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
131	120, 111	mulcld 9612	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
132	117, 112	mulcld 9612	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
133	111, 131, 132	subsub4d 9957	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
134	122, 130, 133	3eqtrd 2512	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
135	120, 109, 110	subdid 10008	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
136		subdir 9987	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
137	29, 136	mp3an1 1311	. . . . . . . . . . . . . . . . 17 $/\$
138	117, 109, 137	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
139	109	mulid2d 9610	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
140	139	oveq1d 6297	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	138, 140	eqtrd 2508	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
142	141	oveq1d 6297	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
143	135, 142	eqtrd 2508	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
144	117, 109	mulcld 9612	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
145	120, 110	mulcld 9612	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
146	109, 144, 145	sub32d 9958	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
147	109, 145, 144	subsub4d 9957	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
148	143, 146, 147	3eqtrd 2512	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
149	134, 148	oveq12d 6300	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
150	121, 149	eqtrd 2508	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
151		subcl 9815	. . . . . . . . . . . . 13 $/\$
152	151	3ad2ant2 1018	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
153		subcl 9815	. . . . . . . . . . . . . 14 $/\$
154	153	ancoms 453	. . . . . . . . . . . . 13 $/\$
155	154	3ad2ant1 1017	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
156	117, 120, 152, 155	mul4d 9787	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
157	117, 110, 109	subdid 10008	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
158		subdir 9987	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
159	29, 158	mp3an1 1311	. . . . . . . . . . . . . . . 16 $/\$
160	120, 110, 159	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
161	125	oveq1d 6297	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
162	110	mulid2d 9610	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
163	162	oveq1d 6297	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3rd 2517	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
165	164	oveq1d 6297	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
166	110, 145, 144	subsub4d 9957	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
167	157, 165, 166	3eqtr2d 2514	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
168	120, 112, 111	subdid 10008	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
169	117, 112, 52	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
170	112	mulid2d 9610	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
171	170	oveq1d 6297	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
172	169, 171	eqtrd 2508	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
173	172	oveq1d 6297	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
174	112, 132, 131	sub32d 9958	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
175	112, 131, 132	subsub4d 9957	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
176	174, 175	eqtrd 2508	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
177	168, 173, 176	3eqtrd 2512	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
178	167, 177	oveq12d 6300	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
179	156, 178	eqtrd 2508	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
180	116, 150, 179	3eqtr3d 2516	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
181	180	3expa 1196	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
182	102, 16, 181	syl2an 477	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
183	182	an32s 802	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
184	183	ralrimivva 2885	. . . . 5 $/\$ $/\$ $/\$
185		fveq2 5864	. . . . . . . . . . 11
186		fveq2 5864	. . . . . . . . . . . . 13
187	186	oveq2d 6298	. . . . . . . . . . . 12
188		fveq2 5864	. . . . . . . . . . . . 13
189	188	oveq2d 6298	. . . . . . . . . . . 12
190	187, 189	oveq12d 6300	. . . . . . . . . . 11
191	185, 190	eqeq12d 2489	. . . . . . . . . 10
192	191	rspccva 3213	. . . . . . . . 9 $/\$
193		oveq2 6290	. . . . . . . . . . 11
194		oveq2 6290	. . . . . . . . . . 11
195	193, 194	oveq12d 6300	. . . . . . . . . 10
196	195	breq1d 4457	. . . . . . . . 9
197	192, 196	syl 16	. . . . . . . 8 $/\$
198	197	ralbidva 2900	. . . . . . 7
199		fveq2 5864	. . . . . . . . . . . 12
200		fveq2 5864	. . . . . . . . . . . . . 14
201	200	oveq2d 6298	. . . . . . . . . . . . 13
202		fveq2 5864	. . . . . . . . . . . . . 14
203	202	oveq2d 6298	. . . . . . . . . . . . 13
204	201, 203	oveq12d 6300	. . . . . . . . . . . 12
205	199, 204	eqeq12d 2489	. . . . . . . . . . 11
206	205	rspccva 3213	. . . . . . . . . 10 $/\$
207		oveq2 6290	. . . . . . . . . . . 12
208	193, 207	oveqan12d 6301	. . . . . . . . . . 11 $/\$
209		oveq2 6290	. . . . . . . . . . . 12
210	209, 194	oveqan12rd 6302	. . . . . . . . . . 11 $/\$
211	208, 210	eqeq12d 2489	. . . . . . . . . 10 $/\$
212	192, 206, 211	syl2an 477	. . . . . . . . 9 $/\$ $/\$ $/\$
213	212	anandis 828	. . . . . . . 8 $/\$ $/\$
214	213	2ralbidva 2906	. . . . . . 7
215	198, 214	anbi12d 710	. . . . . 6 $/\$ $/\$
216	215	biimprcd 225	. . . . 5 $/\$ $/\$
217	92, 184, 216	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$