Metamath Proof Explorer

Theorem axpasch

Description: The inner Pasch axiom. Take a triangle A C E , a point D on A C , and a point B extending C E . Then A E and D B intersect at some point x . Axiom A7 of Schwabhauser p. 12. (Contributed by Scott Fenton, 3-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 axpaschlem 
 |-  ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) )
2 1 3ad2ant3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) )
3 simp1 
 |-  ( ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> q = ( ( 1 - r ) x. ( 1 - t ) ) )
4 3 oveq1d 
 |-  ( ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> ( q x. ( A ` i ) ) = ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) )
5 4 eqcomd 
 |-  ( ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) = ( q x. ( A ` i ) ) )
6 simp2 
 |-  ( ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> r = ( ( 1 - q ) x. ( 1 - s ) ) )
7 6 oveq1d 
 |-  ( ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> ( r x. ( B ` i ) ) = ( ( ( 1 - q ) x. ( 1 - s ) ) x. ( B ` i ) ) )
8 5 7 oveq12d 
 |-  ( ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> ( ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) + ( r x. ( B ` i ) ) ) = ( ( q x. ( A ` i ) ) + ( ( ( 1 - q ) x. ( 1 - s ) ) x. ( B ` i ) ) ) )
9 simp3 
 |-  ( ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) )
10 9 oveq1d 
 |-  ( ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) = ( ( ( 1 - q ) x. s ) x. ( C ` i ) ) )
11 8 10 oveq12d 
 |-  ( ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> ( ( ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) + ( r x. ( B ` i ) ) ) + ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) ) = ( ( ( q x. ( A ` i ) ) + ( ( ( 1 - q ) x. ( 1 - s ) ) x. ( B ` i ) ) ) + ( ( ( 1 - q ) x. s ) x. ( C ` i ) ) ) )
12 11 3ad2ant3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) -> ( ( ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) + ( r x. ( B ` i ) ) ) + ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) ) = ( ( ( q x. ( A ` i ) ) + ( ( ( 1 - q ) x. ( 1 - s ) ) x. ( B ` i ) ) ) + ( ( ( 1 - q ) x. s ) x. ( C ` i ) ) ) )
13 12 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) + ( r x. ( B ` i ) ) ) + ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) ) = ( ( ( q x. ( A ` i ) ) + ( ( ( 1 - q ) x. ( 1 - s ) ) x. ( B ` i ) ) ) + ( ( ( 1 - q ) x. s ) x. ( C ` i ) ) ) )
14 1re 
 |-  1 e. RR
15 simpl2l 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> r e. ( 0 [,] 1 ) )
16 elicc01 
 |-  ( r e. ( 0 [,] 1 ) <-> ( r e. RR /\ 0 <_ r /\ r <_ 1 ) )
17 16 simp1bi 
 |-  ( r e. ( 0 [,] 1 ) -> r e. RR )
18 15 17 syl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> r e. RR )
19 resubcl 
 |-  ( ( 1 e. RR /\ r e. RR ) -> ( 1 - r ) e. RR )
20 14 18 19 sylancr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - r ) e. RR )
21 20 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - r ) e. CC )
22 simp13l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) -> t e. ( 0 [,] 1 ) )
23 22 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> t e. ( 0 [,] 1 ) )
24 elicc01 
 |-  ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
25 24 simp1bi 
 |-  ( t e. ( 0 [,] 1 ) -> t e. RR )
26 23 25 syl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> t e. RR )
27 resubcl 
 |-  ( ( 1 e. RR /\ t e. RR ) -> ( 1 - t ) e. RR )
