brbtwn2 - Metamath Proof Explorer

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

Theorem brbtwn2 25014

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 25008	. 2 $/\$ $/\$
2		fveere 25010	. . . . . . . . . 10 $/\$
3	2	3ad2antl2 1193	. . . . . . . . 9 $/\$ $/\$ $/\$
4		fveere 25010	. . . . . . . . . 10 $/\$
5	4	3ad2antl3 1194	. . . . . . . . 9 $/\$ $/\$ $/\$
6	3, 5	jca 541	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7		resubcl 9958	. . . . . . . . . . . . . . 15 $/\$
8	7	3adant3 1050	. . . . . . . . . . . . . 14 $/\$ $/\$
9	8	recnd 9687	. . . . . . . . . . . . 13 $/\$ $/\$
10	9	sqvald 12451	. . . . . . . . . . . 12 $/\$ $/\$
11	10	oveq2d 6324	. . . . . . . . . . 11 $/\$ $/\$
12		0re 9661	. . . . . . . . . . . . . . . 16
13		1re 9660	. . . . . . . . . . . . . . . 16
14	12, 13	elicc2i 11725	. . . . . . . . . . . . . . 15 $/\$ $/\$
15	14	simp1bi 1045	. . . . . . . . . . . . . 14
16	15	recnd 9687	. . . . . . . . . . . . 13
17	16	3ad2ant3 1053	. . . . . . . . . . . 12 $/\$ $/\$
18		resubcl 9958	. . . . . . . . . . . . . . . 16 $/\$
19	13, 15, 18	sylancr 676	. . . . . . . . . . . . . . 15
20	19	3ad2ant3 1053	. . . . . . . . . . . . . 14 $/\$ $/\$
21	20	recnd 9687	. . . . . . . . . . . . 13 $/\$ $/\$
22	21	negcld 9992	. . . . . . . . . . . 12 $/\$ $/\$
23	17, 9, 22, 9	mul4d 9863	. . . . . . . . . . 11 $/\$ $/\$
24		recn 9647	. . . . . . . . . . . . . . 15
25	24	3ad2ant1 1051	. . . . . . . . . . . . . 14 $/\$ $/\$
26		recn 9647	. . . . . . . . . . . . . . 15
27	26	3ad2ant2 1052	. . . . . . . . . . . . . 14 $/\$ $/\$
28	17, 25, 27	subdid 10095	. . . . . . . . . . . . 13 $/\$ $/\$
29		ax-1cn 9615	. . . . . . . . . . . . . . . . 17
30		subdir 10074	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
31	29, 30	mp3an1 1377	. . . . . . . . . . . . . . . 16 $/\$
32	21, 25, 31	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$
33		nncan 9923	. . . . . . . . . . . . . . . . 17 $/\$
34	29, 17, 33	sylancr 676	. . . . . . . . . . . . . . . 16 $/\$ $/\$
35	34	oveq1d 6323	. . . . . . . . . . . . . . 15 $/\$ $/\$
36	25	mulid2d 9679	. . . . . . . . . . . . . . . 16 $/\$ $/\$
37	36	oveq1d 6323	. . . . . . . . . . . . . . 15 $/\$ $/\$
38	32, 35, 37	3eqtr3d 2513	. . . . . . . . . . . . . 14 $/\$ $/\$
39	38	oveq1d 6323	. . . . . . . . . . . . 13 $/\$ $/\$
40		simp1 1030	. . . . . . . . . . . . . . . 16 $/\$ $/\$
41	20, 40	remulcld 9689	. . . . . . . . . . . . . . 15 $/\$ $/\$
42	41	recnd 9687	. . . . . . . . . . . . . 14 $/\$ $/\$
43	15	3ad2ant3 1053	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44		simp2 1031	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	43, 44	remulcld 9689	. . . . . . . . . . . . . . 15 $/\$ $/\$
46	45	recnd 9687	. . . . . . . . . . . . . 14 $/\$ $/\$
47	25, 42, 46	subsub4d 10036	. . . . . . . . . . . . 13 $/\$ $/\$
48	28, 39, 47	3eqtrd 2509	. . . . . . . . . . . 12 $/\$ $/\$
49	21, 9	mulneg1d 10092	. . . . . . . . . . . . 13 $/\$ $/\$
50	21, 25, 27	subdid 10095	. . . . . . . . . . . . . . 15 $/\$ $/\$
51		subdir 10074	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
52	29, 51	mp3an1 1377	. . . . . . . . . . . . . . . . . 18 $/\$
53	17, 27, 52	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
54	27	mulid2d 9679	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
55	54	oveq1d 6323	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
56	53, 55	eqtrd 2505	. . . . . . . . . . . . . . . 16 $/\$ $/\$
57	56	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$ $/\$
58	42, 27, 46	subsub3d 10035	. . . . . . . . . . . . . . 15 $/\$ $/\$
59	50, 57, 58	3eqtrd 2509	. . . . . . . . . . . . . 14 $/\$ $/\$
60	59	negeqd 9889	. . . . . . . . . . . . 13 $/\$ $/\$
61	41, 45	readdcld 9688	. . . . . . . . . . . . . . 15 $/\$ $/\$
62	61	recnd 9687	. . . . . . . . . . . . . 14 $/\$ $/\$
63	62, 27	negsubdi2d 10021	. . . . . . . . . . . . 13 $/\$ $/\$
64	49, 60, 63	3eqtrd 2509	. . . . . . . . . . . 12 $/\$ $/\$
65	48, 64	oveq12d 6326	. . . . . . . . . . 11 $/\$ $/\$
66	11, 23, 65	3eqtr2rd 2512	. . . . . . . . . 10 $/\$ $/\$
67	17, 21	mulneg2d 10093	. . . . . . . . . . . . 13 $/\$ $/\$
68	67	oveq1d 6323	. . . . . . . . . . . 12 $/\$ $/\$
69	43, 20	remulcld 9689	. . . . . . . . . . . . . 14 $/\$ $/\$
70	69	recnd 9687	. . . . . . . . . . . . 13 $/\$ $/\$
71	8	resqcld 12480	. . . . . . . . . . . . . 14 $/\$ $/\$
72	71	recnd 9687	. . . . . . . . . . . . 13 $/\$ $/\$
73	70, 72	mulneg1d 10092	. . . . . . . . . . . 12 $/\$ $/\$
74	68, 73	eqtrd 2505	. . . . . . . . . . 11 $/\$ $/\$
75	14	simp2bi 1046	. . . . . . . . . . . . . . 15
76	14	simp3bi 1047	. . . . . . . . . . . . . . . 16
77		subge0 10148	. . . . . . . . . . . . . . . . 17 $/\$
78	13, 15, 77	sylancr 676	. . . . . . . . . . . . . . . 16
79	76, 78	mpbird 240	. . . . . . . . . . . . . . 15
80	15, 19, 75, 79	mulge0d 10211	. . . . . . . . . . . . . 14
81	80	3ad2ant3 1053	. . . . . . . . . . . . 13 $/\$ $/\$
82	8	sqge0d 12481	. . . . . . . . . . . . 13 $/\$ $/\$
83	69, 71, 81, 82	mulge0d 10211	. . . . . . . . . . . 12 $/\$ $/\$
84	69, 71	remulcld 9689	. . . . . . . . . . . . 13 $/\$ $/\$
85	84	le0neg2d 10207	. . . . . . . . . . . 12 $/\$ $/\$
86	83, 85	mpbid 215	. . . . . . . . . . 11 $/\$ $/\$
87	74, 86	eqbrtrd 4416	. . . . . . . . . 10 $/\$ $/\$
88	66, 87	eqbrtrd 4416	. . . . . . . . 9 $/\$ $/\$
89	88	3expa 1231	. . . . . . . 8 $/\$ $/\$
90	6, 89	sylan 479	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
91	90	an32s 821	. . . . . 6 $/\$ $/\$ $/\$ $/\$
92	91	ralrimiva 2809	. . . . 5 $/\$ $/\$ $/\$
93		fveecn 25011	. . . . . . . . . . . 12 $/\$
94		fveecn 25011	. . . . . . . . . . . 12 $/\$
95	93, 94	anim12i 576	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
96	95	anandirs 847	. . . . . . . . . 10 $/\$ $/\$ $/\$
97		fveecn 25011	. . . . . . . . . . . 12 $/\$
98		fveecn 25011	. . . . . . . . . . . 12 $/\$
99	97, 98	anim12i 576	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
100	99	anandirs 847	. . . . . . . . . 10 $/\$ $/\$ $/\$
101	96, 100	anim12dan 855	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	3adantl1 1186	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		subcl 9894	. . . . . . . . . . . . . 14 $/\$
104	103	3ad2ant1 1051	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
105		subcl 9894	. . . . . . . . . . . . . . 15 $/\$
106	105	ancoms 460	. . . . . . . . . . . . . 14 $/\$
107	106	3ad2ant2 1052	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	104, 107	mulcomd 9682	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
109		simp2r 1057	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
110		simp2l 1056	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
111		simp1l 1054	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
112		simp1r 1055	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
113		mulsub2 10083	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
114	109, 110, 111, 112, 113	syl22anc 1293	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
115	108, 114	eqtrd 2505	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 6324	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
117		simp3 1032	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
118		subcl 9894	. . . . . . . . . . . . . 14 $/\$
119	29, 118	mpan 684	. . . . . . . . . . . . 13
120	119	3ad2ant3 1053	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
121	117, 120, 104, 107	mul4d 9863	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
122	117, 111, 112	subdid 10095	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
123	120, 111, 31	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	29, 33	mpan 684	. . . . . . . . . . . . . . . . 17
125	124	3ad2ant3 1053	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
126	125	oveq1d 6323	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
127	111	mulid2d 9679	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
128	127	oveq1d 6323	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
129	123, 126, 128	3eqtr3d 2513	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
130	129	oveq1d 6323	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
131	120, 111	mulcld 9681	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
132	117, 112	mulcld 9681	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
133	111, 131, 132	subsub4d 10036	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
134	122, 130, 133	3eqtrd 2509	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
135	120, 109, 110	subdid 10095	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
136		subdir 10074	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
137	29, 136	mp3an1 1377	. . . . . . . . . . . . . . . . 17 $/\$
138	117, 109, 137	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
139	109	mulid2d 9679	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
140	139	oveq1d 6323	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	138, 140	eqtrd 2505	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
142	141	oveq1d 6323	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
143	135, 142	eqtrd 2505	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
144	117, 109	mulcld 9681	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
145	120, 110	mulcld 9681	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
146	109, 144, 145	sub32d 10037	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
147	109, 145, 144	subsub4d 10036	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
148	143, 146, 147	3eqtrd 2509	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
149	134, 148	oveq12d 6326	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
150	121, 149	eqtrd 2505	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
151		subcl 9894	. . . . . . . . . . . . 13 $/\$
152	151	3ad2ant2 1052	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
153		subcl 9894	. . . . . . . . . . . . . 14 $/\$
154	153	ancoms 460	. . . . . . . . . . . . 13 $/\$
155	154	3ad2ant1 1051	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
156	117, 120, 152, 155	mul4d 9863	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
157	117, 110, 109	subdid 10095	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
158		subdir 10074	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
159	29, 158	mp3an1 1377	. . . . . . . . . . . . . . . 16 $/\$
160	120, 110, 159	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
161	125	oveq1d 6323	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
162	110	mulid2d 9679	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
163	162	oveq1d 6323	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3rd 2514	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
165	164	oveq1d 6323	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
166	110, 145, 144	subsub4d 10036	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
167	157, 165, 166	3eqtr2d 2511	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
168	120, 112, 111	subdid 10095	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
169	117, 112, 52	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
170	112	mulid2d 9679	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
171	170	oveq1d 6323	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
172	169, 171	eqtrd 2505	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
173	172	oveq1d 6323	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
174	112, 132, 131	sub32d 10037	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
175	112, 131, 132	subsub4d 10036	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
176	174, 175	eqtrd 2505	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
177	168, 173, 176	3eqtrd 2509	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
178	167, 177	oveq12d 6326	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
179	156, 178	eqtrd 2505	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
180	116, 150, 179	3eqtr3d 2513	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
181	180	3expa 1231	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
182	102, 16, 181	syl2an 485	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
183	182	an32s 821	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
184	183	ralrimivva 2814	. . . . 5 $/\$ $/\$ $/\$
185		fveq2 5879	. . . . . . . . . . 11
186		fveq2 5879	. . . . . . . . . . . . 13
187	186	oveq2d 6324	. . . . . . . . . . . 12
188		fveq2 5879	. . . . . . . . . . . . 13
189	188	oveq2d 6324	. . . . . . . . . . . 12
190	187, 189	oveq12d 6326	. . . . . . . . . . 11
191	185, 190	eqeq12d 2486	. . . . . . . . . 10
192	191	rspccva 3135	. . . . . . . . 9 $/\$
193		oveq2 6316	. . . . . . . . . . 11
194		oveq2 6316	. . . . . . . . . . 11
195	193, 194	oveq12d 6326	. . . . . . . . . 10
196	195	breq1d 4405	. . . . . . . . 9
197	192, 196	syl 17	. . . . . . . 8 $/\$
198	197	ralbidva 2828	. . . . . . 7
199		fveq2 5879	. . . . . . . . . . . 12
200		fveq2 5879	. . . . . . . . . . . . . 14
201	200	oveq2d 6324	. . . . . . . . . . . . 13
202		fveq2 5879	. . . . . . . . . . . . . 14
203	202	oveq2d 6324	. . . . . . . . . . . . 13
204	201, 203	oveq12d 6326	. . . . . . . . . . . 12
205	199, 204	eqeq12d 2486	. . . . . . . . . . 11
206	205	rspccva 3135	. . . . . . . . . 10 $/\$
207		oveq2 6316	. . . . . . . . . . . 12
208	193, 207	oveqan12d 6327	. . . . . . . . . . 11 $/\$
209		oveq2 6316	. . . . . . . . . . . 12
210	209, 194	oveqan12rd 6328	. . . . . . . . . . 11 $/\$
211	208, 210	eqeq12d 2486	. . . . . . . . . 10 $/\$
212	192, 206, 211	syl2an 485	. . . . . . . . 9 $/\$ $/\$ $/\$
213	212	anandis 846	. . . . . . . 8 $/\$ $/\$
214	213	2ralbidva 2831	. . . . . . 7
215	198, 214	anbi12d 725	. . . . . 6 $/\$ $/\$
216	215	biimprcd 233	. . . . 5 $/\$ $/\$
217	92, 184, 216	syl2anc 673	. . . 4 $/\$ $/\$ $/\$ $/\$