brbtwn2 - Metamath Proof Explorer

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

Theorem brbtwn2 24625

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 24619	. 2 $/\$ $/\$
2		fveere 24621	. . . . . . . . . 10 $/\$
3	2	3ad2antl2 1160	. . . . . . . . 9 $/\$ $/\$ $/\$
4		fveere 24621	. . . . . . . . . 10 $/\$
5	4	3ad2antl3 1161	. . . . . . . . 9 $/\$ $/\$ $/\$
6	3, 5	jca 530	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7		resubcl 9919	. . . . . . . . . . . . . . 15 $/\$
8	7	3adant3 1017	. . . . . . . . . . . . . 14 $/\$ $/\$
9	8	recnd 9652	. . . . . . . . . . . . 13 $/\$ $/\$
10	9	sqvald 12351	. . . . . . . . . . . 12 $/\$ $/\$
11	10	oveq2d 6294	. . . . . . . . . . 11 $/\$ $/\$
12		0re 9626	. . . . . . . . . . . . . . . 16
13		1re 9625	. . . . . . . . . . . . . . . 16
14	12, 13	elicc2i 11644	. . . . . . . . . . . . . . 15 $/\$ $/\$
15	14	simp1bi 1012	. . . . . . . . . . . . . 14
16	15	recnd 9652	. . . . . . . . . . . . 13
17	16	3ad2ant3 1020	. . . . . . . . . . . 12 $/\$ $/\$
18		resubcl 9919	. . . . . . . . . . . . . . . 16 $/\$
19	13, 15, 18	sylancr 661	. . . . . . . . . . . . . . 15
20	19	3ad2ant3 1020	. . . . . . . . . . . . . 14 $/\$ $/\$
21	20	recnd 9652	. . . . . . . . . . . . 13 $/\$ $/\$
22	21	negcld 9954	. . . . . . . . . . . 12 $/\$ $/\$
23	17, 9, 22, 9	mul4d 9826	. . . . . . . . . . 11 $/\$ $/\$
24		recn 9612	. . . . . . . . . . . . . . 15
25	24	3ad2ant1 1018	. . . . . . . . . . . . . 14 $/\$ $/\$
26		recn 9612	. . . . . . . . . . . . . . 15
27	26	3ad2ant2 1019	. . . . . . . . . . . . . 14 $/\$ $/\$
28	17, 25, 27	subdid 10053	. . . . . . . . . . . . 13 $/\$ $/\$
29		ax-1cn 9580	. . . . . . . . . . . . . . . . 17
30		subdir 10032	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
31	29, 30	mp3an1 1313	. . . . . . . . . . . . . . . 16 $/\$
32	21, 25, 31	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ $/\$
33		nncan 9884	. . . . . . . . . . . . . . . . 17 $/\$
34	29, 17, 33	sylancr 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$
35	34	oveq1d 6293	. . . . . . . . . . . . . . 15 $/\$ $/\$
36	25	mulid2d 9644	. . . . . . . . . . . . . . . 16 $/\$ $/\$
37	36	oveq1d 6293	. . . . . . . . . . . . . . 15 $/\$ $/\$
38	32, 35, 37	3eqtr3d 2451	. . . . . . . . . . . . . 14 $/\$ $/\$
39	38	oveq1d 6293	. . . . . . . . . . . . 13 $/\$ $/\$
40		simp1 997	. . . . . . . . . . . . . . . 16 $/\$ $/\$
41	20, 40	remulcld 9654	. . . . . . . . . . . . . . 15 $/\$ $/\$
42	41	recnd 9652	. . . . . . . . . . . . . 14 $/\$ $/\$
43	15	3ad2ant3 1020	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44		simp2 998	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	43, 44	remulcld 9654	. . . . . . . . . . . . . . 15 $/\$ $/\$
46	45	recnd 9652	. . . . . . . . . . . . . 14 $/\$ $/\$
47	25, 42, 46	subsub4d 9998	. . . . . . . . . . . . 13 $/\$ $/\$
48	28, 39, 47	3eqtrd 2447	. . . . . . . . . . . 12 $/\$ $/\$
49	21, 9	mulneg1d 10050	. . . . . . . . . . . . 13 $/\$ $/\$
50	21, 25, 27	subdid 10053	. . . . . . . . . . . . . . 15 $/\$ $/\$
51		subdir 10032	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
52	29, 51	mp3an1 1313	. . . . . . . . . . . . . . . . . 18 $/\$
53	17, 27, 52	syl2anc 659	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
54	27	mulid2d 9644	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
55	54	oveq1d 6293	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
56	53, 55	eqtrd 2443	. . . . . . . . . . . . . . . 16 $/\$ $/\$
57	56	oveq2d 6294	. . . . . . . . . . . . . . 15 $/\$ $/\$
58	42, 27, 46	subsub3d 9997	. . . . . . . . . . . . . . 15 $/\$ $/\$
59	50, 57, 58	3eqtrd 2447	. . . . . . . . . . . . . 14 $/\$ $/\$
60	59	negeqd 9850	. . . . . . . . . . . . 13 $/\$ $/\$
61	41, 45	readdcld 9653	. . . . . . . . . . . . . . 15 $/\$ $/\$
62	61	recnd 9652	. . . . . . . . . . . . . 14 $/\$ $/\$
63	62, 27	negsubdi2d 9983	. . . . . . . . . . . . 13 $/\$ $/\$
64	49, 60, 63	3eqtrd 2447	. . . . . . . . . . . 12 $/\$ $/\$
65	48, 64	oveq12d 6296	. . . . . . . . . . 11 $/\$ $/\$
66	11, 23, 65	3eqtr2rd 2450	. . . . . . . . . 10 $/\$ $/\$
67	17, 21	mulneg2d 10051	. . . . . . . . . . . . 13 $/\$ $/\$
68	67	oveq1d 6293	. . . . . . . . . . . 12 $/\$ $/\$
69	43, 20	remulcld 9654	. . . . . . . . . . . . . 14 $/\$ $/\$
70	69	recnd 9652	. . . . . . . . . . . . 13 $/\$ $/\$
71	8	resqcld 12380	. . . . . . . . . . . . . 14 $/\$ $/\$
72	71	recnd 9652	. . . . . . . . . . . . 13 $/\$ $/\$
73	70, 72	mulneg1d 10050	. . . . . . . . . . . 12 $/\$ $/\$
74	68, 73	eqtrd 2443	. . . . . . . . . . 11 $/\$ $/\$
75	14	simp2bi 1013	. . . . . . . . . . . . . . 15
76	14	simp3bi 1014	. . . . . . . . . . . . . . . 16
77		subge0 10106	. . . . . . . . . . . . . . . . 17 $/\$
78	13, 15, 77	sylancr 661	. . . . . . . . . . . . . . . 16
79	76, 78	mpbird 232	. . . . . . . . . . . . . . 15
80	15, 19, 75, 79	mulge0d 10169	. . . . . . . . . . . . . 14
81	80	3ad2ant3 1020	. . . . . . . . . . . . 13 $/\$ $/\$
82	8	sqge0d 12381	. . . . . . . . . . . . 13 $/\$ $/\$
83	69, 71, 81, 82	mulge0d 10169	. . . . . . . . . . . 12 $/\$ $/\$
84	69, 71	remulcld 9654	. . . . . . . . . . . . 13 $/\$ $/\$
85	84	le0neg2d 10165	. . . . . . . . . . . 12 $/\$ $/\$
86	83, 85	mpbid 210	. . . . . . . . . . 11 $/\$ $/\$
87	74, 86	eqbrtrd 4415	. . . . . . . . . 10 $/\$ $/\$
88	66, 87	eqbrtrd 4415	. . . . . . . . 9 $/\$ $/\$
89	88	3expa 1197	. . . . . . . 8 $/\$ $/\$
90	6, 89	sylan 469	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
91	90	an32s 805	. . . . . 6 $/\$ $/\$ $/\$ $/\$
92	91	ralrimiva 2818	. . . . 5 $/\$ $/\$ $/\$
93		fveecn 24622	. . . . . . . . . . . 12 $/\$
94		fveecn 24622	. . . . . . . . . . . 12 $/\$
95	93, 94	anim12i 564	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
96	95	anandirs 832	. . . . . . . . . 10 $/\$ $/\$ $/\$
97		fveecn 24622	. . . . . . . . . . . 12 $/\$
98		fveecn 24622	. . . . . . . . . . . 12 $/\$
99	97, 98	anim12i 564	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
100	99	anandirs 832	. . . . . . . . . 10 $/\$ $/\$ $/\$
101	96, 100	anim12dan 838	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	3adantl1 1153	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		subcl 9855	. . . . . . . . . . . . . 14 $/\$
104	103	3ad2ant1 1018	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
105		subcl 9855	. . . . . . . . . . . . . . 15 $/\$
106	105	ancoms 451	. . . . . . . . . . . . . 14 $/\$
107	106	3ad2ant2 1019	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	104, 107	mulcomd 9647	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
109		simp2r 1024	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
110		simp2l 1023	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
111		simp1l 1021	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
112		simp1r 1022	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
113		mulsub2 10041	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
114	109, 110, 111, 112, 113	syl22anc 1231	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
115	108, 114	eqtrd 2443	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 6294	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
117		simp3 999	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
118		subcl 9855	. . . . . . . . . . . . . 14 $/\$
119	29, 118	mpan 668	. . . . . . . . . . . . 13
120	119	3ad2ant3 1020	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
121	117, 120, 104, 107	mul4d 9826	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
122	117, 111, 112	subdid 10053	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
123	120, 111, 31	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	29, 33	mpan 668	. . . . . . . . . . . . . . . . 17
125	124	3ad2ant3 1020	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
126	125	oveq1d 6293	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
127	111	mulid2d 9644	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
128	127	oveq1d 6293	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
129	123, 126, 128	3eqtr3d 2451	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
130	129	oveq1d 6293	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
131	120, 111	mulcld 9646	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
132	117, 112	mulcld 9646	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
133	111, 131, 132	subsub4d 9998	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
134	122, 130, 133	3eqtrd 2447	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
135	120, 109, 110	subdid 10053	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
136		subdir 10032	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
137	29, 136	mp3an1 1313	. . . . . . . . . . . . . . . . 17 $/\$
138	117, 109, 137	syl2anc 659	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
139	109	mulid2d 9644	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
140	139	oveq1d 6293	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	138, 140	eqtrd 2443	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
142	141	oveq1d 6293	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
143	135, 142	eqtrd 2443	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
144	117, 109	mulcld 9646	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
145	120, 110	mulcld 9646	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
146	109, 144, 145	sub32d 9999	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
147	109, 145, 144	subsub4d 9998	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
148	143, 146, 147	3eqtrd 2447	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
149	134, 148	oveq12d 6296	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
150	121, 149	eqtrd 2443	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
151		subcl 9855	. . . . . . . . . . . . 13 $/\$
152	151	3ad2ant2 1019	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
153		subcl 9855	. . . . . . . . . . . . . 14 $/\$
154	153	ancoms 451	. . . . . . . . . . . . 13 $/\$
155	154	3ad2ant1 1018	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
156	117, 120, 152, 155	mul4d 9826	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
157	117, 110, 109	subdid 10053	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
158		subdir 10032	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
159	29, 158	mp3an1 1313	. . . . . . . . . . . . . . . 16 $/\$
160	120, 110, 159	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
161	125	oveq1d 6293	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
162	110	mulid2d 9644	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
163	162	oveq1d 6293	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3rd 2452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
165	164	oveq1d 6293	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
166	110, 145, 144	subsub4d 9998	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
167	157, 165, 166	3eqtr2d 2449	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
168	120, 112, 111	subdid 10053	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
169	117, 112, 52	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
170	112	mulid2d 9644	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
171	170	oveq1d 6293	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
172	169, 171	eqtrd 2443	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
173	172	oveq1d 6293	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
174	112, 132, 131	sub32d 9999	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
175	112, 131, 132	subsub4d 9998	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
176	174, 175	eqtrd 2443	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
177	168, 173, 176	3eqtrd 2447	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
178	167, 177	oveq12d 6296	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
179	156, 178	eqtrd 2443	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
180	116, 150, 179	3eqtr3d 2451	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
181	180	3expa 1197	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
182	102, 16, 181	syl2an 475	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
183	182	an32s 805	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
184	183	ralrimivva 2825	. . . . 5 $/\$ $/\$ $/\$
185		fveq2 5849	. . . . . . . . . . 11
186		fveq2 5849	. . . . . . . . . . . . 13
187	186	oveq2d 6294	. . . . . . . . . . . 12
188		fveq2 5849	. . . . . . . . . . . . 13
189	188	oveq2d 6294	. . . . . . . . . . . 12
190	187, 189	oveq12d 6296	. . . . . . . . . . 11
191	185, 190	eqeq12d 2424	. . . . . . . . . 10
192	191	rspccva 3159	. . . . . . . . 9 $/\$
193		oveq2 6286	. . . . . . . . . . 11
194		oveq2 6286	. . . . . . . . . . 11
195	193, 194	oveq12d 6296	. . . . . . . . . 10
196	195	breq1d 4405	. . . . . . . . 9
197	192, 196	syl 17	. . . . . . . 8 $/\$
198	197	ralbidva 2840	. . . . . . 7
199		fveq2 5849	. . . . . . . . . . . 12
200		fveq2 5849	. . . . . . . . . . . . . 14
201	200	oveq2d 6294	. . . . . . . . . . . . 13
202		fveq2 5849	. . . . . . . . . . . . . 14
203	202	oveq2d 6294	. . . . . . . . . . . . 13
204	201, 203	oveq12d 6296	. . . . . . . . . . . 12
205	199, 204	eqeq12d 2424	. . . . . . . . . . 11
206	205	rspccva 3159	. . . . . . . . . 10 $/\$
207		oveq2 6286	. . . . . . . . . . . 12
208	193, 207	oveqan12d 6297	. . . . . . . . . . 11 $/\$
209		oveq2 6286	. . . . . . . . . . . 12
210	209, 194	oveqan12rd 6298	. . . . . . . . . . 11 $/\$
211	208, 210	eqeq12d 2424	. . . . . . . . . 10 $/\$
212	192, 206, 211	syl2an 475	. . . . . . . . 9 $/\$ $/\$ $/\$
213	212	anandis 831	. . . . . . . 8 $/\$ $/\$
214	213	2ralbidva 2846	. . . . . . 7
215	198, 214	anbi12d 709	. . . . . 6 $/\$ $/\$
216	215	biimprcd 225	. . . . 5 $/\$ $/\$
217	92, 184, 216	syl2anc 659	. . . 4 $/\$ $/\$ $/\$ $/\$