28 14 26 27 sylancr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - t ) e. RR )
29 simp121 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) -> A e. ( EE ` N ) )
30 fveere 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
31 29 30 sylan 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. RR )
32 28 31 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - t ) x. ( A ` i ) ) e. RR )
33 32 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - t ) x. ( A ` i ) ) e. CC )
34 simp123 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) -> C e. ( EE ` N ) )
35 fveere 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. RR )
36 34 35 sylan 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. RR )
37 26 36 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( t x. ( C ` i ) ) e. RR )
38 37 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( t x. ( C ` i ) ) e. CC )
39 21 33 38 adddid 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) = ( ( ( 1 - r ) x. ( ( 1 - t ) x. ( A ` i ) ) ) + ( ( 1 - r ) x. ( t x. ( C ` i ) ) ) ) )
40 28 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - t ) e. CC )
41 31 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
42 21 40 41 mulassd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) = ( ( 1 - r ) x. ( ( 1 - t ) x. ( A ` i ) ) ) )
43 26 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> t e. CC )
44 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
45 34 44 sylan 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
46 21 43 45 mulassd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) = ( ( 1 - r ) x. ( t x. ( C ` i ) ) ) )
47 42 46 oveq12d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) + ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) ) = ( ( ( 1 - r ) x. ( ( 1 - t ) x. ( A ` i ) ) ) + ( ( 1 - r ) x. ( t x. ( C ` i ) ) ) ) )
48 39 47 eqtr4d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) = ( ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) + ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) ) )
49 48 oveq1d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) + ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) ) + ( r x. ( B ` i ) ) ) )
50 20 28 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - r ) x. ( 1 - t ) ) e. RR )
51 50 31 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) e. RR )
52 51 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) e. CC )
53 20 26 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - r ) x. t ) e. RR )
54 53 36 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) e. RR )
55 54 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) e. CC )
56 simp122 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) -> B e. ( EE ` N ) )
57 fveere 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
58 56 57 sylan 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. RR )
59 18 58 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( r x. ( B ` i ) ) e. RR )
60 59 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( r x. ( B ` i ) ) e. CC )
61 52 55 60 add32d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) + ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) + ( r x. ( B ` i ) ) ) + ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) ) )
62 49 61 eqtrd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( ( ( 1 - r ) x. ( 1 - t ) ) x. ( A ` i ) ) + ( r x. ( B ` i ) ) ) + ( ( ( 1 - r ) x. t ) x. ( C ` i ) ) ) )
63 simpl2r 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> q e. ( 0 [,] 1 ) )
64 elicc01 
 |-  ( q e. ( 0 [,] 1 ) <-> ( q e. RR /\ 0 <_ q /\ q <_ 1 ) )
65 64 simp1bi 
 |-  ( q e. ( 0 [,] 1 ) -> q e. RR )
66 63 65 syl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> q e. RR )
67 resubcl 
 |-  ( ( 1 e. RR /\ q e. RR ) -> ( 1 - q ) e. RR )
68 14 66 67 sylancr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - q ) e. RR )
69 simp13r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) -> s e. ( 0 [,] 1 ) )
70 69 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> s e. ( 0 [,] 1 ) )
71 elicc01 
 |-  ( s e. ( 0 [,] 1 ) <-> ( s e. RR /\ 0 <_ s /\ s <_ 1 ) )
72 71 simp1bi 
 |-  ( s e. ( 0 [,] 1 ) -> s e. RR )
73 70 72 syl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> s e. RR )
74 resubcl 
 |-  ( ( 1 e. RR /\ s e. RR ) -> ( 1 - s ) e. RR )
