colinearalg - Metamath Proof Explorer

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

Theorem colinearalg 25019

Description: An algebraic characterization of colinearity. Note the similarity to brbtwn2 25014. (Contributed by Scott Fenton, 24-Jun-2013.)

**Assertion**
Ref	Expression
colinearalg	$/\$ $/\$ $\/$ $\/$

Distinct variable groups:

Proof of Theorem colinearalg Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		brbtwn2 25014	. . 3 $/\$ $/\$ $/\$
2		brbtwn2 25014	. . . . 5 $/\$ $/\$ $/\$
3	2	3comr 1239	. . . 4 $/\$ $/\$ $/\$
4		colinearalglem3 25017	. . . . . 6 $/\$ $/\$
5	4	3comr 1239	. . . . 5 $/\$ $/\$
6	5	anbi2d 718	. . . 4 $/\$ $/\$ $/\$ $/\$
7	3, 6	bitrd 261	. . 3 $/\$ $/\$ $/\$
8		brbtwn2 25014	. . . . 5 $/\$ $/\$ $/\$
9		colinearalglem2 25016	. . . . . 6 $/\$ $/\$
10	9	anbi2d 718	. . . . 5 $/\$ $/\$ $/\$ $/\$
11	8, 10	bitrd 261	. . . 4 $/\$ $/\$ $/\$
12	11	3coml 1238	. . 3 $/\$ $/\$ $/\$
13	1, 7, 12	3orbi123d 1364	. 2 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
14		fveecn 25011	. . . . . . . . . . . . 13 $/\$
15		fveecn 25011	. . . . . . . . . . . . 13 $/\$
16		subid 9913	. . . . . . . . . . . . . . . 16
17	16	oveq2d 6324	. . . . . . . . . . . . . . 15
18	17	adantl 473	. . . . . . . . . . . . . 14 $/\$
19		subcl 9894	. . . . . . . . . . . . . . 15 $/\$
20	19	mul01d 9850	. . . . . . . . . . . . . 14 $/\$
21	18, 20	eqtrd 2505	. . . . . . . . . . . . 13 $/\$
22	14, 15, 21	syl2an 485	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
23	22	anandirs 847	. . . . . . . . . . 11 $/\$ $/\$
24		0le0 10721	. . . . . . . . . . 11
25	23, 24	syl6eqbr 4433	. . . . . . . . . 10 $/\$ $/\$
26	25	ralrimiva 2809	. . . . . . . . 9 $/\$
27	26	3adant1 1048	. . . . . . . 8 $/\$ $/\$
28		fveq1 5878	. . . . . . . . . . . 12
29	28	oveq2d 6324	. . . . . . . . . . 11
30	28	oveq2d 6324	. . . . . . . . . . 11
31	29, 30	oveq12d 6326	. . . . . . . . . 10
32	31	breq1d 4405	. . . . . . . . 9
33	32	ralbidv 2829	. . . . . . . 8
34	27, 33	syl5ibcom 228	. . . . . . 7 $/\$ $/\$
35		3mix1 1199	. . . . . . 7 $\/$ $\/$
36	34, 35	syl6 33	. . . . . 6 $/\$ $/\$ $\/$ $\/$
37	36	a1dd 46	. . . . 5 $/\$ $/\$ $\/$ $\/$
38		simp3 1032	. . . . . . . . 9 $/\$ $/\$
39		simp1 1030	. . . . . . . . 9 $/\$ $/\$
40		eqeefv 25012	. . . . . . . . 9 $/\$
41	38, 39, 40	syl2anc 673	. . . . . . . 8 $/\$ $/\$
42	41	necon3abid 2679	. . . . . . 7 $/\$ $/\$
43		df-ne 2643	. . . . . . . . 9
44	43	rexbii 2881	. . . . . . . 8
45		rexnal 2836	. . . . . . . 8
46	44, 45	bitr2i 258	. . . . . . 7
47	42, 46	syl6bb 269	. . . . . 6 $/\$ $/\$
48		ralcom 2937	. . . . . . . 8
49		fveq2 5879	. . . . . . . . . . . . . . 15
50		fveq2 5879	. . . . . . . . . . . . . . 15
51	49, 50	oveq12d 6326	. . . . . . . . . . . . . 14
52	51	oveq2d 6324	. . . . . . . . . . . . 13
53		fveq2 5879	. . . . . . . . . . . . . . 15
54	53, 50	oveq12d 6326	. . . . . . . . . . . . . 14
55	54	oveq1d 6323	. . . . . . . . . . . . 13
56	52, 55	eqeq12d 2486	. . . . . . . . . . . 12
57	56	ralbidv 2829	. . . . . . . . . . 11
58	57	rspcv 3132	. . . . . . . . . 10
59	58	ad2antrl 742	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
60		fveere 25010	. . . . . . . . . . . . . 14 $/\$
61	60	3ad2antl1 1192	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
62		fveere 25010	. . . . . . . . . . . . . 14 $/\$
63	62	3ad2antl2 1193	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
64		fveere 25010	. . . . . . . . . . . . . 14 $/\$
65	64	3ad2antl3 1194	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
66	61, 63, 65	3jca 1210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
67	66	anim1i 578	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68	67	anasss 659	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		fveecn 25011	. . . . . . . . . . . . . . . 16 $/\$
70	69	3ad2antl1 1192	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
71	14	3ad2antl2 1193	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
72	15	3ad2antl3 1194	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
73	70, 71, 72	3jca 1210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
74	73	adantlr 729	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		recn 9647	. . . . . . . . . . . . . . . 16
76		recn 9647	. . . . . . . . . . . . . . . 16
77		recn 9647	. . . . . . . . . . . . . . . 16
78	75, 76, 77	3anim123i 1215	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
79	78	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
80	79	ad2antlr 741	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		simplrr 779	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82		eqcom 2478	. . . . . . . . . . . . . 14
83		simp12 1061	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84		simp11 1060	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		simp22 1064	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86		simp21 1063	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
87	85, 86	subcld 10005	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88		simp23 1065	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89	88, 86	subcld 10005	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90		simpr3 1038	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
91		simpr1 1036	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
92	90, 91	subeq0ad 10015	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
93	92	necon3bid 2687	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
94	93	biimp3ar 1398	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95	87, 89, 94	divcld 10405	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		simp13 1062	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	96, 84	subcld 10005	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98	95, 97	mulcld 9681	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		subadd2 9899	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
100	99	bicomd 206	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	83, 84, 98, 100	syl3anc 1292	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	87, 97, 89, 94	div23d 10442	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	102	eqeq2d 2481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104		eqcom 2478	. . . . . . . . . . . . . . . 16
105	87, 97	mulcld 9681	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106	83, 84	subcld 10005	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	105, 89, 106, 94	divmuld 10427	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108	89, 106	mulcomd 9682	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109	108	eqeq1d 2473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
110	107, 109	bitrd 261	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
111	104, 110	syl5bb 265	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
112	101, 103, 111	3bitr2d 289	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113	82, 112	syl5bb 265	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	74, 80, 81, 113	syl3anc 1292	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	114	ralbidva 2828	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		3simpb 1028	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
117		simpl2 1034	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
118		simpl1 1033	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
119	117, 118	resubcld 10068	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
120		simpl3 1035	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
121	120, 118	resubcld 10068	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
122		simp3 1032	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
123	122	recnd 9687	. . . . . . . . . . . . . . . 16 $/\$ $/\$
124	75	3ad2ant1 1051	. . . . . . . . . . . . . . . 16 $/\$ $/\$
125	123, 124	subeq0ad 10015	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	125	necon3bid 2687	. . . . . . . . . . . . . 14 $/\$ $/\$
127	126	biimpar 493	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
128	119, 121, 127	redivcld 10457	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
129		colinearalglem4 25018	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $\/$
130		oveq1 6315	. . . . . . . . . . . . . . . . . 18
131	130	oveq1d 6323	. . . . . . . . . . . . . . . . 17
132	131	breq1d 4405	. . . . . . . . . . . . . . . 16
133	132	ralimi 2796	. . . . . . . . . . . . . . 15
134		ralbi 2908	. . . . . . . . . . . . . . 15
135	133, 134	syl 17	. . . . . . . . . . . . . 14
136		oveq2 6316	. . . . . . . . . . . . . . . . . 18
137		oveq2 6316	. . . . . . . . . . . . . . . . . 18
138	136, 137	oveq12d 6326	. . . . . . . . . . . . . . . . 17
139	138	breq1d 4405	. . . . . . . . . . . . . . . 16
140	139	ralimi 2796	. . . . . . . . . . . . . . 15
141		ralbi 2908	. . . . . . . . . . . . . . 15
142	140, 141	syl 17	. . . . . . . . . . . . . 14
143		oveq1 6315	. . . . . . . . . . . . . . . . . 18
144	143	oveq2d 6324	. . . . . . . . . . . . . . . . 17
145	144	breq1d 4405	. . . . . . . . . . . . . . . 16
146	145	ralimi 2796	. . . . . . . . . . . . . . 15
147		ralbi 2908	. . . . . . . . . . . . . . 15
148	146, 147	syl 17	. . . . . . . . . . . . . 14
149	135, 142, 148	3orbi123d 1364	. . . . . . . . . . . . 13 $\/$ $\/$ $\/$ $\/$
150	129, 149	syl5ibrcom 230	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $\/$
151	116, 128, 150	syl2an 485	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
152	115, 151	sylbird 243	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$