Theorem axcontlem2

Description: Lemma for axcont . The idea here is to set up a mapping F that will allow to transfer dedekind to two sets of points. Here, we set up F and show its domain and codomain. (Contributed by Scott Fenton, 17-Jun-2013)

	Ref	Expression
Hypotheses	axcontlem2.1	|- D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
	axcontlem2.2	|- F = { <. x , t >. | ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
Assertion	axcontlem2	|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F : D -1-1-onto-> ( 0 [,) +oo ) )

Proof

Step	Hyp	Ref	Expression
1		axcontlem2.1	|- D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
2		axcontlem2.2	|- F = { <. x , t >. | ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
3		opeq2	|- ( p = x -> <. Z , p >. = <. Z , x >. )
4	3	breq2d	|- ( p = x -> ( U Btwn <. Z , p >. <-> U Btwn <. Z , x >. ) )
5		breq1	|- ( p = x -> ( p Btwn <. Z , U >. <-> x Btwn <. Z , U >. ) )
6	4 5	orbi12d	|- ( p = x -> ( ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) <-> ( U Btwn <. Z , x >. \/ x Btwn <. Z , U >. ) ) )
7	6 1	elrab2	|- ( x e. D <-> ( x e. ( EE ` N ) /\ ( U Btwn <. Z , x >. \/ x Btwn <. Z , U >. ) ) )
8		simpll3	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) -> U e. ( EE ` N ) )
9		simpll2	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) -> Z e. ( EE ` N ) )
10		simpr	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
11		brbtwn	|- ( ( U e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ x e. ( EE ` N ) ) -> ( U Btwn <. Z , x >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) )
12	8 9 10 11	syl3anc	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) -> ( U Btwn <. Z , x >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) )
13	12	biimpa	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ U Btwn <. Z , x >. ) -> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) )
14		simp-4r	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> Z =/= U )
15		oveq2	|- ( s = 0 -> ( 1 - s ) = ( 1 - 0 ) )
16		1m0e1	|- ( 1 - 0 ) = 1
17	15 16	eqtrdi	|- ( s = 0 -> ( 1 - s ) = 1 )
18	17	oveq1d	|- ( s = 0 -> ( ( 1 - s ) x. ( Z ` i ) ) = ( 1 x. ( Z ` i ) ) )
19		oveq1	|- ( s = 0 -> ( s x. ( x ` i ) ) = ( 0 x. ( x ` i ) ) )
20	18 19	oveq12d	|- ( s = 0 -> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) )
21	20	eqeq2d	|- ( s = 0 -> ( ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) <-> ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) ) )
22	21	ralbidv	|- ( s = 0 -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) ) )
23	22	biimpac	|- ( ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) /\ s = 0 ) -> A. i e. ( 1 ... N ) ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) )
24		eqcom	|- ( Z = U <-> U = Z )
25	8	adantr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> U e. ( EE ` N ) )
26	9	adantr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> Z e. ( EE ` N ) )
27		eqeefv	|- ( ( U e. ( EE ` N ) /\ Z e. ( EE ` N ) ) -> ( U = Z <-> A. i e. ( 1 ... N ) ( U ` i ) = ( Z ` i ) ) )
28	25 26 27	syl2anc	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> ( U = Z <-> A. i e. ( 1 ... N ) ( U ` i ) = ( Z ` i ) ) )
29	9	ad2antrr	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
30		fveecn	|- ( ( Z e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
31	29 30	sylancom	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
32		fveecn	|- ( ( x e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. CC )
33	32	ad4ant24	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. CC )
34		mullid	|- ( ( Z ` i ) e. CC -> ( 1 x. ( Z ` i ) ) = ( Z ` i ) )
35		mul02	|- ( ( x ` i ) e. CC -> ( 0 x. ( x ` i ) ) = 0 )
36	34 35	oveqan12d	|- ( ( ( Z ` i ) e. CC /\ ( x ` i ) e. CC ) -> ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) = ( ( Z ` i ) + 0 ) )
37		addrid	|- ( ( Z ` i ) e. CC -> ( ( Z ` i ) + 0 ) = ( Z ` i ) )
38	37	adantr	|- ( ( ( Z ` i ) e. CC /\ ( x ` i ) e. CC ) -> ( ( Z ` i ) + 0 ) = ( Z ` i ) )
39	36 38	eqtrd	|- ( ( ( Z ` i ) e. CC /\ ( x ` i ) e. CC ) -> ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) = ( Z ` i ) )
40	39	eqeq2d	|- ( ( ( Z ` i ) e. CC /\ ( x ` i ) e. CC ) -> ( ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) <-> ( U ` i ) = ( Z ` i ) ) )
41	31 33 40	syl2anc	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) <-> ( U ` i ) = ( Z ` i ) ) )
42	41	ralbidva	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) <-> A. i e. ( 1 ... N ) ( U ` i ) = ( Z ` i ) ) )
43	28 42	bitr4d	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> ( U = Z <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) ) )
44	24 43	bitrid	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( x ` i ) ) ) ) )
45	23 44	imbitrrid	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) -> ( ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) /\ s = 0 ) -> Z = U ) )
46	45	expdimp	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> ( s = 0 -> Z = U ) )
47	46	necon3d	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> ( Z =/= U -> s =/= 0 ) )
48	14 47	mpd	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> s =/= 0 )
49		elicc01	|- ( s e. ( 0 [,] 1 ) <-> ( s e. RR /\ 0 <_ s /\ s <_ 1 ) )
50	49	simp1bi	|- ( s e. ( 0 [,] 1 ) -> s e. RR )
51		rereccl	|- ( ( s e. RR /\ s =/= 0 ) -> ( 1 / s ) e. RR )
52	50 51	sylan	|- ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> ( 1 / s ) e. RR )
53	50	adantr	|- ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> s e. RR )
54	49	simp2bi	|- ( s e. ( 0 [,] 1 ) -> 0 <_ s )
55	54	adantr	|- ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> 0 <_ s )
56		simpr	|- ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> s =/= 0 )
57	53 55 56	ne0gt0d	|- ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> 0 < s )
58		1re	|- 1 e. RR
59		0le1	|- 0 <_ 1
60		divge0	|- ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( s e. RR /\ 0 < s ) ) -> 0 <_ ( 1 / s ) )
61	58 59 60	mpanl12	|- ( ( s e. RR /\ 0 < s ) -> 0 <_ ( 1 / s ) )
62	53 57 61	syl2anc	|- ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> 0 <_ ( 1 / s ) )
63		elrege0	|- ( ( 1 / s ) e. ( 0 [,) +oo ) <-> ( ( 1 / s ) e. RR /\ 0 <_ ( 1 / s ) ) )
64	52 62 63	sylanbrc	|- ( ( s e. ( 0 [,] 1 ) /\ s =/= 0 ) -> ( 1 / s ) e. ( 0 [,) +oo ) )
65	64	adantll	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) -> ( 1 / s ) e. ( 0 [,) +oo ) )
66	50	ad3antlr	|- ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> s e. RR )
67	66	recnd	|- ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> s e. CC )
68		simplr	|- ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> s =/= 0 )
69	32	ad5ant25	|- ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. CC )
70	9	ad3antrrr	|- ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
71	70 30	sylancom	|- ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
72		ax-1cn	|- 1 e. CC
73		reccl	|- ( ( s e. CC /\ s =/= 0 ) -> ( 1 / s ) e. CC )
74		subcl	|- ( ( 1 e. CC /\ ( 1 / s ) e. CC ) -> ( 1 - ( 1 / s ) ) e. CC )
75	72 73 74	sylancr	|- ( ( s e. CC /\ s =/= 0 ) -> ( 1 - ( 1 / s ) ) e. CC )
76	75	adantr	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( 1 - ( 1 / s ) ) e. CC )
77		subcl	|- ( ( 1 e. CC /\ s e. CC ) -> ( 1 - s ) e. CC )
78	72 77	mpan	|- ( s e. CC -> ( 1 - s ) e. CC )
79	78	adantr	|- ( ( s e. CC /\ s =/= 0 ) -> ( 1 - s ) e. CC )
80	73 79	mulcld	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 / s ) x. ( 1 - s ) ) e. CC )
81	80	adantr	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 / s ) x. ( 1 - s ) ) e. CC )
82		simprr	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( Z ` i ) e. CC )
83	76 81 82	adddird	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) x. ( 1 - s ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( ( 1 / s ) x. ( 1 - s ) ) x. ( Z ` i ) ) ) )
84		simpl	|- ( ( s e. CC /\ s =/= 0 ) -> s e. CC )
85		subdi	|- ( ( ( 1 / s ) e. CC /\ 1 e. CC /\ s e. CC ) -> ( ( 1 / s ) x. ( 1 - s ) ) = ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) )
86	72 85	mp3an2	|- ( ( ( 1 / s ) e. CC /\ s e. CC ) -> ( ( 1 / s ) x. ( 1 - s ) ) = ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) )
87	73 84 86	syl2anc	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 / s ) x. ( 1 - s ) ) = ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) )
88	87	oveq2d	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) x. ( 1 - s ) ) ) = ( ( 1 - ( 1 / s ) ) + ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) ) )
89	73	mulridd	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 / s ) x. 1 ) = ( 1 / s ) )
90		recid2	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 / s ) x. s ) = 1 )
91	89 90	oveq12d	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) = ( ( 1 / s ) - 1 ) )
92	91	oveq2d	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) ) = ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) - 1 ) ) )
93		addsubass	|- ( ( ( 1 - ( 1 / s ) ) e. CC /\ ( 1 / s ) e. CC /\ 1 e. CC ) -> ( ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) - 1 ) = ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) - 1 ) ) )
94	72 93	mp3an3	|- ( ( ( 1 - ( 1 / s ) ) e. CC /\ ( 1 / s ) e. CC ) -> ( ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) - 1 ) = ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) - 1 ) ) )
95	75 73 94	syl2anc	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) - 1 ) = ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) - 1 ) ) )
96	75 73	addcld	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) e. CC )
97		npcan	|- ( ( 1 e. CC /\ ( 1 / s ) e. CC ) -> ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) = 1 )
98	72 73 97	sylancr	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) = 1 )
99	96 98	subeq0bd	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( ( 1 - ( 1 / s ) ) + ( 1 / s ) ) - 1 ) = 0 )
100	92 95 99	3eqtr2d	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( ( ( 1 / s ) x. 1 ) - ( ( 1 / s ) x. s ) ) ) = 0 )
101	88 100	eqtrd	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) x. ( 1 - s ) ) ) = 0 )
102	101	adantr	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) x. ( 1 - s ) ) ) = 0 )
103	102	oveq1d	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) + ( ( 1 / s ) x. ( 1 - s ) ) ) x. ( Z ` i ) ) = ( 0 x. ( Z ` i ) ) )
104	73	adantr	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( 1 / s ) e. CC )
105	78	ad2antrr	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( 1 - s ) e. CC )
106	104 105 82	mulassd	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 / s ) x. ( 1 - s ) ) x. ( Z ` i ) ) = ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) )
107	106	oveq2d	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( ( 1 / s ) x. ( 1 - s ) ) x. ( Z ` i ) ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) )
108	83 103 107	3eqtr3rd	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) = ( 0 x. ( Z ` i ) ) )
109		mul02	|- ( ( Z ` i ) e. CC -> ( 0 x. ( Z ` i ) ) = 0 )
110	109	ad2antll	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( 0 x. ( Z ` i ) ) = 0 )
111	108 110	eqtrd	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) = 0 )
112		simpll	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> s e. CC )
113		simprl	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( x ` i ) e. CC )
114	104 112 113	mulassd	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 / s ) x. s ) x. ( x ` i ) ) = ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) )
115	90	oveq1d	|- ( ( s e. CC /\ s =/= 0 ) -> ( ( ( 1 / s ) x. s ) x. ( x ` i ) ) = ( 1 x. ( x ` i ) ) )
116		mullid	|- ( ( x ` i ) e. CC -> ( 1 x. ( x ` i ) ) = ( x ` i ) )
117	116	adantr	|- ( ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) -> ( 1 x. ( x ` i ) ) = ( x ` i ) )
118	115 117	sylan9eq	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 / s ) x. s ) x. ( x ` i ) ) = ( x ` i ) )
119	114 118	eqtr3d	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) = ( x ` i ) )
120	111 119	oveq12d	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) = ( 0 + ( x ` i ) ) )
121	76 82	mulcld	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) e. CC )
122		simpr	|- ( ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) -> ( Z ` i ) e. CC )
123		mulcl	|- ( ( ( 1 - s ) e. CC /\ ( Z ` i ) e. CC ) -> ( ( 1 - s ) x. ( Z ` i ) ) e. CC )
124	79 122 123	syl2an	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 - s ) x. ( Z ` i ) ) e. CC )
125	104 124	mulcld	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) e. CC )
126		mulcl	|- ( ( s e. CC /\ ( x ` i ) e. CC ) -> ( s x. ( x ` i ) ) e. CC )
127	126	ad2ant2r	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( s x. ( x ` i ) ) e. CC )
128	104 127	mulcld	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) e. CC )
129	121 125 128	addassd	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) ) )
130	104 124 127	adddid	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) = ( ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) )
131	130	oveq2d	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) ) )
132	129 131	eqtr4d	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) + ( ( 1 / s ) x. ( s x. ( x ` i ) ) ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
133		addlid	|- ( ( x ` i ) e. CC -> ( 0 + ( x ` i ) ) = ( x ` i ) )
134	133	ad2antrl	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( 0 + ( x ` i ) ) = ( x ` i ) )
135	120 132 134	3eqtr3rd	|- ( ( ( s e. CC /\ s =/= 0 ) /\ ( ( x ` i ) e. CC /\ ( Z ` i ) e. CC ) ) -> ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
136	67 68 69 71 135	syl22anc	|- ( ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
137	136	ralrimiva	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) -> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
138		oveq2	|- ( t = ( 1 / s ) -> ( 1 - t ) = ( 1 - ( 1 / s ) ) )
139	138	oveq1d	|- ( t = ( 1 / s ) -> ( ( 1 - t ) x. ( Z ` i ) ) = ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) )
140		oveq1	|- ( t = ( 1 / s ) -> ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) = ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) )
141	139 140	oveq12d	|- ( t = ( 1 / s ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
142	141	eqeq2d	|- ( t = ( 1 / s ) -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) <-> ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
143	142	ralbidv	|- ( t = ( 1 / s ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) <-> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
144	143	rspcev	|- ( ( ( 1 / s ) e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - ( 1 / s ) ) x. ( Z ` i ) ) + ( ( 1 / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
145	65 137 144	syl2anc	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
146		oveq2	|- ( ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> ( t x. ( U ` i ) ) = ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) )
147	146	oveq2d	|- ( ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) )
148	147	eqeq2d	|- ( ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
149	148	ralimi	|- ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
150		ralbi	|- ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
151	149 150	syl	|- ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
152	151	rexbidv	|- ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> ( E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) ) ) )
153	145 152	syl5ibrcom	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ s =/= 0 ) -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
154	153	impancom	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> ( s =/= 0 -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
155	48 154	mpd	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ s e. ( 0 [,] 1 ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
156	155	r19.29an	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( x ` i ) ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
157	13 156	syldan	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ U Btwn <. Z , x >. ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
158		3simpa	|- ( ( x e. RR /\ 0 <_ x /\ x <_ 1 ) -> ( x e. RR /\ 0 <_ x ) )
159		elicc01	|- ( x e. ( 0 [,] 1 ) <-> ( x e. RR /\ 0 <_ x /\ x <_ 1 ) )
160		elrege0	|- ( x e. ( 0 [,) +oo ) <-> ( x e. RR /\ 0 <_ x ) )
161	158 159 160	3imtr4i	|- ( x e. ( 0 [,] 1 ) -> x e. ( 0 [,) +oo ) )
162	161	ssriv	|- ( 0 [,] 1 ) C_ ( 0 [,) +oo )
163		brbtwn	|- ( ( x e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) -> ( x Btwn <. Z , U >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
164	10 9 8 163	syl3anc	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. Z , U >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
165	164	biimpa	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ x Btwn <. Z , U >. ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
166		ssrexv	|- ( ( 0 [,] 1 ) C_ ( 0 [,) +oo ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
167	162 165 166	mpsyl	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ x Btwn <. Z , U >. ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
168	157 167	jaodan	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. ( EE ` N ) ) /\ ( U Btwn <. Z , x >. \/ x Btwn <. Z , U >. ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
169	168	anasss	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( x e. ( EE ` N ) /\ ( U Btwn <. Z , x >. \/ x Btwn <. Z , U >. ) ) ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
170	7 169	sylan2b	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. D ) -> E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
171		r19.26	|- ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) <-> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
172		eqtr2	|- ( ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
173	172	ralimi	|- ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
174	171 173	sylbir	|- ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
175		elrege0	|- ( t e. ( 0 [,) +oo ) <-> ( t e. RR /\ 0 <_ t ) )
176	175	simplbi	|- ( t e. ( 0 [,) +oo ) -> t e. RR )
177	176	recnd	|- ( t e. ( 0 [,) +oo ) -> t e. CC )
178		elrege0	|- ( s e. ( 0 [,) +oo ) <-> ( s e. RR /\ 0 <_ s ) )
179	178	simplbi	|- ( s e. ( 0 [,) +oo ) -> s e. RR )
180	179	recnd	|- ( s e. ( 0 [,) +oo ) -> s e. CC )
181	177 180	anim12i	|- ( ( t e. ( 0 [,) +oo ) /\ s e. ( 0 [,) +oo ) ) -> ( t e. CC /\ s e. CC ) )
182		simplr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> ( t e. CC /\ s e. CC ) )
183		simpl2	|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> Z e. ( EE ` N ) )
184	183	ad2antrr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
185	184 30	sylancom	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
186		simpl3	|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> U e. ( EE ` N ) )
187	186	ad2antrr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> U e. ( EE ` N ) )
188		fveecn	|- ( ( U e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) e. CC )
189	187 188	sylancom	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) e. CC )
190		subcl	|- ( ( 1 e. CC /\ t e. CC ) -> ( 1 - t ) e. CC )
191	72 190	mpan	|- ( t e. CC -> ( 1 - t ) e. CC )
192	191	adantr	|- ( ( t e. CC /\ s e. CC ) -> ( 1 - t ) e. CC )
193		simpl	|- ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) -> ( Z ` i ) e. CC )
194		mulcl	|- ( ( ( 1 - t ) e. CC /\ ( Z ` i ) e. CC ) -> ( ( 1 - t ) x. ( Z ` i ) ) e. CC )
195	192 193 194	syl2an	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - t ) x. ( Z ` i ) ) e. CC )
196		mulcl	|- ( ( t e. CC /\ ( U ` i ) e. CC ) -> ( t x. ( U ` i ) ) e. CC )
197	196	ad2ant2rl	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( t x. ( U ` i ) ) e. CC )
198	78	adantl	|- ( ( t e. CC /\ s e. CC ) -> ( 1 - s ) e. CC )
199	198 193 123	syl2an	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - s ) x. ( Z ` i ) ) e. CC )
200		mulcl	|- ( ( s e. CC /\ ( U ` i ) e. CC ) -> ( s x. ( U ` i ) ) e. CC )
201	200	ad2ant2l	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( s x. ( U ` i ) ) e. CC )
202	195 197 199 201	addsubeq4d	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> ( ( ( 1 - s ) x. ( Z ` i ) ) - ( ( 1 - t ) x. ( Z ` i ) ) ) = ( ( t x. ( U ` i ) ) - ( s x. ( U ` i ) ) ) ) )
203		nnncan1	|- ( ( 1 e. CC /\ s e. CC /\ t e. CC ) -> ( ( 1 - s ) - ( 1 - t ) ) = ( t - s ) )
204	72 203	mp3an1	|- ( ( s e. CC /\ t e. CC ) -> ( ( 1 - s ) - ( 1 - t ) ) = ( t - s ) )
205	204	ancoms	|- ( ( t e. CC /\ s e. CC ) -> ( ( 1 - s ) - ( 1 - t ) ) = ( t - s ) )
206	205	oveq1d	|- ( ( t e. CC /\ s e. CC ) -> ( ( ( 1 - s ) - ( 1 - t ) ) x. ( Z ` i ) ) = ( ( t - s ) x. ( Z ` i ) ) )
207	206	adantr	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - s ) - ( 1 - t ) ) x. ( Z ` i ) ) = ( ( t - s ) x. ( Z ` i ) ) )
208	78	ad2antlr	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 - s ) e. CC )
209	191	ad2antrr	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 - t ) e. CC )
210		simprl	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( Z ` i ) e. CC )
211	208 209 210	subdird	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - s ) - ( 1 - t ) ) x. ( Z ` i ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) - ( ( 1 - t ) x. ( Z ` i ) ) ) )
212	207 211	eqtr3d	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( t - s ) x. ( Z ` i ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) - ( ( 1 - t ) x. ( Z ` i ) ) ) )
213		simpll	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> t e. CC )
214		simplr	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> s e. CC )
215		simprr	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( U ` i ) e. CC )
216	213 214 215	subdird	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( t - s ) x. ( U ` i ) ) = ( ( t x. ( U ` i ) ) - ( s x. ( U ` i ) ) ) )
217	212 216	eqeq12d	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( t - s ) x. ( Z ` i ) ) = ( ( t - s ) x. ( U ` i ) ) <-> ( ( ( 1 - s ) x. ( Z ` i ) ) - ( ( 1 - t ) x. ( Z ` i ) ) ) = ( ( t x. ( U ` i ) ) - ( s x. ( U ` i ) ) ) ) )
218		subcl	|- ( ( t e. CC /\ s e. CC ) -> ( t - s ) e. CC )
219	218	adantr	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( t - s ) e. CC )
220		mulcan1g	|- ( ( ( t - s ) e. CC /\ ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) -> ( ( ( t - s ) x. ( Z ` i ) ) = ( ( t - s ) x. ( U ` i ) ) <-> ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
221	219 210 215 220	syl3anc	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( t - s ) x. ( Z ` i ) ) = ( ( t - s ) x. ( U ` i ) ) <-> ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
222	202 217 221	3bitr2d	|- ( ( ( t e. CC /\ s e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
223	182 185 189 222	syl12anc	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
224	223	ralbidva	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
225		r19.32v	|- ( A. i e. ( 1 ... N ) ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) <-> ( ( t - s ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
226		simplr	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> Z =/= U )
227	226	neneqd	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> -. Z = U )
228		simpll2	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> Z e. ( EE ` N ) )
229		simpll3	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> U e. ( EE ` N ) )
230		eqeefv	|- ( ( Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
231	228 229 230	syl2anc	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
232	227 231	mtbid	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> -. A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) )
233		orel2	|- ( -. A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) -> ( ( ( t - s ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) -> ( t - s ) = 0 ) )
234	232 233	syl	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( ( ( t - s ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) -> ( t - s ) = 0 ) )
235		subeq0	|- ( ( t e. CC /\ s e. CC ) -> ( ( t - s ) = 0 <-> t = s ) )
236	235	adantl	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( ( t - s ) = 0 <-> t = s ) )
237	234 236	sylibd	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( ( ( t - s ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) -> t = s ) )
238	225 237	biimtrid	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( A. i e. ( 1 ... N ) ( ( t - s ) = 0 \/ ( Z ` i ) = ( U ` i ) ) -> t = s ) )
239	224 238	sylbid	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. CC /\ s e. CC ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) -> t = s ) )
240	181 239	sylan2	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. ( 0 [,) +oo ) /\ s e. ( 0 [,) +oo ) ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) -> t = s ) )
241	174 240	syl5	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( t e. ( 0 [,) +oo ) /\ s e. ( 0 [,) +oo ) ) ) -> ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> t = s ) )
242	241	ralrimivva	|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> A. t e. ( 0 [,) +oo ) A. s e. ( 0 [,) +oo ) ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> t = s ) )
243	242	adantr	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. D ) -> A. t e. ( 0 [,) +oo ) A. s e. ( 0 [,) +oo ) ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> t = s ) )
244		oveq2	|- ( t = s -> ( 1 - t ) = ( 1 - s ) )
245	244	oveq1d	|- ( t = s -> ( ( 1 - t ) x. ( Z ` i ) ) = ( ( 1 - s ) x. ( Z ` i ) ) )
246		oveq1	|- ( t = s -> ( t x. ( U ` i ) ) = ( s x. ( U ` i ) ) )
247	245 246	oveq12d	|- ( t = s -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
248	247	eqeq2d	|- ( t = s -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
249	248	ralbidv	|- ( t = s -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
250	249	reu4	|- ( E! t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( E. t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. t e. ( 0 [,) +oo ) A. s e. ( 0 [,) +oo ) ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) -> t = s ) ) )
251	170 243 250	sylanbrc	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. D ) -> E! t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
252		df-reu	|- ( E! t e. ( 0 [,) +oo ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> E! t ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
253	251 252	sylib	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ x e. D ) -> E! t ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
254	253	ralrimiva	|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> A. x e. D E! t ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
255	2	fnopabg	|- ( A. x e. D E! t ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> F Fn D )
256	254 255	sylib	|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F Fn D )
257	176	ad2antlr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> t e. RR )
258	183	ad2antrr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
259		fveere	|- ( ( Z e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( Z ` k ) e. RR )
260	258 259	sylancom	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> ( Z ` k ) e. RR )
261	186	ad2antrr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> U e. ( EE ` N ) )
262		fveere	|- ( ( U e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( U ` k ) e. RR )
263	261 262	sylancom	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> ( U ` k ) e. RR )
264		resubcl	|- ( ( 1 e. RR /\ t e. RR ) -> ( 1 - t ) e. RR )
265	58 264	mpan	|- ( t e. RR -> ( 1 - t ) e. RR )
266		remulcl	|- ( ( ( 1 - t ) e. RR /\ ( Z ` k ) e. RR ) -> ( ( 1 - t ) x. ( Z ` k ) ) e. RR )
267	265 266	sylan	|- ( ( t e. RR /\ ( Z ` k ) e. RR ) -> ( ( 1 - t ) x. ( Z ` k ) ) e. RR )
268	267	3adant3	|- ( ( t e. RR /\ ( Z ` k ) e. RR /\ ( U ` k ) e. RR ) -> ( ( 1 - t ) x. ( Z ` k ) ) e. RR )
269		remulcl	|- ( ( t e. RR /\ ( U ` k ) e. RR ) -> ( t x. ( U ` k ) ) e. RR )
270	269	3adant2	|- ( ( t e. RR /\ ( Z ` k ) e. RR /\ ( U ` k ) e. RR ) -> ( t x. ( U ` k ) ) e. RR )
271	268 270	readdcld	|- ( ( t e. RR /\ ( Z ` k ) e. RR /\ ( U ` k ) e. RR ) -> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) e. RR )
272	257 260 263 271	syl3anc	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) e. RR )
273	272	ralrimiva	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> A. k e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) e. RR )
274		simpll1	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> N e. NN )
275		mptelee	|- ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) e. RR ) )
276	274 275	syl	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) e. RR ) )
277	273 276	mpbird	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) )
278		letric	|- ( ( 1 e. RR /\ t e. RR ) -> ( 1 <_ t \/ t <_ 1 ) )
279	58 176 278	sylancr	|- ( t e. ( 0 [,) +oo ) -> ( 1 <_ t \/ t <_ 1 ) )
280	279	adantl	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( 1 <_ t \/ t <_ 1 ) )
281		simpr	|- ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> 1 <_ t )
282	176	adantr	|- ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> t e. RR )
283		0red	|- ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> 0 e. RR )
284		1red	|- ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> 1 e. RR )
285		0lt1	|- 0 < 1
286	285	a1i	|- ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> 0 < 1 )
287	283 284 282 286 281	ltletrd	|- ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> 0 < t )
288		divelunit	|- ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( t e. RR /\ 0 < t ) ) -> ( ( 1 / t ) e. ( 0 [,] 1 ) <-> 1 <_ t ) )
289	58 59 288	mpanl12	|- ( ( t e. RR /\ 0 < t ) -> ( ( 1 / t ) e. ( 0 [,] 1 ) <-> 1 <_ t ) )
290	282 287 289	syl2anc	|- ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> ( ( 1 / t ) e. ( 0 [,] 1 ) <-> 1 <_ t ) )
291	281 290	mpbird	|- ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> ( 1 / t ) e. ( 0 [,] 1 ) )
292	291	adantll	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> ( 1 / t ) e. ( 0 [,] 1 ) )
293	176	ad3antlr	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> t e. RR )
294	293	recnd	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> t e. CC )
295	287	gt0ne0d	|- ( ( t e. ( 0 [,) +oo ) /\ 1 <_ t ) -> t =/= 0 )
296	295	adantll	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> t =/= 0 )
297	296	adantr	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> t =/= 0 )
298	183	ad3antrrr	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
299	298 30	sylancom	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
300	186	ad3antrrr	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> U e. ( EE ` N ) )
301	300 188	sylancom	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) e. CC )
302		reccl	|- ( ( t e. CC /\ t =/= 0 ) -> ( 1 / t ) e. CC )
303	302	adantr	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 / t ) e. CC )
304	191	adantr	|- ( ( t e. CC /\ t =/= 0 ) -> ( 1 - t ) e. CC )
305	304 193 194	syl2an	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - t ) x. ( Z ` i ) ) e. CC )
306	196	ad2ant2rl	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( t x. ( U ` i ) ) e. CC )
307	303 305 306	adddid	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) = ( ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) )
308	307	oveq2d	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) ) )
309		subcl	|- ( ( 1 e. CC /\ ( 1 / t ) e. CC ) -> ( 1 - ( 1 / t ) ) e. CC )
310	72 302 309	sylancr	|- ( ( t e. CC /\ t =/= 0 ) -> ( 1 - ( 1 / t ) ) e. CC )
311		mulcl	|- ( ( ( 1 - ( 1 / t ) ) e. CC /\ ( Z ` i ) e. CC ) -> ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) e. CC )
312	310 193 311	syl2an	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) e. CC )
313	303 305	mulcld	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) e. CC )
314		recid2	|- ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 / t ) x. t ) = 1 )
315	314	oveq1d	|- ( ( t e. CC /\ t =/= 0 ) -> ( ( ( 1 / t ) x. t ) x. ( U ` i ) ) = ( 1 x. ( U ` i ) ) )
316	315	adantr	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 / t ) x. t ) x. ( U ` i ) ) = ( 1 x. ( U ` i ) ) )
317		simpll	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> t e. CC )
318		simprr	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( U ` i ) e. CC )
319	303 317 318	mulassd	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 / t ) x. t ) x. ( U ` i ) ) = ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) )
320		mullid	|- ( ( U ` i ) e. CC -> ( 1 x. ( U ` i ) ) = ( U ` i ) )
321	320	ad2antll	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 x. ( U ` i ) ) = ( U ` i ) )
322	316 319 321	3eqtr3d	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) = ( U ` i ) )
323	322 318	eqeltrd	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) e. CC )
324	312 313 323	addassd	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) ) )
325	310	adantr	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 - ( 1 / t ) ) e. CC )
326	302 304	mulcld	|- ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 / t ) x. ( 1 - t ) ) e. CC )
327	326	adantr	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 / t ) x. ( 1 - t ) ) e. CC )
328		simprl	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( Z ` i ) e. CC )
329	325 327 328	adddird	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( ( 1 / t ) x. ( 1 - t ) ) x. ( Z ` i ) ) ) )
330		simpl	|- ( ( t e. CC /\ t =/= 0 ) -> t e. CC )
331		subdi	|- ( ( ( 1 / t ) e. CC /\ 1 e. CC /\ t e. CC ) -> ( ( 1 / t ) x. ( 1 - t ) ) = ( ( ( 1 / t ) x. 1 ) - ( ( 1 / t ) x. t ) ) )
332	72 331	mp3an2	|- ( ( ( 1 / t ) e. CC /\ t e. CC ) -> ( ( 1 / t ) x. ( 1 - t ) ) = ( ( ( 1 / t ) x. 1 ) - ( ( 1 / t ) x. t ) ) )
333	302 330 332	syl2anc	|- ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 / t ) x. ( 1 - t ) ) = ( ( ( 1 / t ) x. 1 ) - ( ( 1 / t ) x. t ) ) )
334	302	mulridd	|- ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 / t ) x. 1 ) = ( 1 / t ) )
335	334 314	oveq12d	|- ( ( t e. CC /\ t =/= 0 ) -> ( ( ( 1 / t ) x. 1 ) - ( ( 1 / t ) x. t ) ) = ( ( 1 / t ) - 1 ) )
336	333 335	eqtrd	|- ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 / t ) x. ( 1 - t ) ) = ( ( 1 / t ) - 1 ) )
337	336	oveq2d	|- ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) = ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) - 1 ) ) )
338		npncan2	|- ( ( 1 e. CC /\ ( 1 / t ) e. CC ) -> ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) - 1 ) ) = 0 )
339	72 302 338	sylancr	|- ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) - 1 ) ) = 0 )
340	337 339	eqtrd	|- ( ( t e. CC /\ t =/= 0 ) -> ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) = 0 )
341	340	adantr	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) = 0 )
342	341	oveq1d	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) x. ( Z ` i ) ) = ( 0 x. ( Z ` i ) ) )
343	109	ad2antrl	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 0 x. ( Z ` i ) ) = 0 )
344	342 343	eqtrd	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) + ( ( 1 / t ) x. ( 1 - t ) ) ) x. ( Z ` i ) ) = 0 )
345	191	ad2antrr	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 - t ) e. CC )
346	303 345 328	mulassd	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 / t ) x. ( 1 - t ) ) x. ( Z ` i ) ) = ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) )
347	346	oveq2d	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( ( 1 / t ) x. ( 1 - t ) ) x. ( Z ` i ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) )
348	329 344 347	3eqtr3rd	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) = 0 )
349	348 322	oveq12d	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) = ( 0 + ( U ` i ) ) )
350		addlid	|- ( ( U ` i ) e. CC -> ( 0 + ( U ` i ) ) = ( U ` i ) )
351	350	ad2antll	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 0 + ( U ` i ) ) = ( U ` i ) )
352	349 351	eqtrd	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) + ( ( 1 / t ) x. ( t x. ( U ` i ) ) ) ) = ( U ` i ) )
353	308 324 352	3eqtr2rd	|- ( ( ( t e. CC /\ t =/= 0 ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
354	294 297 299 301 353	syl22anc	|- ( ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
355	354	ralrimiva	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
356		oveq2	|- ( s = ( 1 / t ) -> ( 1 - s ) = ( 1 - ( 1 / t ) ) )
357	356	oveq1d	|- ( s = ( 1 / t ) -> ( ( 1 - s ) x. ( Z ` i ) ) = ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) )
358		oveq1	|- ( s = ( 1 / t ) -> ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) = ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) )
359	357 358	oveq12d	|- ( s = ( 1 / t ) -> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) )
360	359	eqeq2d	|- ( s = ( 1 / t ) -> ( ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) <-> ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) ) )
361	360	ralbidv	|- ( s = ( 1 / t ) -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) ) )
362		fveq2	|- ( k = i -> ( Z ` k ) = ( Z ` i ) )
363	362	oveq2d	|- ( k = i -> ( ( 1 - t ) x. ( Z ` k ) ) = ( ( 1 - t ) x. ( Z ` i ) ) )
364		fveq2	|- ( k = i -> ( U ` k ) = ( U ` i ) )
365	364	oveq2d	|- ( k = i -> ( t x. ( U ` k ) ) = ( t x. ( U ` i ) ) )
366	363 365	oveq12d	|- ( k = i -> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
367		eqid	|- ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) )
368		ovex	|- ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) e. _V
369	366 367 368	fvmpt	|- ( i e. ( 1 ... N ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
370	369	oveq2d	|- ( i e. ( 1 ... N ) -> ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) = ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
371	370	oveq2d	|- ( i e. ( 1 ... N ) -> ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
372	371	eqeq2d	|- ( i e. ( 1 ... N ) -> ( ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) <-> ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) ) )
373	372	ralbiia	|- ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
374	361 373	bitrdi	|- ( s = ( 1 / t ) -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) <-> A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) ) )
375	374	rspcev	|- ( ( ( 1 / t ) e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( Z ` i ) ) + ( ( 1 / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) ) -> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) )
376	292 355 375	syl2anc	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) )
377	186	ad2antrr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> U e. ( EE ` N ) )
378	183	ad2antrr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> Z e. ( EE ` N ) )
379	277	adantr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) )
380		brbtwn	|- ( ( U e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) ) -> ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) ) )
381	377 378 379 380	syl3anc	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) ) ) ) )
382	376 381	mpbird	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ 1 <_ t ) -> U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. )
383	382	ex	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( 1 <_ t -> U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. ) )
384		simpll	|- ( ( ( t e. RR /\ 0 <_ t ) /\ t <_ 1 ) -> t e. RR )
385		simplr	|- ( ( ( t e. RR /\ 0 <_ t ) /\ t <_ 1 ) -> 0 <_ t )
386		simpr	|- ( ( ( t e. RR /\ 0 <_ t ) /\ t <_ 1 ) -> t <_ 1 )
387	384 385 386	3jca	|- ( ( ( t e. RR /\ 0 <_ t ) /\ t <_ 1 ) -> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
388	175	anbi1i	|- ( ( t e. ( 0 [,) +oo ) /\ t <_ 1 ) <-> ( ( t e. RR /\ 0 <_ t ) /\ t <_ 1 ) )
389		elicc01	|- ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
390	387 388 389	3imtr4i	|- ( ( t e. ( 0 [,) +oo ) /\ t <_ 1 ) -> t e. ( 0 [,] 1 ) )
391	390	adantll	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> t e. ( 0 [,] 1 ) )
392	369	rgen	|- A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) )
393		oveq2	|- ( s = t -> ( 1 - s ) = ( 1 - t ) )
394	393	oveq1d	|- ( s = t -> ( ( 1 - s ) x. ( Z ` i ) ) = ( ( 1 - t ) x. ( Z ` i ) ) )
395		oveq1	|- ( s = t -> ( s x. ( U ` i ) ) = ( t x. ( U ` i ) ) )
396	394 395	oveq12d	|- ( s = t -> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
397	396	eqeq2d	|- ( s = t -> ( ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
398	397	ralbidv	|- ( s = t -> ( A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
399	398	rspcev	|- ( ( t e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
400	391 392 399	sylancl	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
401	277	adantr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) )
402	183	ad2antrr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> Z e. ( EE ` N ) )
403	186	ad2antrr	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> U e. ( EE ` N ) )
404		brbtwn	|- ( ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
405	401 402 403 404	syl3anc	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
406	400 405	mpbird	|- ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) /\ t <_ 1 ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. )
407	406	ex	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( t <_ 1 -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) )
408	383 407	orim12d	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( ( 1 <_ t \/ t <_ 1 ) -> ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. \/ ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) ) )
409	280 408	mpd	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. \/ ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) )
410		opeq2	|- ( p = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> <. Z , p >. = <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. )
411	410	breq2d	|- ( p = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( U Btwn <. Z , p >. <-> U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. ) )
412		breq1	|- ( p = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( p Btwn <. Z , U >. <-> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) )
413	411 412	orbi12d	|- ( p = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) <-> ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. \/ ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) ) )
414	413 1	elrab2	|- ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. D <-> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. ( EE ` N ) /\ ( U Btwn <. Z , ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) >. \/ ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) Btwn <. Z , U >. ) ) )
415	277 409 414	sylanbrc	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. D )
416		fveq1	|- ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( x ` i ) = ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) )
417	416	eqeq1d	|- ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
418	417	ralbidv	|- ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
419	418	rspcev	|- ( ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) e. D /\ A. i e. ( 1 ... N ) ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - t ) x. ( Z ` k ) ) + ( t x. ( U ` k ) ) ) ) ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> E. x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
420	415 392 419	sylancl	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> E. x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) )
421	7	simplbi	|- ( x e. D -> x e. ( EE ` N ) )
422	1	ssrab3	|- D C_ ( EE ` N )
423	422	sseli	|- ( y e. D -> y e. ( EE ` N ) )
424	421 423	anim12i	|- ( ( x e. D /\ y e. D ) -> ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) )
425		r19.26	|- ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
426		eqtr3	|- ( ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> ( x ` i ) = ( y ` i ) )
427	426	ralimi	|- ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( x ` i ) = ( y ` i ) )
428	425 427	sylbir	|- ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( x ` i ) = ( y ` i ) )
429		eqeefv	|- ( ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) -> ( x = y <-> A. i e. ( 1 ... N ) ( x ` i ) = ( y ` i ) ) )
430	429	adantl	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( x = y <-> A. i e. ( 1 ... N ) ( x ` i ) = ( y ` i ) ) )
431	428 430	imbitrrid	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) )
432	424 431	sylan2	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( x e. D /\ y e. D ) ) -> ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) )
433	432	ralrimivva	|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> A. x e. D A. y e. D ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) )
434	433	adantr	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> A. x e. D A. y e. D ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) )
435		df-reu	|- ( E! x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> E! x ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
436		fveq1	|- ( x = y -> ( x ` i ) = ( y ` i ) )
437	436	eqeq1d	|- ( x = y -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
438	437	ralbidv	|- ( x = y -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
439	438	reu4	|- ( E! x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( E. x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. x e. D A. y e. D ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) ) )
440	435 439	bitr3i	|- ( E! x ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> ( E. x e. D A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. x e. D A. y e. D ( ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) /\ A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) -> x = y ) ) )
441	420 434 440	sylanbrc	|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ t e. ( 0 [,) +oo ) ) -> E! x ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
442	441	ralrimiva	|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> A. t e. ( 0 [,) +oo ) E! x ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
443		an12	|- ( ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) <-> ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
444	443	opabbii	|- { <. x , t >. | ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) } = { <. x , t >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
445	2 444	eqtri	|- F = { <. x , t >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
446	445	cnveqi	|- `' F = `' { <. x , t >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
447		cnvopab	|- `' { <. x , t >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) } = { <. t , x >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
448	446 447	eqtri	|- `' F = { <. t , x >. | ( t e. ( 0 [,) +oo ) /\ ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
449	448	fnopabg	|- ( A. t e. ( 0 [,) +oo ) E! x ( x e. D /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> `' F Fn ( 0 [,) +oo ) )
450	442 449	sylib	|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> `' F Fn ( 0 [,) +oo ) )
451		dff1o4	|- ( F : D -1-1-onto-> ( 0 [,) +oo ) <-> ( F Fn D /\ `' F Fn ( 0 [,) +oo ) ) )
452	256 450 451	sylanbrc	|- ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F : D -1-1-onto-> ( 0 [,) +oo ) )