75 14 73 74 sylancr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - s ) e. RR )
76 75 58 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - s ) x. ( B ` i ) ) e. RR )
77 68 76 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - q ) x. ( ( 1 - s ) x. ( B ` i ) ) ) e. RR )
78 77 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - q ) x. ( ( 1 - s ) x. ( B ` i ) ) ) e. CC )
79 73 36 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( s x. ( C ` i ) ) e. RR )
80 68 79 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - q ) x. ( s x. ( C ` i ) ) ) e. RR )
81 80 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - q ) x. ( s x. ( C ` i ) ) ) e. CC )
82 66 31 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( q x. ( A ` i ) ) e. RR )
83 82 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( q x. ( A ` i ) ) e. CC )
84 78 81 83 add32d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 - q ) x. ( ( 1 - s ) x. ( B ` i ) ) ) + ( ( 1 - q ) x. ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) = ( ( ( ( 1 - q ) x. ( ( 1 - s ) x. ( B ` i ) ) ) + ( q x. ( A ` i ) ) ) + ( ( 1 - q ) x. ( s x. ( C ` i ) ) ) ) )
85 68 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - q ) e. CC )
86 76 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - s ) x. ( B ` i ) ) e. CC )
87 79 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( s x. ( C ` i ) ) e. CC )
88 85 86 87 adddid 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) = ( ( ( 1 - q ) x. ( ( 1 - s ) x. ( B ` i ) ) ) + ( ( 1 - q ) x. ( s x. ( C ` i ) ) ) ) )
89 88 oveq1d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) = ( ( ( ( 1 - q ) x. ( ( 1 - s ) x. ( B ` i ) ) ) + ( ( 1 - q ) x. ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) )
90 75 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( 1 - s ) e. CC )
91 58 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
92 85 90 91 mulassd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - q ) x. ( 1 - s ) ) x. ( B ` i ) ) = ( ( 1 - q ) x. ( ( 1 - s ) x. ( B ` i ) ) ) )
93 92 oveq2d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( q x. ( A ` i ) ) + ( ( ( 1 - q ) x. ( 1 - s ) ) x. ( B ` i ) ) ) = ( ( q x. ( A ` i ) ) + ( ( 1 - q ) x. ( ( 1 - s ) x. ( B ` i ) ) ) ) )
94 83 78 93 comraddd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( q x. ( A ` i ) ) + ( ( ( 1 - q ) x. ( 1 - s ) ) x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( 1 - s ) x. ( B ` i ) ) ) + ( q x. ( A ` i ) ) ) )
95 73 recnd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> s e. CC )
96 85 95 45 mulassd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - q ) x. s ) x. ( C ` i ) ) = ( ( 1 - q ) x. ( s x. ( C ` i ) ) ) )
97 94 96 oveq12d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( q x. ( A ` i ) ) + ( ( ( 1 - q ) x. ( 1 - s ) ) x. ( B ` i ) ) ) + ( ( ( 1 - q ) x. s ) x. ( C ` i ) ) ) = ( ( ( ( 1 - q ) x. ( ( 1 - s ) x. ( B ` i ) ) ) + ( q x. ( A ` i ) ) ) + ( ( 1 - q ) x. ( s x. ( C ` i ) ) ) ) )
98 84 89 97 3eqtr4d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) = ( ( ( q x. ( A ` i ) ) + ( ( ( 1 - q ) x. ( 1 - s ) ) x. ( B ` i ) ) ) + ( ( ( 1 - q ) x. s ) x. ( C ` i ) ) ) )
99 13 62 98 3eqtr4d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) )
100 99 ralrimiva 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) /\ ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) ) -> A. i e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) )
101 100 3expia 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) -> ( ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> A. i e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
102 101 reximdvva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( q = ( ( 1 - r ) x. ( 1 - t ) ) /\ r = ( ( 1 - q ) x. ( 1 - s ) ) /\ ( ( 1 - r ) x. t ) = ( ( 1 - q ) x. s ) ) -> E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
103 2 102 mpd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) )
104 simplrl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> r e. ( 0 [,] 1 ) )
105 104 17 syl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> r e. RR )
106 14 105 19 sylancr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( 1 - r ) e. RR )
107 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) -> t e. ( 0 [,] 1 ) )
108 107 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> t e. ( 0 [,] 1 ) )
109 108 25 syl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> t e. RR )
110 14 109 27 sylancr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( 1 - t ) e. RR )
111 simpl21 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) -> A e. ( EE ` N ) )
112 fveere 
 |-  ( ( A e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. RR )
113 111 112 sylan 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. RR )
114 110 113 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( ( 1 - t ) x. ( A ` k ) ) e. RR )
115 simpl23 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) -> C e. ( EE ` N ) )
116 fveere 
 |-  ( ( C e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( C ` k ) e. RR )
117 115 116 sylan 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( C ` k ) e. RR )
118 109 117 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( t x. ( C ` k ) ) e. RR )
119 114 118 readdcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) e. RR )
120 106 119 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) e. RR )
121 simpl22 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) -> B e. ( EE ` N ) )
122 fveere 
 |-  ( ( B e. ( EE ` N ) /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. RR )
123 121 122 sylan 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( B ` k ) e. RR )
124 105 123 remulcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( r x. ( B ` k ) ) e. RR )
125 120 124 readdcld 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) /\ k e. ( 1 ... N ) ) -> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) e. RR )
126 125 ralrimiva 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ ( r e. ( 0 [,] 1 ) /\ q e. ( 0 [,] 1 ) ) ) -> A. k e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) e. RR )
127 126 anassrs 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ r e. ( 0 [,] 1 ) ) /\ q e. ( 0 [,] 1 ) ) -> A. k e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) e. RR )
128 simpll1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ r e. ( 0 [,] 1 ) ) /\ q e. ( 0 [,] 1 ) ) -> N e. NN )
129 mptelee 
 |-  ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) e. RR ) )
130 128 129 syl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ r e. ( 0 [,] 1 ) ) /\ q e. ( 0 [,] 1 ) ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) e. RR ) )
131 127 130 mpbird 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ r e. ( 0 [,] 1 ) ) /\ q e. ( 0 [,] 1 ) ) -> ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) e. ( EE ` N ) )
132 fveq1 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) -> ( x ` i ) = ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) ` i ) )
133 fveq2 
 |-  ( k = i -> ( A ` k ) = ( A ` i ) )
134 133 oveq2d 
 |-  ( k = i -> ( ( 1 - t ) x. ( A ` k ) ) = ( ( 1 - t ) x. ( A ` i ) ) )
135 fveq2 
 |-  ( k = i -> ( C ` k ) = ( C ` i ) )
136 135 oveq2d 
 |-  ( k = i -> ( t x. ( C ` k ) ) = ( t x. ( C ` i ) ) )
137 134 136 oveq12d 
 |-  ( k = i -> ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) )
