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

Theorem axcontlem4 24667
Description: Lemma for axcont 24676. Given the separation assumption,  A is a subset of  D. (Contributed by Scott Fenton, 18-Jun-2013.)
Hypothesis
Ref Expression
axcontlem4.1  |-  D  =  { p  e.  ( EE `  N )  |  ( U  Btwn  <. Z ,  p >.  \/  p  Btwn  <. Z ,  U >. ) }
Assertion
Ref Expression
axcontlem4  |-  ( ( ( N  e.  NN  /\  ( A  C_  ( EE `  N )  /\  B  C_  ( EE `  N )  /\  A. x  e.  A  A. y  e.  B  x  Btwn  <. Z ,  y
>. ) )  /\  (
( Z  e.  ( EE `  N )  /\  U  e.  A  /\  B  =/=  (/) )  /\  Z  =/=  U ) )  ->  A  C_  D
)
Distinct variable groups:    A, p, x    B, p, x, y    N, p, x, y    U, p, x, y    Z, p, x, y
Allowed substitution hints:    A( y)    D( x, y, p)

Proof of Theorem axcontlem4
Dummy variables  b 
i  r  t  s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr1 997 . 2  |-  ( ( ( N  e.  NN  /\  ( A  C_  ( EE `  N )  /\  B  C_  ( EE `  N )  /\  A. x  e.  A  A. y  e.  B  x  Btwn  <. Z ,  y
>. ) )  /\  (
( Z  e.  ( EE `  N )  /\  U  e.  A  /\  B  =/=  (/) )  /\  Z  =/=  U ) )  ->  A  C_  ( EE `  N ) )
2 n0 3477 . . . . . 6  |-  ( B  =/=  (/)  <->  E. b  b  e.  B )
3 idd 21 . . . . . . . . . 10  |-  ( b  e.  B  ->  ( A  C_  ( EE `  N )  ->  A  C_  ( EE `  N
) ) )
4 ssel 3187 . . . . . . . . . . 11  |-  ( B 
C_  ( EE `  N )  ->  (
b  e.  B  -> 
b  e.  ( EE
`  N ) ) )
54com12 27 . . . . . . . . . 10  |-  ( b  e.  B  ->  ( B  C_  ( EE `  N )  ->  b  e.  ( EE `  N
) ) )
6 opeq2 3813 . . . . . . . . . . . . 13  |-  ( y  =  b  ->  <. Z , 
y >.  =  <. Z , 
b >. )
76breq2d 4051 . . . . . . . . . . . 12  |-  ( y  =  b  ->  (
x  Btwn  <. Z , 
y >. 
<->  x  Btwn  <. Z , 
b >. ) )
87rspcv 2893 . . . . . . . . . . 11  |-  ( b  e.  B  ->  ( A. y  e.  B  x  Btwn  <. Z ,  y
>.  ->  x  Btwn  <. Z , 
b >. ) )
98ralimdv 2635 . . . . . . . . . 10  |-  ( b  e.  B  ->  ( A. x  e.  A  A. y  e.  B  x  Btwn  <. Z ,  y
>.  ->  A. x  e.  A  x  Btwn  <. Z ,  b
>. ) )
103, 5, 93anim123d 1259 . . . . . . . . 9  |-  ( b  e.  B  ->  (
( A  C_  ( EE `  N )  /\  B  C_  ( EE `  N )  /\  A. x  e.  A  A. y  e.  B  x  Btwn  <. Z ,  y
>. )  ->  ( A 
C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) ) )
1110anim2d 548 . . . . . . . 8  |-  ( b  e.  B  ->  (
( N  e.  NN  /\  ( A  C_  ( EE `  N )  /\  B  C_  ( EE `  N )  /\  A. x  e.  A  A. y  e.  B  x  Btwn  <. Z ,  y
>. ) )  ->  ( N  e.  NN  /\  ( A  C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) ) ) )
12 simplr1 997 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN  /\  ( A  C_  ( EE `  N )  /\  b  e.  ( EE `  N )  /\  A. x  e.  A  x  Btwn  <. Z ,  b
>. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  ->  A  C_  ( EE `  N ) )
1312adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( A 
C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  /\  p  e.  A )  ->  A  C_  ( EE `  N ) )
14 simplr2 998 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  ( A 
C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  /\  p  e.  A )  ->  U  e.  A )
1513, 14sseldd 3194 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( A 
C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  /\  p  e.  A )  ->  U  e.  ( EE
`  N ) )
16 simpr3 963 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  ( A  C_  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  A. x  e.  A  x  Btwn  <. Z ,  b
>. ) )  ->  A. x  e.  A  x  Btwn  <. Z ,  b >. )
17 simp2 956 . . . . . . . . . . . . . . . 16  |-  ( ( Z  e.  ( EE
`  N )  /\  U  e.  A  /\  Z  =/=  U )  ->  U  e.  A )
18 breq1 4042 . . . . . . . . . . . . . . . . 17  |-  ( x  =  U  ->  (
x  Btwn  <. Z , 
b >. 
<->  U  Btwn  <. Z , 
b >. ) )
1918rspccva 2896 . . . . . . . . . . . . . . . 16  |-  ( ( A. x  e.  A  x  Btwn  <. Z ,  b
>.  /\  U  e.  A
)  ->  U  Btwn  <. Z ,  b >. )
2016, 17, 19syl2an 463 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  ( A  C_  ( EE `  N )  /\  b  e.  ( EE `  N )  /\  A. x  e.  A  x  Btwn  <. Z ,  b
>. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  ->  U  Btwn  <. Z ,  b
>. )
2120adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  ( A 
C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  /\  p  e.  A )  ->  U  Btwn  <. Z , 
b >. )
2215, 21jca 518 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( A 
C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  /\  p  e.  A )  ->  ( U  e.  ( EE `  N )  /\  U  Btwn  <. Z , 
b >. ) )
2312sselda 3193 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( A 
C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  /\  p  e.  A )  ->  p  e.  ( EE
`  N ) )
2416adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  ( A  C_  ( EE `  N )  /\  b  e.  ( EE `  N )  /\  A. x  e.  A  x  Btwn  <. Z ,  b
>. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  ->  A. x  e.  A  x  Btwn  <. Z ,  b
>. )
25 breq1 4042 . . . . . . . . . . . . . . 15  |-  ( x  =  p  ->  (
x  Btwn  <. Z , 
b >. 
<->  p  Btwn  <. Z , 
b >. ) )
2625rspccva 2896 . . . . . . . . . . . . . 14  |-  ( ( A. x  e.  A  x  Btwn  <. Z ,  b
>.  /\  p  e.  A
)  ->  p  Btwn  <. Z ,  b >. )
2724, 26sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( A 
C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  /\  p  e.  A )  ->  p  Btwn  <. Z , 
b >. )
2822, 23, 27jca32 521 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( A 
C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  /\  p  e.  A )  ->  ( ( U  e.  ( EE `  N
)  /\  U  Btwn  <. Z ,  b >. )  /\  ( p  e.  ( EE `  N
)  /\  p  Btwn  <. Z ,  b >. ) ) )
29 an4 797 . . . . . . . . . . . 12  |-  ( ( ( U  e.  ( EE `  N )  /\  U  Btwn  <. Z , 
b >. )  /\  (
p  e.  ( EE
`  N )  /\  p  Btwn  <. Z ,  b
>. ) )  <->  ( ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) )  /\  ( U  Btwn  <. Z ,  b
>.  /\  p  Btwn  <. Z , 
b >. ) ) )
3028, 29sylib 188 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( A 
C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. ) )  /\  ( Z  e.  ( EE `  N )  /\  U  e.  A  /\  Z  =/= 
U ) )  /\  p  e.  A )  ->  ( ( U  e.  ( EE `  N
)  /\  p  e.  ( EE `  N ) )  /\  ( U 
Btwn  <. Z ,  b
>.  /\  p  Btwn  <. Z , 
b >. ) ) )
31 simp2 956 . . . . . . . . . . . . . 14  |-  ( ( A  C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. )  ->  b  e.  ( EE `  N ) )
32 simpl2r 1009 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  ->  Z  =/=  U )
3332adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  /\  A. i  e.  ( 1 ... N ) ( ( U `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  /\  ( p `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) ) ) )  ->  Z  =/=  U )
34 simpl 443 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( U `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  /\  ( p `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) ) )  ->  ( U `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) ) )
3534ralimi 2631 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. i  e.  ( 1 ... N ) ( ( U `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  /\  ( p `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) ) )  ->  A. i  e.  ( 1 ... N ) ( U `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) ) )
36 eqcom 2298 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( U `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
b `  i )
) )  <->  ( (
( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  =  ( U `  i
) )
37 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( t  =  0  ->  (
1  -  t )  =  ( 1  -  0 ) )
38 ax-1cn 8811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  1  e.  CC
3938subid1i 9134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 1  -  0 )  =  1
4037, 39syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( t  =  0  ->  (
1  -  t )  =  1 )
4140oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( t  =  0  ->  (
( 1  -  t
)  x.  ( Z `
 i ) )  =  ( 1  x.  ( Z `  i
) ) )
42 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( t  =  0  ->  (
t  x.  ( b `
 i ) )  =  ( 0  x.  ( b `  i
) ) )
4341, 42oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  =  0  ->  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) )  =  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
b `  i )
) ) )
4443eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  0  ->  (
( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( b `
 i ) ) )  =  ( U `
 i )  <->  ( (
1  x.  ( Z `
 i ) )  +  ( 0  x.  ( b `  i
) ) )  =  ( U `  i
) ) )
4536, 44syl5bb 248 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  0  ->  (
( U `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  <->  ( (
1  x.  ( Z `
 i ) )  +  ( 0  x.  ( b `  i
) ) )  =  ( U `  i
) ) )
4645ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  0  ->  ( A. i  e.  (
1 ... N ) ( U `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
b `  i )
) )  <->  A. i  e.  ( 1 ... N
) ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
b `  i )
) )  =  ( U `  i ) ) )
4746biimpac 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A. i  e.  ( 1 ... N ) ( U `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  /\  t  =  0 )  ->  A. i  e.  ( 1 ... N ) ( ( 1  x.  ( Z `  i
) )  +  ( 0  x.  ( b `
 i ) ) )  =  ( U `
 i ) )
48 simpl2l 1008 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  ->  Z  e.  ( EE `  N
) )
49 simpl3l 1010 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  ->  U  e.  ( EE `  N
) )
50 eqeefv 24603 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  -> 
( Z  =  U  <->  A. i  e.  (
1 ... N ) ( Z `  i )  =  ( U `  i ) ) )
5148, 49, 50syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  ->  ( Z  =  U  <->  A. i  e.  ( 1 ... N
) ( Z `  i )  =  ( U `  i ) ) )
52 fveecn 24602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( Z  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( Z `  i )  e.  CC )
5348, 52sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( Z `  i )  e.  CC )
54 simp1r 980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( N  e.  NN  /\  b  e.  ( EE
`  N ) )  /\  ( Z  e.  ( EE `  N
)  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  -> 
b  e.  ( EE
`  N ) )
5554ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  /\  i  e.  ( 1 ... N
) )  ->  b  e.  ( EE `  N
) )
56 fveecn 24602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( b  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( b `  i )  e.  CC )
5755, 56sylancom 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  /\  i  e.  ( 1 ... N
) )  ->  (
b `  i )  e.  CC )
58 mulid2 8852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Z `  i )  e.  CC  ->  (
1  x.  ( Z `
 i ) )  =  ( Z `  i ) )
