brbtwn2 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > brbtwn2		Unicode version

Theorem brbtwn2 25748

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 25742	. 2 $/\$ $/\$
2		fveere 25744	. . . . . . . . . 10 $/\$
3	2	3ad2antl2 1120	. . . . . . . . 9 $/\$ $/\$ $/\$
4		fveere 25744	. . . . . . . . . 10 $/\$
5	4	3ad2antl3 1121	. . . . . . . . 9 $/\$ $/\$ $/\$
6	3, 5	jca 519	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7		resubcl 9321	. . . . . . . . . . . . . . 15 $/\$
8	7	3adant3 977	. . . . . . . . . . . . . 14 $/\$ $/\$
9	8	recnd 9070	. . . . . . . . . . . . 13 $/\$ $/\$
10	9	sqvald 11475	. . . . . . . . . . . 12 $/\$ $/\$
11	10	oveq2d 6056	. . . . . . . . . . 11 $/\$ $/\$
12		0re 9047	. . . . . . . . . . . . . . . 16
13		1re 9046	. . . . . . . . . . . . . . . 16
14	12, 13	elicc2i 10932	. . . . . . . . . . . . . . 15 $/\$ $/\$
15	14	simp1bi 972	. . . . . . . . . . . . . 14
16	15	recnd 9070	. . . . . . . . . . . . 13
17	16	3ad2ant3 980	. . . . . . . . . . . 12 $/\$ $/\$
18		resubcl 9321	. . . . . . . . . . . . . . . 16 $/\$
19	13, 15, 18	sylancr 645	. . . . . . . . . . . . . . 15
20	19	3ad2ant3 980	. . . . . . . . . . . . . 14 $/\$ $/\$
21	20	recnd 9070	. . . . . . . . . . . . 13 $/\$ $/\$
22	21	negcld 9354	. . . . . . . . . . . 12 $/\$ $/\$
23	17, 9, 22, 9	mul4d 9234	. . . . . . . . . . 11 $/\$ $/\$
24		recn 9036	. . . . . . . . . . . . . . 15
25	24	3ad2ant1 978	. . . . . . . . . . . . . 14 $/\$ $/\$
26		recn 9036	. . . . . . . . . . . . . . 15
27	26	3ad2ant2 979	. . . . . . . . . . . . . 14 $/\$ $/\$
28	17, 25, 27	subdid 9445	. . . . . . . . . . . . 13 $/\$ $/\$
29		ax-1cn 9004	. . . . . . . . . . . . . . . . 17
30		subdir 9424	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
31	29, 30	mp3an1 1266	. . . . . . . . . . . . . . . 16 $/\$
32	21, 25, 31	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ $/\$
33		nncan 9286	. . . . . . . . . . . . . . . . 17 $/\$
34	29, 17, 33	sylancr 645	. . . . . . . . . . . . . . . 16 $/\$ $/\$
35	34	oveq1d 6055	. . . . . . . . . . . . . . 15 $/\$ $/\$
36	25	mulid2d 9062	. . . . . . . . . . . . . . . 16 $/\$ $/\$
37	36	oveq1d 6055	. . . . . . . . . . . . . . 15 $/\$ $/\$
38	32, 35, 37	3eqtr3d 2444	. . . . . . . . . . . . . 14 $/\$ $/\$
39	38	oveq1d 6055	. . . . . . . . . . . . 13 $/\$ $/\$
40		simp1 957	. . . . . . . . . . . . . . . 16 $/\$ $/\$
41	20, 40	remulcld 9072	. . . . . . . . . . . . . . 15 $/\$ $/\$
42	41	recnd 9070	. . . . . . . . . . . . . 14 $/\$ $/\$
43	15	3ad2ant3 980	. . . . . . . . . . . . . . . 16 $/\$ $/\$
44		simp2 958	. . . . . . . . . . . . . . . 16 $/\$ $/\$
45	43, 44	remulcld 9072	. . . . . . . . . . . . . . 15 $/\$ $/\$
46	45	recnd 9070	. . . . . . . . . . . . . 14 $/\$ $/\$
47	25, 42, 46	subsub4d 9398	. . . . . . . . . . . . 13 $/\$ $/\$
48	28, 39, 47	3eqtrd 2440	. . . . . . . . . . . 12 $/\$ $/\$
49	21, 9	mulneg1d 9442	. . . . . . . . . . . . 13 $/\$ $/\$
50	21, 25, 27	subdid 9445	. . . . . . . . . . . . . . 15 $/\$ $/\$
51		subdir 9424	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
52	29, 51	mp3an1 1266	. . . . . . . . . . . . . . . . . 18 $/\$
53	17, 27, 52	syl2anc 643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
54	27	mulid2d 9062	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
55	54	oveq1d 6055	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
56	53, 55	eqtrd 2436	. . . . . . . . . . . . . . . 16 $/\$ $/\$
57	56	oveq2d 6056	. . . . . . . . . . . . . . 15 $/\$ $/\$
58	42, 27, 46	subsub3d 9397	. . . . . . . . . . . . . . 15 $/\$ $/\$
59	50, 57, 58	3eqtrd 2440	. . . . . . . . . . . . . 14 $/\$ $/\$
60	59	negeqd 9256	. . . . . . . . . . . . 13 $/\$ $/\$
61	41, 45	readdcld 9071	. . . . . . . . . . . . . . 15 $/\$ $/\$
62	61	recnd 9070	. . . . . . . . . . . . . 14 $/\$ $/\$
63	62, 27	negsubdi2d 9383	. . . . . . . . . . . . 13 $/\$ $/\$
64	49, 60, 63	3eqtrd 2440	. . . . . . . . . . . 12 $/\$ $/\$
65	48, 64	oveq12d 6058	. . . . . . . . . . 11 $/\$ $/\$
66	11, 23, 65	3eqtr2rd 2443	. . . . . . . . . 10 $/\$ $/\$
67	17, 21	mulneg2d 9443	. . . . . . . . . . . . 13 $/\$ $/\$
68	67	oveq1d 6055	. . . . . . . . . . . 12 $/\$ $/\$
69	43, 20	remulcld 9072	. . . . . . . . . . . . . 14 $/\$ $/\$
70	69	recnd 9070	. . . . . . . . . . . . 13 $/\$ $/\$
71	8	resqcld 11504	. . . . . . . . . . . . . 14 $/\$ $/\$
72	71	recnd 9070	. . . . . . . . . . . . 13 $/\$ $/\$
73	70, 72	mulneg1d 9442	. . . . . . . . . . . 12 $/\$ $/\$
74	68, 73	eqtrd 2436	. . . . . . . . . . 11 $/\$ $/\$
75	14	simp2bi 973	. . . . . . . . . . . . . . 15
76	14	simp3bi 974	. . . . . . . . . . . . . . . 16
77		subge0 9497	. . . . . . . . . . . . . . . . 17 $/\$
78	13, 15, 77	sylancr 645	. . . . . . . . . . . . . . . 16
79	76, 78	mpbird 224	. . . . . . . . . . . . . . 15
80	15, 19, 75, 79	mulge0d 9559	. . . . . . . . . . . . . 14
81	80	3ad2ant3 980	. . . . . . . . . . . . 13 $/\$ $/\$
82	8	sqge0d 11505	. . . . . . . . . . . . 13 $/\$ $/\$
83	69, 71, 81, 82	mulge0d 9559	. . . . . . . . . . . 12 $/\$ $/\$
84	69, 71	remulcld 9072	. . . . . . . . . . . . 13 $/\$ $/\$
85	84	le0neg2d 9555	. . . . . . . . . . . 12 $/\$ $/\$
86	83, 85	mpbid 202	. . . . . . . . . . 11 $/\$ $/\$
87	74, 86	eqbrtrd 4192	. . . . . . . . . 10 $/\$ $/\$
88	66, 87	eqbrtrd 4192	. . . . . . . . 9 $/\$ $/\$
89	88	3expa 1153	. . . . . . . 8 $/\$ $/\$
90	6, 89	sylan 458	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
91	90	an32s 780	. . . . . 6 $/\$ $/\$ $/\$ $/\$
92	91	ralrimiva 2749	. . . . 5 $/\$ $/\$ $/\$
93		fveecn 25745	. . . . . . . . . . . 12 $/\$
94		fveecn 25745	. . . . . . . . . . . 12 $/\$
95	93, 94	anim12i 550	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
96	95	anandirs 805	. . . . . . . . . 10 $/\$ $/\$ $/\$
97		fveecn 25745	. . . . . . . . . . . 12 $/\$
98		fveecn 25745	. . . . . . . . . . . 12 $/\$
99	97, 98	anim12i 550	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
100	99	anandirs 805	. . . . . . . . . 10 $/\$ $/\$ $/\$
101	96, 100	anim12dan 811	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	101	3adantl1 1113	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103		subcl 9261	. . . . . . . . . . . . . 14 $/\$
104	103	3ad2ant1 978	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
105		subcl 9261	. . . . . . . . . . . . . . 15 $/\$
106	105	ancoms 440	. . . . . . . . . . . . . 14 $/\$
107	106	3ad2ant2 979	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
108	104, 107	mulcomd 9065	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
109		simp2r 984	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
110		simp2l 983	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
111		simp1l 981	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
112		simp1r 982	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
113		mulsub2 9433	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
114	109, 110, 111, 112, 113	syl22anc 1185	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
115	108, 114	eqtrd 2436	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 6056	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
117		simp3 959	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
118		subcl 9261	. . . . . . . . . . . . . 14 $/\$
119	29, 118	mpan 652	. . . . . . . . . . . . 13
120	119	3ad2ant3 980	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
121	117, 120, 104, 107	mul4d 9234	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
122	117, 111, 112	subdid 9445	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
123	120, 111, 31	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	29, 33	mpan 652	. . . . . . . . . . . . . . . . 17
125	124	3ad2ant3 980	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
126	125	oveq1d 6055	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
127	111	mulid2d 9062	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
128	127	oveq1d 6055	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
129	123, 126, 128	3eqtr3d 2444	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
130	129	oveq1d 6055	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
131	120, 111	mulcld 9064	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
132	117, 112	mulcld 9064	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
133	111, 131, 132	subsub4d 9398	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
134	122, 130, 133	3eqtrd 2440	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
135	120, 109, 110	subdid 9445	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
136		subdir 9424	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
137	29, 136	mp3an1 1266	. . . . . . . . . . . . . . . . 17 $/\$
138	117, 109, 137	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
139	109	mulid2d 9062	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
140	139	oveq1d 6055	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
141	138, 140	eqtrd 2436	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
142	141	oveq1d 6055	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
143	135, 142	eqtrd 2436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
144	117, 109	mulcld 9064	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
145	120, 110	mulcld 9064	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
146	109, 144, 145	sub32d 9399	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
147	109, 145, 144	subsub4d 9398	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
148	143, 146, 147	3eqtrd 2440	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
149	134, 148	oveq12d 6058	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
150	121, 149	eqtrd 2436	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
151		subcl 9261	. . . . . . . . . . . . 13 $/\$
152	151	3ad2ant2 979	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
153		subcl 9261	. . . . . . . . . . . . . 14 $/\$
154	153	ancoms 440	. . . . . . . . . . . . 13 $/\$
155	154	3ad2ant1 978	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
156	117, 120, 152, 155	mul4d 9234	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
157	117, 110, 109	subdid 9445	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
158		subdir 9424	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
159	29, 158	mp3an1 1266	. . . . . . . . . . . . . . . 16 $/\$
160	120, 110, 159	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
161	125	oveq1d 6055	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
162	110	mulid2d 9062	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
163	162	oveq1d 6055	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3rd 2445	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
165	164	oveq1d 6055	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
166	110, 145, 144	subsub4d 9398	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
167	157, 165, 166	3eqtr2d 2442	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
168	120, 112, 111	subdid 9445	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
169	117, 112, 52	syl2anc 643	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
170	112	mulid2d 9062	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
171	170	oveq1d 6055	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
172	169, 171	eqtrd 2436	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
173	172	oveq1d 6055	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
174	112, 132, 131	sub32d 9399	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
175	112, 131, 132	subsub4d 9398	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
176	174, 175	eqtrd 2436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
177	168, 173, 176	3eqtrd 2440	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
178	167, 177	oveq12d 6058	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
179	156, 178	eqtrd 2436	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
180	116, 150, 179	3eqtr3d 2444	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
181	180	3expa 1153	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
182	102, 16, 181	syl2an 464	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
183	182	an32s 780	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
184	183	ralrimivva 2758	. . . . 5 $/\$ $/\$ $/\$
185		fveq2 5687	. . . . . . . . . . 11
186		fveq2 5687	. . . . . . . . . . . . 13
187	186	oveq2d 6056	. . . . . . . . . . . 12
188		fveq2 5687	. . . . . . . . . . . . 13
189	188	oveq2d 6056	. . . . . . . . . . . 12
190	187, 189	oveq12d 6058	. . . . . . . . . . 11
191	185, 190	eqeq12d 2418	. . . . . . . . . 10
192	191	rspccva 3011	. . . . . . . . 9 $/\$
193		oveq2 6048	. . . . . . . . . . 11
194		oveq2 6048	. . . . . . . . . . 11
195	193, 194	oveq12d 6058	. . . . . . . . . 10
196	195	breq1d 4182	. . . . . . . . 9
197	192, 196	syl 16	. . . . . . . 8 $/\$
198	197	ralbidva 2682	. . . . . . 7
199		fveq2 5687	. . . . . . . . . . . 12
200		fveq2 5687	. . . . . . . . . . . . . 14
201	200	oveq2d 6056	. . . . . . . . . . . . 13
202		fveq2 5687	. . . . . . . . . . . . . 14
203	202	oveq2d 6056	. . . . . . . . . . . . 13
204	201, 203	oveq12d 6058	. . . . . . . . . . . 12
205	199, 204	eqeq12d 2418	. . . . . . . . . . 11
206	205	rspccva 3011	. . . . . . . . . 10 $/\$
207		oveq2 6048	. . . . . . . . . . . 12
208	193, 207	oveqan12d 6059	. . . . . . . . . . 11 $/\$
209		oveq2 6048	. . . . . . . . . . . 12
210	209, 194	oveqan12rd 6060	. . . . . . . . . . 11 $/\$
211	208, 210	eqeq12d 2418	. . . . . . . . . 10 $/\$
212	192, 206, 211	syl2an 464	. . . . . . . . 9 $/\$ $/\$ $/\$
213	212	anandis 804	. . . . . . . 8 $/\$ $/\$
214	213	2ralbidva 2706	. . . . . . 7
215	198, 214	anbi12d 692	. . . . . 6 $/\$ $/\$
216	215	biimprcd 217	. . . . 5 $/\$ $/\$
217	92, 184, 216	syl2anc 643	. . . 4 $/\$ $/\$ $/\$ $/\$