138 137 oveq2d 
 |-  ( k = i -> ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) = ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) )
139 fveq2 
 |-  ( k = i -> ( B ` k ) = ( B ` i ) )
140 139 oveq2d 
 |-  ( k = i -> ( r x. ( B ` k ) ) = ( r x. ( B ` i ) ) )
141 138 140 oveq12d 
 |-  ( k = i -> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) )
142 eqid 
 |-  ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) = ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) )
143 ovex 
 |-  ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) e. _V
144 141 142 143 fvmpt 
 |-  ( i e. ( 1 ... N ) -> ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) )
145 132 144 sylan9eq 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) )
146 145 eqeq1d 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) <-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) ) )
147 145 eqeq1d 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) <-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
148 146 147 anbi12d 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) <-> ( ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
149 eqid 
 |-  ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) )
150 149 biantrur 
 |-  ( ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) <-> ( ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
151 148 150 bitr4di 
 |-  ( ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) <-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
152 151 ralbidva 
 |-  ( x = ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) -> ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
153 152 rspcev 
 |-  ( ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) e. ( EE ` N ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) -> E. x e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
154 153 ex 
 |-  ( ( k e. ( 1 ... N ) |-> ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` k ) ) + ( t x. ( C ` k ) ) ) ) + ( r x. ( B ` k ) ) ) ) e. ( EE ` N ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) -> E. x e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
155 131 154 syl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ r e. ( 0 [,] 1 ) ) /\ q e. ( 0 [,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) -> E. x e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
156 155 reximdva 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ r e. ( 0 [,] 1 ) ) -> ( E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) -> E. q e. ( 0 [,] 1 ) E. x e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
157 156 reximdva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) -> E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) E. x e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
158 103 157 mpd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) E. x e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
159 rexcom 
 |-  ( E. q e. ( 0 [,] 1 ) E. x e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
160 159 rexbii 
 |-  ( E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) E. x e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) <-> E. r e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
161 rexcom 
 |-  ( E. r e. ( 0 [,] 1 ) E. x e. ( EE ` N ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
162 160 161 bitri 
 |-  ( E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) E. x e. ( EE ` N ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
163 158 162 sylib 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
164 oveq2 
 |-  ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) -> ( ( 1 - r ) x. ( D ` i ) ) = ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) )