59 mul02 9006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( b `  i )  e.  CC  ->  (
0  x.  ( b `
 i ) )  =  0 )
6058, 59oveqan12d 5893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( Z `  i
)  e.  CC  /\  ( b `  i
)  e.  CC )  ->  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
b `  i )
) )  =  ( ( Z `  i
)  +  0 ) )
61 addid1 9008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Z `  i )  e.  CC  ->  (
( Z `  i
)  +  0 )  =  ( Z `  i ) )
6261adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( Z `  i
)  e.  CC  /\  ( b `  i
)  e.  CC )  ->  ( ( Z `
 i )  +  0 )  =  ( Z `  i ) )
6360, 62eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( Z `  i
)  e.  CC  /\  ( b `  i
)  e.  CC )  ->  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
b `  i )
) )  =  ( Z `  i ) )
6453, 57, 63syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( 1  x.  ( Z `  i )
)  +  ( 0  x.  ( b `  i ) ) )  =  ( Z `  i ) )
6564eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( 1  x.  ( Z `  i
) )  +  ( 0  x.  ( b `
 i ) ) )  =  ( U `
 i )  <->  ( Z `  i )  =  ( U `  i ) ) )
6665ralbidva 2572 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  ->  ( A. i  e.  (
1 ... N ) ( ( 1  x.  ( Z `  i )
)  +  ( 0  x.  ( b `  i ) ) )  =  ( U `  i )  <->  A. i  e.  ( 1 ... N
) ( Z `  i )  =  ( U `  i ) ) )
6751, 66bitr4d 247 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  ->  ( Z  =  U  <->  A. i  e.  ( 1 ... N
) ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
b `  i )
) )  =  ( U `  i ) ) )
6847, 67syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  ->  (
( A. i  e.  ( 1 ... N
) ( U `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) )  /\  t  =  0 )  ->  Z  =  U ) )
6968expdimp 426 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  /\  A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
b `  i )
) ) )  -> 
( t  =  0  ->  Z  =  U ) )
7035, 69sylan2 460 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  /\  A. i  e.  ( 1 ... N ) ( ( U `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  /\  ( p `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) ) ) )  ->  ( t  =  0  ->  Z  =  U ) )
7170necon3d 2497 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  /\  A. i  e.  ( 1 ... N ) ( ( U `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  /\  ( p `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) ) ) )  ->  ( Z  =/=  U  ->  t  =/=  0 ) )
7233, 71mpd 14 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( N  e.  NN  /\  b  e.  ( EE `  N
) )  /\  ( Z  e.  ( EE `  N )  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) ) )  /\  A. i  e.  ( 1 ... N ) ( ( U `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  /\  ( p `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) ) ) )  ->  t  =/=  0 )
73 simp1l 979 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( N  e.  NN  /\  b  e.  ( EE
`  N ) )  /\  ( Z  e.  ( EE `  N
)  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  ->  N  e.  NN )
74 simp2l 981 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( N  e.  NN  /\  b  e.  ( EE
`  N ) )  /\  ( Z  e.  ( EE `  N
)  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  ->  Z  e.  ( EE `  N ) )
7573, 74, 543jca 1132 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  e.  NN  /\  b  e.  ( EE
`  N ) )  /\  ( Z  e.  ( EE `  N
)  /\  Z  =/=  U )  /\  ( U  e.  ( EE `  N )  /\  p  e.  ( EE `  N
) ) )  -> 
( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) ) )
76 simp2l 981 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  t  e.  ( 0 [,] 1
) )
77 0re 8854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  0  e.  RR
78 1re 8853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  1  e.  RR
7977, 78elicc2i 10732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  e.  ( 0 [,] 1 )  <->  ( t  e.  RR  /\  0  <_ 
t  /\  t  <_  1 ) )
8079simp1bi 970 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  RR )
8176, 80syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  t  e.  RR )
82 simp2r 982 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  s  e.  ( 0 [,] 1
) )
8377, 78elicc2i 10732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( 0 [,] 1 )  <->  ( s  e.  RR  /\  0  <_ 
s  /\  s  <_  1 ) )
8483simp1bi 970 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  ( 0 [,] 1 )  ->  s  e.  RR )
8582, 84syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  s  e.  RR )
8681, 85letrid 8985 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  (
t  <_  s  \/  s  <_  t ) )
87 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  t  <_  s )
8881adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  t  e.  RR )
8979simp2bi 971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( t  e.  ( 0 [,] 1 )  ->  0  <_  t )
9076, 89syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  0  <_  t )
9190adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  0  <_  t )
9285adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  s  e.  RR )
9377a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  0  e.  RR )
94 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  t  =/=  0 )
9581, 90, 94ne0gt0d 8972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  0  <  t )
9695adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  0  <  t )
9793, 88, 92, 96, 87ltletrd 8992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  0  <  s )
98 divelunit 24095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( t  e.  RR  /\  0  <_  t )  /\  ( s  e.  RR  /\  0  <  s ) )  ->  ( (
t  /  s )  e.  ( 0 [,] 1 )  <->  t  <_  s ) )
9988, 91, 92, 97, 98syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  (
( t  /  s
)  e.  ( 0 [,] 1 )  <->  t  <_  s ) )
10087, 99mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  (
t  /  s )  e.  ( 0 [,] 1 ) )
101 simp12 986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  Z  e.  ( EE `  N
) )
102101ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  Z  e.  ( EE `  N
) )
103102, 52sylancom 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  ( Z `  i )  e.  CC )
104 simp13 987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  b  e.  ( EE `  N
) )
105104ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  b  e.  ( EE `  N
) )
106105, 56sylancom 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  (
b `  i )  e.  CC )
10780recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  CC )
10876, 107syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  t  e.  CC )
109108ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  t  e.  CC )
11084recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( s  e.  ( 0 [,] 1 )  ->  s  e.  CC )
11182, 110syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  s  e.  CC )
112111ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  s  e.  CC )
11377a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  0  e.  RR )
11481ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  t  e.  RR )
11585ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  s  e.  RR )
11690ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  0  <_  t )
117 simpll3 996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  t  =/=  0 )
118114, 116, 117ne0gt0d 8972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  0  <  t )
119 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  t  <_  s )
120113, 114, 115, 118, 119ltletrd 8992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  0  <  s )
121120gt0ne0d 9353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  s  =/=  0 )
122 divcl 9446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
t  /  s )  e.  CC )
123122adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( t  /  s
)  e.  CC )
124 simpr2 962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
s  e.  CC )
125 subcl 9067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 1  e.  CC  /\  s  e.  CC )  ->  ( 1  -  s
)  e.  CC )
12638, 124, 125sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( 1  -  s
)  e.  CC )
127 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( Z `  i
)  e.  CC )
128126, 127mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( 1  -  s )  x.  ( Z `  i )
)  e.  CC )
129 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( b `  i
)  e.  CC )
130124, 129mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( s  x.  (
b `  i )
)  e.  CC )
131123, 128, 130adddid 8875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( t  / 
s )  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( b `  i ) ) ) )  =  ( ( ( t  /  s
)  x.  ( ( 1  -  s )  x.  ( Z `  i ) ) )  +  ( ( t  /  s )  x.  ( s  x.  (
b `  i )
) ) ) )
132131oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( 1  -  ( t  / 
s ) )  x.  ( Z `  i
) )  +  ( ( t  /  s
)  x.  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) ) ) )  =  ( ( ( 1  -  (
t  /  s ) )  x.  ( Z `
 i ) )  +  ( ( ( t  /  s )  x.  ( ( 1  -  s )  x.  ( Z `  i
) ) )  +  ( ( t  / 
s )  x.  (
s  x.  ( b `
 i ) ) ) ) ) )
