Theorem axeuclid 24930

Description: Euclid's axiom. Take an angle B A C and a point D between B and C. Now, if you extend the segment A D to a point T, then T lies between two points x and y that lie on the angle. Axiom A10 of [Schwabhauser] p. 13. (Contributed by Scott Fenton, 9-Sep-2013.)

Assertion

Ref	Expression
axeuclid	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , T >. /\ D Btwn <. B , C >. /\ A =/= D ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) ( B Btwn <. A , x >. /\ C Btwn <. A , y >. /\ T Btwn <. x , y >. ) ) )

Distinct variable groups:   x, A, y   x, B, y   x, C, y   x, D, y   x, N, y   x, T, y

Proof of Theorem axeuclid

Dummy variables i p q r s u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl21 1083	. . . . . 6 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> A e. ( EE ` N ) )
2		simpl22 1084	. . . . . 6 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> B e. ( EE ` N ) )
3	1, 2	jca 534	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
4		simpl23 1085	. . . . . 6 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> C e. ( EE ` N ) )
5		simpl3r 1061	. . . . . 6 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> T e. ( EE ` N ) )
6	4, 5	jca 534	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) )
7		simprll 770	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> p e. ( 0 [,] 1 ) )
8		simprlr 771	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> q e. ( 0 [,] 1 ) )
9		simp21 1038	. . . . . . . . . . . . . . . . . . 19 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
10	9	ad2antrr 730	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) -> A e. ( EE ` N ) )
11		fveecn 24869	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
12	10, 11	sylan 473	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
13		simp3r 1034	. . . . . . . . . . . . . . . . . . 19 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> T e. ( EE ` N ) )
14	13	ad2antrr 730	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) -> T e. ( EE ` N ) )
15		fveecn 24869	. . . . . . . . . . . . . . . . . 18 |- ( ( T e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( T ` i ) e. CC )
16	14, 15	sylan 473	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) /\ i e. ( 1 ... N ) ) -> ( T ` i ) e. CC )
17		mulid2 9587	. . . . . . . . . . . . . . . . . . 19 |- ( ( A ` i ) e. CC -> ( 1 x. ( A ` i ) ) = ( A ` i ) )
18		mul02 9757	. . . . . . . . . . . . . . . . . . 19 |- ( ( T ` i ) e. CC -> ( 0 x. ( T ` i ) ) = 0 )
19	17, 18	oveqan12d 6263	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A ` i ) e. CC /\ ( T ` i ) e. CC ) -> ( ( 1 x. ( A ` i ) ) + ( 0 x. ( T ` i ) ) ) = ( ( A ` i ) + 0 ) )
20		addid1 9759	. . . . . . . . . . . . . . . . . . 19 |- ( ( A ` i ) e. CC -> ( ( A ` i ) + 0 ) = ( A ` i ) )
21	20	adantr 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A ` i ) e. CC /\ ( T ` i ) e. CC ) -> ( ( A ` i ) + 0 ) = ( A ` i ) )
22	19, 21	eqtrd 2457	. . . . . . . . . . . . . . . . 17 |- ( ( ( A ` i ) e. CC /\ ( T ` i ) e. CC ) -> ( ( 1 x. ( A ` i ) ) + ( 0 x. ( T ` i ) ) ) = ( A ` i ) )
23	12, 16, 22	syl2anc 665	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) /\ i e. ( 1 ... N ) ) -> ( ( 1 x. ( A ` i ) ) + ( 0 x. ( T ` i ) ) ) = ( A ` i ) )
24		oveq2 6252	. . . . . . . . . . . . . . . . . . . . 21 |- ( p = 0 -> ( 1 - p ) = ( 1 - 0 ) )
25		1m0e1 10666	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1 - 0 ) = 1
26	24, 25	syl6eq 2473	. . . . . . . . . . . . . . . . . . . 20 |- ( p = 0 -> ( 1 - p ) = 1 )
27	26	oveq1d 6259	. . . . . . . . . . . . . . . . . . 19 |- ( p = 0 -> ( ( 1 - p ) x. ( A ` i ) ) = ( 1 x. ( A ` i ) ) )
28		oveq1 6251	. . . . . . . . . . . . . . . . . . 19 |- ( p = 0 -> ( p x. ( T ` i ) ) = ( 0 x. ( T ` i ) ) )
29	27, 28	oveq12d 6262	. . . . . . . . . . . . . . . . . 18 |- ( p = 0 -> ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) = ( ( 1 x. ( A ` i ) ) + ( 0 x. ( T ` i ) ) ) )
30	29	eqeq1d 2425	. . . . . . . . . . . . . . . . 17 |- ( p = 0 -> ( ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) = ( A ` i ) <-> ( ( 1 x. ( A ` i ) ) + ( 0 x. ( T ` i ) ) ) = ( A ` i ) ) )
31	30	ad2antlr 731	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) = ( A ` i ) <-> ( ( 1 x. ( A ` i ) ) + ( 0 x. ( T ` i ) ) ) = ( A ` i ) ) )
32	23, 31	mpbird 235	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) = ( A ` i ) )
33	32	eqeq2d 2433	. . . . . . . . . . . . . 14 |- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) /\ i e. ( 1 ... N ) ) -> ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) <-> ( D ` i ) = ( A ` i ) ) )
34		eqcom 2430	. . . . . . . . . . . . . 14 |- ( ( D ` i ) = ( A ` i ) <-> ( A ` i ) = ( D ` i ) )
35	33, 34	syl6bb 264	. . . . . . . . . . . . 13 |- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) /\ i e. ( 1 ... N ) ) -> ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) <-> ( A ` i ) = ( D ` i ) ) )
36	35	biimpd 210	. . . . . . . . . . . 12 |- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) /\ i e. ( 1 ... N ) ) -> ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) -> ( A ` i ) = ( D ` i ) ) )
37	36	adantrd 469	. . . . . . . . . . 11 |- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) -> ( A ` i ) = ( D ` i ) ) )
38	37	ralimdva 2768	. . . . . . . . . 10 |- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ p = 0 ) -> ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( A ` i ) = ( D ` i ) ) )
39	38	impancom 441	. . . . . . . . 9 |- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) ) -> ( p = 0 -> A. i e. ( 1 ... N ) ( A ` i ) = ( D ` i ) ) )
40	9	ad2antrr 730	. . . . . . . . . 10 |- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) ) -> A e. ( EE ` N ) )
41		simp3l 1033	. . . . . . . . . . 11 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
42	41	ad2antrr 730	. . . . . . . . . 10 |- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) ) -> D e. ( EE ` N ) )
43		eqeefv 24870	. . . . . . . . . 10 |- ( ( A e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( A = D <-> A. i e. ( 1 ... N ) ( A ` i ) = ( D ` i ) ) )
44	40, 42, 43	syl2anc 665	. . . . . . . . 9 |- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) ) -> ( A = D <-> A. i e. ( 1 ... N ) ( A ` i ) = ( D ` i ) ) )
45	39, 44	sylibrd 237	. . . . . . . 8 |- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) ) -> ( p = 0 -> A = D ) )
46	45	necon3d 2617	. . . . . . 7 |- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) ) -> ( A =/= D -> p =/= 0 ) )
47	46	impr 623	. . . . . 6 |- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) -> p =/= 0 )
48	47	anasss 651	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> p =/= 0 )
49		eqtr2 2443	. . . . . . . 8 |- ( ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) -> ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) )
50	49	ralimi 2753	. . . . . . 7 |- ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) )
51	50	adantr 466	. . . . . 6 |- ( ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) -> A. i e. ( 1 ... N ) ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) )
52	51	ad2antll 733	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> A. i e. ( 1 ... N ) ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) )
53		axeuclidlem 24929	. . . . 5 |- ( ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) /\ p =/= 0 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
54	3, 6, 7, 8, 48, 52, 53	syl231anc 1284	. . . 4 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
55	54	exp32 608	. . 3 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( ( p e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) -> ( ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) ) )
56	55	rexlimdvv 2857	. 2 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( E. p e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) )
57		brbtwn 24866	. . . . 5 |- ( ( D e. ( EE ` N ) /\ A e. ( EE ` N ) /\ T e. ( EE ` N ) ) -> ( D Btwn <. A , T >. <-> E. p e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) ) )
58	41, 9, 13, 57	syl3anc 1264	. . . 4 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( D Btwn <. A , T >. <-> E. p e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) ) )
59		simp22 1039	. . . . 5 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
60		simp23 1040	. . . . 5 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
61		brbtwn 24866	. . . . 5 |- ( ( D e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( D Btwn <. B , C >. <-> E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) )
62	41, 59, 60, 61	syl3anc 1264	. . . 4 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( D Btwn <. B , C >. <-> E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) )
63	58, 62	3anbi12d 1336	. . 3 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , T >. /\ D Btwn <. B , C >. /\ A =/= D ) <-> ( E. p e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) /\ A =/= D ) ) )
64		r19.26 2889	. . . . . . 7 |- ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) <-> ( A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) )
65	64	2rexbii 2862	. . . . . 6 |- ( E. p e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) <-> E. p e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) )
66		reeanv 2930	. . . . . 6 |- ( E. p e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) <-> ( E. p e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) )
67	65, 66	bitri 252	. . . . 5 |- ( E. p e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) <-> ( E. p e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) )
68	67	anbi1i 699	. . . 4 |- ( ( E. p e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) <-> ( ( E. p e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) )
69		r19.41vv 2916	. . . 4 |- ( E. p e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) <-> ( E. p e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) )
70		df-3an 984	. . . 4 |- ( ( E. p e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) /\ A =/= D ) <-> ( ( E. p e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) )
71	68, 69, 70	3bitr4i 280	. . 3 |- ( E. p e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) <-> ( E. p e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) /\ A =/= D ) )
72	63, 71	syl6bbr 266	. 2 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , T >. /\ D Btwn <. B , C >. /\ A =/= D ) <-> E. p e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - p ) x. ( A ` i ) ) + ( p x. ( T ` i ) ) ) /\ ( D ` i ) = ( ( ( 1 - q ) x. ( B ` i ) ) + ( q x. ( C ` i ) ) ) ) /\ A =/= D ) ) )
73		simpl22 1084	. . . . . 6 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
74		simpl21 1083	. . . . . 6 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
75		simprl 762	. . . . . 6 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> x e. ( EE ` N ) )
76		brbtwn 24866	. . . . . 6 |- ( ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ x e. ( EE ` N ) ) -> ( B Btwn <. A , x >. <-> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) ) )
77	73, 74, 75, 76	syl3anc 1264	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( B Btwn <. A , x >. <-> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) ) )
78		simpl23 1085	. . . . . 6 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
79		simprr 764	. . . . . 6 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> y e. ( EE ` N ) )
80		brbtwn 24866	. . . . . 6 |- ( ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ y e. ( EE ` N ) ) -> ( C Btwn <. A , y >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) ) )
81	78, 74, 79, 80	syl3anc 1264	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( C Btwn <. A , y >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) ) )
82		simpl3r 1061	. . . . . 6 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> T e. ( EE ` N ) )
83		brbtwn 24866	. . . . . 6 |- ( ( T e. ( EE ` N ) /\ x e. ( EE ` N ) /\ y e. ( EE ` N ) ) -> ( T Btwn <. x , y >. <-> E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
84	82, 75, 79, 83	syl3anc 1264	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( T Btwn <. x , y >. <-> E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
85	77, 81, 84	3anbi123d 1335	. . . 4 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , x >. /\ C Btwn <. A , y >. /\ T Btwn <. x , y >. ) <-> ( E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) )
86		r19.26-3 2891	. . . . . . 7 |- ( A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ A. i e. ( 1 ... N ) ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ A. i e. ( 1 ... N ) ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
87	86	rexbii 2861	. . . . . 6 |- ( E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. u e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ A. i e. ( 1 ... N ) ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ A. i e. ( 1 ... N ) ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
88	87	2rexbii 2862	. . . . 5 |- ( E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ A. i e. ( 1 ... N ) ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ A. i e. ( 1 ... N ) ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
89		3reeanv 2931	. . . . 5 |- ( E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ A. i e. ( 1 ... N ) ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ A. i e. ( 1 ... N ) ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> ( E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
90	88, 89	bitri 252	. . . 4 |- ( E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) <-> ( E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) )
91	85, 90	syl6bbr 266	. . 3 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , x >. /\ C Btwn <. A , y >. /\ T Btwn <. x , y >. ) <-> E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) )
92	91	2rexbidva 2879	. 2 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( E. x e. ( EE ` N ) E. y e. ( EE ` N ) ( B Btwn <. A , x >. /\ C Btwn <. A , y >. /\ T Btwn <. x , y >. ) <-> E. x e. ( EE ` N ) E. y e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) E. u e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( B ` i ) = ( ( ( 1 - r ) x. ( A ` i ) ) + ( r x. ( x ` i ) ) ) /\ ( C ` i ) = ( ( ( 1 - s ) x. ( A ` i ) ) + ( s x. ( y ` i ) ) ) /\ ( T ` i ) = ( ( ( 1 - u ) x. ( x ` i ) ) + ( u x. ( y ` i ) ) ) ) ) )
93	56, 72, 92	3imtr4d 271	1 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ T e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , T >. /\ D Btwn <. B , C >. /\ A =/= D ) -> E. x e. ( EE ` N ) E. y e. ( EE ` N ) ( B Btwn <. A , x >. /\ C Btwn <. A , y >. /\ T Btwn <. x , y >. ) ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1872   =/= wne 2594   A.wral 2709   E.wrex 2710   <.cop 3942   class class class wbr 4361   ` cfv 5539  (class class class)co 6244   CCcc 9483   0cc0 9485   1c1 9486   + caddc 9488   x. cmul 9490   - cmin 9806   NNcn 10555   [,]cicc 11584   ...cfz 11730   EEcee 24855   Btwn cbtwn 24856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-1st 6746  df-2nd 6747  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-er 7313  df-map 7424  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216  df-nn 10556  df-z 10884  df-uz 11106  df-icc 11588  df-fz 11731  df-ee 24858  df-btwn 24859

This theorem is referenced by:  eengtrkge  24953