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

Theorem axpasch 23944
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.)
Assertion
Ref Expression
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 >. ) ) )
Distinct variable groups:    x, A    x, B    x, C    x, D    x, E    x, N

Proof of Theorem axpasch
StepHypRef Expression
1 axpaschlem 23943 . . . . . . . . . 10  |-  ( ( 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 ) ) )
213ad2ant3 983 . . . . . . . . 9  |-  ( ( 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 960 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 ) ) )
43oveq1d 5807 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) )
54eqcomd 2263 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 961 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) )
76oveq1d 5807 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) )
85, 7oveq12d 5810 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 962 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) )
109oveq1d 5807 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) )
118, 10oveq12d 5810 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) ) ) )
12113ad2ant3 983 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
1312adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 8805 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  RR
15 simpl2l 1013 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 0re 8806 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  RR
1716, 14elicc2i 10682 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( r  e.  ( 0 [,] 1 )  <->  ( r  e.  RR  /\  0  <_ 
r  /\  r  <_  1 ) )
1817simp1bi 975 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( r  e.  ( 0 [,] 1 )  ->  r  e.  RR )
1915, 18syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 )
20 resubcl 9079 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  RR  /\  r  e.  RR )  ->  ( 1  -  r
)  e.  RR )
2114, 19, 20sylancr 647 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
2221recnd 8829 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
23 simp13l 1075 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) )
2423adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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
) )
2516, 14elicc2i 10682 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  ( 0 [,] 1 )  <->  ( t  e.  RR  /\  0  <_ 
t  /\  t  <_  1 ) )
2625simp1bi 975 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  RR )
2724, 26syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 )
28 resubcl 9079 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  e.  RR  /\  t  e.  RR )  ->  ( 1  -  t
)  e.  RR )
2914, 27, 28sylancr 647 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 )
30 simp121 1092 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) )
31 fveere 23904 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( A `  i )  e.  RR )
3230, 31sylan 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 )
3329, 32remulcld 8831 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
3433recnd 8829 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
35 simp123 1094 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) )
36 fveere 23904 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  RR )
3735, 36sylan 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 )
3827, 37remulcld 8831 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
3938recnd 8829 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
4022, 34, 39adddid 8827 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 ) ) ) ) )
4129recnd 8829 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
4232recnd 8829 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
4322, 41, 42mulassd 8826 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 ) ) ) )
4427recnd 8829 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
45 fveecn 23905 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( C  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( C `  i )  e.  CC )
4635, 45sylan 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
4722, 44, 46mulassd 8826 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 ) ) ) )
4843, 47oveq12d 5810 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 ) ) ) ) )
4940, 48eqtr4d 2293 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) ) )
5049oveq1d 5807 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) ) ) )
5121, 29remulcld 8831 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
5251, 32remulcld 8831 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
5352recnd 8829 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
5421, 27remulcld 8831 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
5554, 37remulcld 8831 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
5655recnd 8829 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
57 simp122 1093 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) )
58 fveere 23904 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( B  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( B `  i )  e.  RR )
5957, 58sylan 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
6019, 59remulcld 8831 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
6160recnd 8829 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
6253, 56, 61add32d 9002 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) ) ) )
6350, 62eqtrd 2290 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) ) ) )
64 simpl2r 1014 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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
) )
6516, 14elicc2i 10682 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( q  e.  ( 0 [,] 1 )  <->  ( q  e.  RR  /\  0  <_ 
q  /\  q  <_  1 ) )
6665simp1bi 975 . . . . . . . . . . . . . . . . . . . . 21  |-  ( q  e.  ( 0 [,] 1 )  ->  q  e.  RR )
6764, 66syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
68 resubcl 9079 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  RR  /\  q  e.  RR )  ->  ( 1  -  q
)  e.  RR )
6914, 67, 68sylancr 647 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
70 simp13r 1076 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) )
7170adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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
) )
7216, 14elicc2i 10682 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  e.  ( 0 [,] 1 )  <->  ( s  e.  RR  /\  0  <_ 
s  /\  s  <_  1 ) )
7372simp1bi 975 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  e.  ( 0 [,] 1 )  ->  s  e.  RR )
7471, 73syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 )
75 resubcl 9079 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  RR  /\  s  e.  RR )  ->  ( 1  -  s
)  e.  RR )
7614, 74, 75sylancr 647 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
7776, 59remulcld 8831 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
7869, 77remulcld 8831 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
7978recnd 8829 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
8074, 37remulcld 8831 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
8169, 80remulcld 8831 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
8281recnd 8829 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
8367, 32remulcld 8831 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
8483recnd 8829 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
8579, 82, 84add32d 9002 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) ) ) ) )
8669recnd 8829 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
8777recnd 8829 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
8880recnd 8829 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
8986, 87, 88adddid 8827 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) ) ) )
9089oveq1d 5807 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) ) ) )
9176recnd 8829 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
9259recnd 8829 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 )
9386, 91, 92mulassd 8826 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 ) ) ) )
9493oveq2d 5808 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 ) ) ) ) )
9584, 79addcomd 8982 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 ) ) ) )
9694, 95eqtrd 2290 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) ) )
9774recnd 8829 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
9886, 97, 46mulassd 8826 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) ) )
9996, 98oveq12d 5810 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) ) ) ) )
10085, 90, 993eqtr4d 2300 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) ) ) )
10113, 63, 1003eqtr4d 2300 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) ) )
102101ralrimiva 2601 . . . . . . . . . . . . 13  |-  ( ( ( 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
) ) ) )
1031023expia 1158 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) ) )
104103anassrs 632 . . . . . . . . . . 11  |-  ( ( ( ( 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
) ) ) ) )
105104reximdva 2630 . . . . . . . . . 10  |-  ( ( ( 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
) ( q  =  ( ( 1  -  r )  x.  (
1  -  t ) )  /\  r  =  ( ( 1  -  q )  x.  (
1  -  s ) )  /\  ( ( 1  -  r )  x.  t )  =  ( ( 1  -  q )  x.  s
) )  ->  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 ) ) ) ) )
106105reximdva 2630 . . . . . . . . 9  |-  ( ( 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
) ) ) ) )
1072, 106mpd 16 . . . . . . . 8  |-  ( ( 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 ) ) ) )
108 simplrl 739 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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
) )
109108, 18syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
11014, 109, 20sylancr 647 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 )
111 simpl3l 1015 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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
) )
112111adantr 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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
) )
113112, 26syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
11414, 113, 28sylancr 647 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
115 simpl21 1038 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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
) )
116 fveere 23904 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( A `  k )  e.  RR )
117115, 116sylan 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
118114, 117remulcld 8831 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
119 simpl23 1040 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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
) )
120 fveere 23904 . . . . . . . . . . . . . . . . . . 19  |-  ( ( C  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( C `  k )  e.  RR )
121119, 120sylan 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
122113, 121remulcld 8831 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
123118, 122readdcld 8830 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 )
124110, 123remulcld 8831 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
125 simpl22 1039 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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
) )
126 fveere 23904 . . . . . . . . . . . . . . . . 17  |-  ( ( B  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( B `  k )  e.  RR )
127125, 126sylan 459 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 )
128109, 127remulcld 8831 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
129124, 128readdcld 8830 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
130129ralrimiva 2601 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
131130anassrs 632 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
132 simpll1 999 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
133 mptelee 23898 . . . . . . . . . . . . 13  |-  ( 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 ) )
134132, 133syl 17 . . . . . . . . . . . 12  |-  ( ( ( ( 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.  (