133 subcl 9067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 1  e.  CC  /\  ( t  /  s
)  e.  CC )  ->  ( 1  -  ( t  /  s
) )  e.  CC )
13438, 123, 133sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( 1  -  (
t  /  s ) )  e.  CC )
135134, 127mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( 1  -  ( t  /  s
) )  x.  ( Z `  i )
)  e.  CC )
136123, 128mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( t  / 
s )  x.  (
( 1  -  s
)  x.  ( Z `
 i ) ) )  e.  CC )
137123, 130mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( t  / 
s )  x.  (
s  x.  ( b `
 i ) ) )  e.  CC )
138135, 136, 137addassd 8873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( ( 1  -  ( t  /  s ) )  x.  ( Z `  i ) )  +  ( ( t  / 
s )  x.  (
( 1  -  s
)  x.  ( Z `
 i ) ) ) )  +  ( ( t  /  s
)  x.  ( s  x.  ( b `  i ) ) ) )  =  ( ( ( 1  -  (
t  /  s ) )  x.  ( Z `
 i ) )  +  ( ( ( t  /  s )  x.  ( ( 1  -  s )  x.  ( Z `  i
) ) )  +  ( ( t  / 
s )  x.  (
s  x.  ( b `
 i ) ) ) ) ) )
139123, 126mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( t  / 
s )  x.  (
1  -  s ) )  e.  CC )
140134, 139, 127adddird 8876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( 1  -  ( t  / 
s ) )  +  ( ( t  / 
s )  x.  (
1  -  s ) ) )  x.  ( Z `  i )
)  =  ( ( ( 1  -  (
t  /  s ) )  x.  ( Z `
 i ) )  +  ( ( ( t  /  s )  x.  ( 1  -  s ) )  x.  ( Z `  i
) ) ) )
141 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  s  e.  CC )
142 subdi 9229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( t  /  s
)  e.  CC  /\  1  e.  CC  /\  s  e.  CC )  ->  (
( t  /  s
)  x.  ( 1  -  s ) )  =  ( ( ( t  /  s )  x.  1 )  -  ( ( t  / 
s )  x.  s
) ) )
14338, 142mp3an2 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( t  /  s
)  e.  CC  /\  s  e.  CC )  ->  ( ( t  / 
s )  x.  (
1  -  s ) )  =  ( ( ( t  /  s
)  x.  1 )  -  ( ( t  /  s )  x.  s ) ) )
144122, 141, 143syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( t  /  s
)  x.  ( 1  -  s ) )  =  ( ( ( t  /  s )  x.  1 )  -  ( ( t  / 
s )  x.  s
) ) )
145122mulid1d 8868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( t  /  s
)  x.  1 )  =  ( t  / 
s ) )
146 divcan1 9449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( t  /  s
)  x.  s )  =  t )
147145, 146oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( ( t  / 
s )  x.  1 )  -  ( ( t  /  s )  x.  s ) )  =  ( ( t  /  s )  -  t ) )
148144, 147eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( t  /  s
)  x.  ( 1  -  s ) )  =  ( ( t  /  s )  -  t ) )
149148oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( 1  -  (
t  /  s ) )  +  ( ( t  /  s )  x.  ( 1  -  s ) ) )  =  ( ( 1  -  ( t  / 
s ) )  +  ( ( t  / 
s )  -  t
) ) )
150 simp1 955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  t  e.  CC )
151 npncan 9085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( 1  e.  CC  /\  ( t  /  s
)  e.  CC  /\  t  e.  CC )  ->  ( ( 1  -  ( t  /  s
) )  +  ( ( t  /  s
)  -  t ) )  =  ( 1  -  t ) )
15238, 151mp3an1 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( t  /  s
)  e.  CC  /\  t  e.  CC )  ->  ( ( 1  -  ( t  /  s
) )  +  ( ( t  /  s
)  -  t ) )  =  ( 1  -  t ) )
153122, 150, 152syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( 1  -  (
t  /  s ) )  +  ( ( t  /  s )  -  t ) )  =  ( 1  -  t ) )
154149, 153eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( 1  -  (
t  /  s ) )  +  ( ( t  /  s )  x.  ( 1  -  s ) ) )  =  ( 1  -  t ) )
155154adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( 1  -  ( t  /  s
) )  +  ( ( t  /  s
)  x.  ( 1  -  s ) ) )  =  ( 1  -  t ) )
156155oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( 1  -  ( t  / 
s ) )  +  ( ( t  / 
s )  x.  (
1  -  s ) ) )  x.  ( Z `  i )
)  =  ( ( 1  -  t )  x.  ( Z `  i ) ) )
157123, 126, 127mulassd 8874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( t  /  s )  x.  ( 1  -  s
) )  x.  ( Z `  i )
)  =  ( ( t  /  s )  x.  ( ( 1  -  s )  x.  ( Z `  i
) ) ) )
158157oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( 1  -  ( t  / 
s ) )  x.  ( Z `  i
) )  +  ( ( ( t  / 
s )  x.  (
1  -  s ) )  x.  ( Z `
 i ) ) )  =  ( ( ( 1  -  (
t  /  s ) )  x.  ( Z `
 i ) )  +  ( ( t  /  s )  x.  ( ( 1  -  s )  x.  ( Z `  i )
) ) ) )
159140, 156, 1583eqtr3rd 2337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( 1  -  ( t  / 
s ) )  x.  ( Z `  i
) )  +  ( ( t  /  s
)  x.  ( ( 1  -  s )  x.  ( Z `  i ) ) ) )  =  ( ( 1  -  t )  x.  ( Z `  i ) ) )
160123, 124, 129mulassd 8874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( t  /  s )  x.  s )  x.  (
b `  i )
)  =  ( ( t  /  s )  x.  ( s  x.  ( b `  i
) ) ) )
161146adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( t  / 
s )  x.  s
)  =  t )
162161oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( t  /  s )  x.  s )  x.  (
b `  i )
)  =  ( t  x.  ( b `  i ) ) )
163160, 162eqtr3d 2330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( t  / 
s )  x.  (
s  x.  ( b `
 i ) ) )  =  ( t  x.  ( b `  i ) ) )
164159, 163oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( ( 1  -  ( t  /  s ) )  x.  ( Z `  i ) )  +  ( ( t  / 
s )  x.  (
( 1  -  s
)  x.  ( Z `
 i ) ) ) )  +  ( ( t  /  s
)  x.  ( s  x.  ( b `  i ) ) ) )  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) ) )
165132, 138, 1643eqtr2rd 2335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( b `
 i ) ) )  =  ( ( ( 1  -  (
t  /  s ) )  x.  ( Z `
 i ) )  +  ( ( t  /  s )  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( b `
 i ) ) ) ) ) )
166103, 106, 109, 112, 121, 165syl23anc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) )  =  ( ( ( 1  -  ( t  /  s ) )  x.  ( Z `  i ) )  +  ( ( t  / 
s )  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( b `  i ) ) ) ) ) )
167166ralrimiva 2639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  A. i  e.  ( 1 ... N
) ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
b `  i )
) )  =  ( ( ( 1  -  ( t  /  s
) )  x.  ( Z `  i )
)  +  ( ( t  /  s )  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
b `  i )
) ) ) ) )
168 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( r  =  ( t  / 
s )  ->  (
1  -  r )  =  ( 1  -  ( t  /  s
) ) )
169168oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( r  =  ( t  / 
s )  ->  (
( 1  -  r
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( t  / 
s ) )  x.  ( Z `  i
) ) )
170 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( r  =  ( t  / 
s )  ->  (
r  x.  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) ) )  =  ( ( t  /  s )  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( b `
 i ) ) ) ) )