165 164 oveq1d 
 |-  ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) -> ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) )
166 165 eqeq2d 
 |-  ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) -> ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) ) )
167 oveq2 
 |-  ( ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) -> ( ( 1 - q ) x. ( E ` i ) ) = ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) )
168 167 oveq1d 
 |-  ( ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) -> ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) )
169 168 eqeq2d 
 |-  ( ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) -> ( ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) )
170 166 169 bi2anan9 
 |-  ( ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) -> ( ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
171 170 ralimi 
 |-  ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
172 ralbi 
 |-  ( A. i e. ( 1 ... N ) ( ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) -> ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
173 171 172 syl 
 |-  ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) -> ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
174 173 rexbidv 
 |-  ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) -> ( E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
175 174 2rexbidv 
 |-  ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) -> ( E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) + ( q x. ( A ` i ) ) ) ) ) )
176 163 175 syl5ibrcom 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) -> E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) ) )
177 176 3expia 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) -> E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) ) ) )
178 177 rexlimdvv 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) -> E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) ) )
179 178 3adant3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) -> E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) ) )
180 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
181 simp21 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
182 simp23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
183 brbtwn 
 |-  ( ( D e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( D Btwn <. A , C >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) )
184 180 181 182 183 syl3anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( D Btwn <. A , C >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) )
185 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
186 simp22 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
187 brbtwn 
 |-  ( ( E e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( E Btwn <. B , C >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) )
188 185 186 182 187 syl3anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( E Btwn <. B , C >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) )
189 184 188 anbi12d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , C >. /\ E Btwn <. B , C >. ) <-> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) ) )
190 r19.26 
 |-  ( A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) <-> ( A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) )
191 190 2rexbii 
 |-  ( E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) <-> E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) )
192 reeanv 
 |-  ( E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) <-> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) )
193 191 192 bitri 
 |-  ( E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) <-> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) )
194 189 193 bitr4di 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , C >. /\ E Btwn <. B , C >. ) <-> E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( D ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ ( E ` i ) = ( ( ( 1 - s ) x. ( B ` i ) ) + ( s x. ( C ` i ) ) ) ) ) )
195 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
196 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> D e. ( EE ` N ) )
197 simpl22 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> B e. ( EE ` N ) )
198 brbtwn 
 |-  ( ( x e. ( EE ` N ) /\ D e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( x Btwn <. D , B >. <-> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) ) )
199 195 196 197 198 syl3anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. D , B >. <-> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) ) )
200 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> E e. ( EE ` N ) )
201 simpl21 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> A e. ( EE ` N ) )
202 brbtwn 
 |-  ( ( x e. ( EE ` N ) /\ E e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( x Btwn <. E , A >. <-> E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) )
203 195 200 201 202 syl3anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( x Btwn <. E , A >. <-> E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) )
204 199 203 anbi12d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( x Btwn <. D , B >. /\ x Btwn <. E , A >. ) <-> ( E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) ) )
205 r19.26 
 |-  ( A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) )
206 205 2rexbii 
 |-  ( E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) )
207 reeanv 
 |-  ( E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> ( E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) )
208 206 207 bitri 
 |-  ( E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) <-> ( E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) )
209 204 208 bitr4di 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( x Btwn <. D , B >. /\ x Btwn <. E , A >. ) <-> E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) ) )
210 209 rexbidva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( E. x e. ( EE ` N ) ( x Btwn <. D , B >. /\ x Btwn <. E , A >. ) <-> E. x e. ( EE ` N ) E. r e. ( 0 [,] 1 ) E. q e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( x ` i ) = ( ( ( 1 - r ) x. ( D ` i ) ) + ( r x. ( B ` i ) ) ) /\ ( x ` i ) = ( ( ( 1 - q ) x. ( E ` i ) ) + ( q x. ( A ` i ) ) ) ) ) )
211 179 194 210 3imtr4d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , C >. /\ E Btwn <. B , C >. ) -> E. x e. ( EE ` N ) ( x Btwn <. D , B >. /\ x Btwn <. E , A >. ) ) )