171169, 170oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( r  =  ( t  / 
s )  ->  (
( ( 1  -  r )  x.  ( Z `  i )
)  +  ( r  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
b `  i )
) ) ) )  =  ( ( ( 1  -  ( t  /  s ) )  x.  ( Z `  i ) )  +  ( ( t  / 
s )  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( b `  i ) ) ) ) ) )
172171eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( r  =  ( t  / 
s )  ->  (
( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( b `
 i ) ) )  =  ( ( ( 1  -  r
)  x.  ( Z `
 i ) )  +  ( r  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( b `
 i ) ) ) ) )  <->  ( (
( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  =  ( ( ( 1  -  ( t  / 
s ) )  x.  ( Z `  i
) )  +  ( ( t  /  s
)  x.  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) ) ) ) ) )
173172ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( r  =  ( t  / 
s )  ->  ( A. i  e.  (
1 ... N ) ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) )  =  ( ( ( 1  -  r )  x.  ( Z `  i ) )  +  ( r  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( b `  i ) ) ) ) )  <->  A. i  e.  ( 1 ... N
) ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
b `  i )
) )  =  ( ( ( 1  -  ( t  /  s
) )  x.  ( Z `  i )
)  +  ( ( t  /  s )  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
b `  i )
) ) ) ) ) )
174173rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( t  /  s
)  e.  ( 0 [,] 1 )  /\  A. i  e.  ( 1 ... N ) ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) )  =  ( ( ( 1  -  ( t  /  s ) )  x.  ( Z `  i ) )  +  ( ( t  / 
s )  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( b `  i ) ) ) ) ) )  ->  E. r  e.  (
0 [,] 1 ) A. i  e.  ( 1 ... N ) ( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( b `
 i ) ) )  =  ( ( ( 1  -  r
)  x.  ( Z `
 i ) )  +  ( r  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( b `
 i ) ) ) ) ) )
175100, 167, 174syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  t  <_  s )  ->  E. r  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... N
) ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
b `  i )
) )  =  ( ( ( 1  -  r )  x.  ( Z `  i )
)  +  ( r  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
b `  i )
) ) ) ) )
176175ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  (
t  <_  s  ->  E. r  e.  ( 0 [,] 1 ) A. i  e.  ( 1 ... N ) ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) )  =  ( ( ( 1  -  r )  x.  ( Z `  i ) )  +  ( r  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( b `  i ) ) ) ) ) ) )
17783simp2bi 971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( s  e.  ( 0 [,] 1 )  ->  0  <_  s )
17882, 177syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  0  <_  s )
179 divelunit 24095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( s  e.  RR  /\  0  <_  s )  /\  ( t  e.  RR  /\  0  <  t ) )  ->  ( (
s  /  t )  e.  ( 0 [,] 1 )  <->  s  <_  t ) )
18085, 178, 81, 95, 179syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  (
( s  /  t
)  e.  ( 0 [,] 1 )  <->  s  <_  t ) )
181180biimpar 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t )  ->  (
s  /  t )  e.  ( 0 [,] 1 ) )
182 simp112 1085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  Z  e.  ( EE `  N
) )
183 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  i  e.  ( 1 ... N
) )
184182, 183, 52syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  ( Z `  i )  e.  CC )
185 simp113 1086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  b  e.  ( EE `  N
) )
186185, 183, 56syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  (
b `  i )  e.  CC )
187 simp12r 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  s  e.  ( 0 [,] 1
) )
188187, 110syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  s  e.  CC )
189 simp12l 1068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  t  e.  ( 0 [,] 1
) )
190189, 107syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  t  e.  CC )
191 simp13 987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  t  =/=  0 )
192 divcl 9446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
s  /  t )  e.  CC )
193192adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( s  /  t
)  e.  CC )
194 simpr2 962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
t  e.  CC )
195 subcl 9067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 1  e.  CC  /\  t  e.  CC )  ->  ( 1  -  t
)  e.  CC )
19638, 194, 195sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( 1  -  t
)  e.  CC )
197 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( Z `  i
)  e.  CC )
198196, 197mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( 1  -  t )  x.  ( Z `  i )
)  e.  CC )
199 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( b `  i
)  e.  CC )
200194, 199mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( t  x.  (
b `  i )
)  e.  CC )
201193, 198, 200adddid 8875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( s  / 
t )  x.  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) ) )  =  ( ( ( s  /  t
)  x.  ( ( 1  -  t )  x.  ( Z `  i ) ) )  +  ( ( s  /  t )  x.  ( t  x.  (
b `  i )
) ) ) )
202201oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( ( 1  -  ( s  / 
t ) )  x.  ( Z `  i
) )  +  ( ( s  /  t
)  x.  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) ) ) )  =  ( ( ( 1  -  (
s  /  t ) )  x.  ( Z `
 i ) )  +  ( ( ( s  /  t )  x.  ( ( 1  -  t )  x.  ( Z `  i
) ) )  +  ( ( s  / 
t )  x.  (
t  x.  ( b `
 i ) ) ) ) ) )
203 subcl 9067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 1  e.  CC  /\  ( s  /  t
)  e.  CC )  ->  ( 1  -  ( s  /  t
) )  e.  CC )
20438, 193, 203sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( 1  -  (
s  /  t ) )  e.  CC )
205204, 197mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( 1  -  ( s  /  t
) )  x.  ( Z `  i )
)  e.  CC )
206193, 198mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( s  / 
t )  x.  (
( 1  -  t
)  x.  ( Z `
 i ) ) )  e.  CC )
207193, 200mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( s  / 
t )  x.  (
t  x.  ( b `
 i ) ) )  e.  CC )
208205, 206, 207addassd 8873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( ( ( 1  -  ( s  /  t ) )  x.  ( Z `  i ) )  +  ( ( s  / 
t )  x.  (
( 1  -  t
)  x.  ( Z `
 i ) ) ) )  +  ( ( s  /  t
)  x.  ( t  x.  ( b `  i ) ) ) )  =  ( ( ( 1  -  (
s  /  t ) )  x.  ( Z `
 i ) )  +  ( ( ( s  /  t )  x.  ( ( 1  -  t )  x.  ( Z `  i
) ) )  +  ( ( s  / 
t )  x.  (
t  x.  ( b `
 i ) ) ) ) ) )
209 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  t  e.  CC )
210 subdi 9229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( s  /  t
)  e.  CC  /\  1  e.  CC  /\  t  e.  CC )  ->  (
( s  /  t
)  x.  ( 1  -  t ) )  =  ( ( ( s  /  t )  x.  1 )  -  ( ( s  / 
t )  x.  t
) ) )
21138, 210mp3an2 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( s  /  t
)  e.  CC  /\  t  e.  CC )  ->  ( ( s  / 
t )  x.  (
1  -  t ) )  =  ( ( ( s  /  t
)  x.  1 )  -  ( ( s  /  t )  x.  t ) ) )
212192, 209, 211syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( s  /  t
)  x.  ( 1  -  t ) )  =  ( ( ( s  /  t )  x.  1 )  -  ( ( s  / 
t )  x.  t
) ) )
213192mulid1d 8868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( s  /  t
)  x.  1 )  =  ( s  / 
t ) )
214 divcan1 9449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( s  /  t
)  x.  t )  =  s )
215213, 214oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( ( s  / 
t )  x.  1 )  -  ( ( s  /  t )  x.  t ) )  =  ( ( s  /  t )  -  s ) )
216212, 215eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( s  /  t
)  x.  ( 1  -  t ) )  =  ( ( s  /  t )  -  s ) )
217216oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( 1  -  (
s  /  t ) )  +  ( ( s  /  t )  x.  ( 1  -  t ) ) )  =  ( ( 1  -  ( s  / 
t ) )  +  ( ( s  / 
t )  -  s
) ) )
218 simp1 955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  s  e.  CC )
219 npncan 9085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( 1  e.  CC  /\  ( s  /  t
)  e.  CC  /\  s  e.  CC )  ->  ( ( 1  -  ( s  /  t
) )  +  ( ( s  /  t
)  -  s ) )  =  ( 1  -  s ) )
22038, 219mp3an1 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( s  /  t
)  e.  CC  /\  s  e.  CC )  ->  ( ( 1  -  ( s  /  t
) )  +  ( ( s  /  t
)  -  s ) )  =  ( 1  -  s ) )
221192, 218, 220syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( 1  -  (
s  /  t ) )  +  ( ( s  /  t )  -  s ) )  =  ( 1  -  s ) )
222217, 221eqtr2d 2329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
1  -  s )  =  ( ( 1  -  ( s  / 
t ) )  +  ( ( s  / 
t )  x.  (
1  -  t ) ) ) )
223222oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( 1  -  s
)  x.  ( Z `
 i ) )  =  ( ( ( 1  -  ( s  /  t ) )  +  ( ( s  /  t )  x.  ( 1  -  t
) ) )  x.  ( Z `  i
) ) )
224223adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( 1  -  s )  x.  ( Z `  i )
)  =  ( ( ( 1  -  (
s  /  t ) )  +  ( ( s  /  t )  x.  ( 1  -  t ) ) )  x.  ( Z `  i ) ) )
225193, 196mulcld 8871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( s  / 
t )  x.  (
1  -  t ) )  e.  CC )
226204, 225, 197adddird 8876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( ( 1  -  ( s  / 
t ) )  +  ( ( s  / 
t )  x.  (
1  -  t ) ) )  x.  ( Z `  i )
)  =  ( ( ( 1  -  (
s  /  t ) )  x.  ( Z `
 i ) )  +  ( ( ( s  /  t )  x.  ( 1  -  t ) )  x.  ( Z `  i
) ) ) )
227193, 196, 197mulassd 8874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( ( s  /  t )  x.  ( 1  -  t
) )  x.  ( Z `  i )
)  =  ( ( s  /  t )  x.  ( ( 1  -  t )  x.  ( Z `  i
) ) ) )
228227oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( ( 1  -  ( s  / 
t ) )  x.  ( Z `  i
) )  +  ( ( ( s  / 
t )  x.  (
1  -  t ) )  x.  ( Z `
 i ) ) )  =  ( ( ( 1  -  (
s  /  t ) )  x.  ( Z `
 i ) )  +  ( ( s  /  t )  x.  ( ( 1  -  t )  x.  ( Z `  i )
) ) ) )
229224, 226, 2283eqtrrd 2333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( ( 1  -  ( s  / 
t ) )  x.  ( Z `  i
) )  +  ( ( s  /  t
)  x.  ( ( 1  -  t )  x.  ( Z `  i ) ) ) )  =  ( ( 1  -  s )  x.  ( Z `  i ) ) )
230193, 194, 199mulassd 8874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( ( s  /  t )  x.  t )  x.  (
b `  i )
)  =  ( ( s  /  t )  x.  ( t  x.  ( b `  i
) ) ) )
231214oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( ( s  / 
t )  x.  t
)  x.  ( b `
 i ) )  =  ( s  x.  ( b `  i
) ) )
232231adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( ( s  /  t )  x.  t )  x.  (
b `  i )
)  =  ( s  x.  ( b `  i ) ) )
233230, 232eqtr3d 2330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( s  / 
t )  x.  (
t  x.  ( b `
 i ) ) )  =  ( s  x.  ( b `  i ) ) )
234229, 233oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( ( ( 1  -  ( s  /  t ) )  x.  ( Z `  i ) )  +  ( ( s  / 
t )  x.  (
( 1  -  t
)  x.  ( Z `
 i ) ) ) )  +  ( ( s  /  t
)  x.  ( t  x.  ( b `  i ) ) ) )  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) ) )
235202, 208, 2343eqtr2rd 2335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( b `
 i ) ) )  =  ( ( ( 1  -  (
s  /  t ) )  x.  ( Z `
 i ) )  +  ( ( s  /  t )  x.  ( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( b `
 i ) ) ) ) ) )
236184, 186, 188, 190, 191, 235syl23anc 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t  /\  i  e.  ( 1 ... N
) )  ->  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( b `  i ) ) )  =  ( ( ( 1  -  ( s  /  t ) )  x.  ( Z `  i ) )  +  ( ( s  / 
t )  x.  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) ) ) ) )
2372363expa 1151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( b `  i ) ) )  =  ( ( ( 1  -  ( s  /  t ) )  x.  ( Z `  i ) )  +  ( ( s  / 
t )  x.  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) ) ) ) )
238237ralrimiva 2639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t )  ->  A. i  e.  ( 1 ... N
) ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
b `  i )
) )  =  ( ( ( 1  -  ( s  /  t
) )  x.  ( Z `  i )
)  +  ( ( s  /  t )  x.  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
b `  i )
) ) ) ) )
239 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( r  =  ( s  / 
t )  ->  (
1  -  r )  =  ( 1  -  ( s  /  t
) ) )
240239oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( r  =  ( s  / 
t )  ->  (
( 1  -  r
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( s  / 
t ) )  x.  ( Z `  i
) ) )
241 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( r  =  ( s  / 
t )  ->  (
r  x.  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) ) )  =  ( ( s  /  t )  x.  ( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( b `
 i ) ) ) ) )
242240, 241oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( r  =  ( s  / 
t )  ->  (
( ( 1  -  r )  x.  ( Z `  i )
)  +  ( r  x.  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
b `  i )
) ) ) )  =  ( ( ( 1  -  ( s  /  t ) )  x.  ( Z `  i ) )  +  ( ( s  / 
t )  x.  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) ) ) ) )
243242eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( r  =  ( s  / 
t )  ->  (
( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( b `
 i ) ) )  =  ( ( ( 1  -  r
)  x.  ( Z `
 i ) )  +  ( r  x.  ( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( b `
 i ) ) ) ) )  <->  ( (
( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( b `  i
) ) )  =  ( ( ( 1  -  ( s  / 
t ) )  x.  ( Z `  i
) )  +  ( ( s  /  t
)  x.  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) ) ) ) ) )
244243ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( r  =  ( s  / 
t )  ->  ( A. i  e.  (
1 ... N ) ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( b `  i ) ) )  =  ( ( ( 1  -  r )  x.  ( Z `  i ) )  +  ( r  x.  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) ) ) )  <->  A. i  e.  ( 1 ... N
) ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
b `  i )
) )  =  ( ( ( 1  -  ( s  /  t
) )  x.  ( Z `  i )
)  +  ( ( s  /  t )  x.  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
b `  i )
) ) ) ) ) )
245244rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( s  /  t
)  e.  ( 0 [,] 1 )  /\  A. i  e.  ( 1 ... N ) ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( b `  i ) ) )  =  ( ( ( 1  -  ( s  /  t ) )  x.  ( Z `  i ) )  +  ( ( s  / 
t )  x.  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) ) ) ) )  ->  E. r  e.  (
0 [,] 1 ) A. i  e.  ( 1 ... N ) ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( b `
 i ) ) )  =  ( ( ( 1  -  r
)  x.  ( Z `
 i ) )  +  ( r  x.  ( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( b `
 i ) ) ) ) ) )
246181, 238, 245syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1
) )  /\  t  =/=  0 )  /\  s  <_  t )  ->  E. r  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... N
) ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
b `  i )
) )  =  ( ( ( 1  -  r )  x.  ( Z `  i )
)  +  ( r  x.  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
b `  i )
) ) ) ) )
247246ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  (
s  <_  t  ->  E.