MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axcontlem4 Structured version   Unicode version

Theorem axcontlem4 23164
Description: Lemma for axcont 23173. 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 1030 . 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 3641 . . . . . 6  |-  ( B  =/=  (/)  <->  E. b  b  e.  B )
3 idd 24 . . . . . . . . . 10  |-  ( b  e.  B  ->  ( A  C_  ( EE `  N )  ->  A  C_  ( EE `  N
) ) )
4 ssel 3345 . . . . . . . . . . 11  |-  ( B 
C_  ( EE `  N )  ->  (
b  e.  B  -> 
b  e.  ( EE
`  N ) ) )
54com12 31 . . . . . . . . . 10  |-  ( b  e.  B  ->  ( B  C_  ( EE `  N )  ->  b  e.  ( EE `  N
) ) )
6 opeq2 4055 . . . . . . . . . . . . 13  |-  ( y  =  b  ->  <. Z , 
y >.  =  <. Z , 
b >. )
76breq2d 4299 . . . . . . . . . . . 12  |-  ( y  =  b  ->  (
x  Btwn  <. Z , 
y >. 
<->  x  Btwn  <. Z , 
b >. ) )
87rspcv 3064 . . . . . . . . . . 11  |-  ( b  e.  B  ->  ( A. y  e.  B  x  Btwn  <. Z ,  y
>.  ->  x  Btwn  <. Z , 
b >. ) )
98ralimdv 2790 . . . . . . . . . 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 1296 . . . . . . . . 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 565 . . . . . . . 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 1030 . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . 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 1031 . . . . . . . . . . . . . . 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 3352 . . . . . . . . . . . . . 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 996 . . . . . . . . . . . . . . . 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 989 . . . . . . . . . . . . . . . 16  |-  ( ( Z  e.  ( EE
`  N )  /\  U  e.  A  /\  Z  =/=  U )  ->  U  e.  A )
18 breq1 4290 . . . . . . . . . . . . . . . . 17  |-  ( x  =  U  ->  (
x  Btwn  <. Z , 
b >. 
<->  U  Btwn  <. Z , 
b >. ) )
1918rspccva 3067 . . . . . . . . . . . . . . . 16  |-  ( ( A. x  e.  A  x  Btwn  <. Z ,  b
>.  /\  U  e.  A
)  ->  U  Btwn  <. Z ,  b >. )
2016, 17, 19syl2an 477 . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . 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 532 . . . . . . . . . . . . 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 3351 . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . 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 4290 . . . . . . . . . . . . . . 15  |-  ( x  =  p  ->  (
x  Btwn  <. Z , 
b >. 
<->  p  Btwn  <. Z , 
b >. ) )
2625rspccva 3067 . . . . . . . . . . . . . 14  |-  ( ( A. x  e.  A  x  Btwn  <. Z ,  b
>.  /\  p  e.  A
)  ->  p  Btwn  <. Z ,  b >. )
2724, 26sylan 471 . . . . . . . . . . . . 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 535 . . . . . . . . . . . 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 820 . . . . . . . . . . . 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 196 . . . . . . . . . . 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 989 . . . . . . . . . . . . . 14  |-  ( ( A  C_  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  A. x  e.  A  x  Btwn  <. Z ,  b >. )  ->  b  e.  ( EE `  N ) )
32 simpl2r 1042 . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . . . . . . . . . . . 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 2786 . . . . . . . . . . . . . . . . . . . . . . 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 2440 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( t  =  0  ->  (
1  -  t )  =  ( 1  -  0 ) )
38 1m0e1 10424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 1  -  0 )  =  1
3937, 38syl6eq 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( t  =  0  ->  (
1  -  t )  =  1 )
4039oveq1d 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( t  =  0  ->  (
( 1  -  t
)  x.  ( Z `
 i ) )  =  ( 1  x.  ( Z `  i
) ) )
41 oveq1 6093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( t  =  0  ->  (
t  x.  ( b `
 i ) )  =  ( 0  x.  ( b `  i
) ) )
4240, 41oveq12d 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  =  0  ->  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( b `  i ) ) )  =  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
b `  i )
) ) )
4342eqeq1d 2446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  0  ->  (
( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( b `
 i ) ) )  =  ( U `
 i )  <->  ( (
1  x.  ( Z `
 i ) )  +  ( 0  x.  ( b `  i
) ) )  =  ( U `  i
) ) )
4436, 43syl5bb 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  0  ->  (
( U `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( b `  i
) ) )  <->  ( (
1  x.  ( Z `
 i ) )  +  ( 0  x.  ( b `  i
) ) )  =  ( U `  i
) ) )
4544ralbidv 2730 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
4645biimpac 486 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
47 simpl2l 1041 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
48 simpl3l 1043 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
49 eqeefv 23100 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  -> 
( Z  =  U  <->  A. i  e.  (
1 ... N ) ( Z `  i )  =  ( U `  i ) ) )
5047, 48, 49syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
51 fveecn 23099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( Z  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( Z `  i )  e.  CC )
5247, 51sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
53 simp1r 1013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
5453ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
55 fveecn 23099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( b  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( b `  i )  e.  CC )
5654, 55sylancom 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
57 mulid2 9376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Z `  i )  e.  CC  ->  (
1  x.  ( Z `
 i ) )  =  ( Z `  i ) )
58 mul02 9539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( b `  i )  e.  CC  ->  (
0  x.  ( b `
 i ) )  =  0 )
5957, 58oveqan12d 6105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( Z `  i
)  e.  CC  /\  ( b `  i
)  e.  CC )  ->  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
b `  i )
) )  =  ( ( Z `  i
)  +  0 ) )
60 addid1 9541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( Z `  i )  e.  CC  ->  (
( Z `  i
)  +  0 )  =  ( Z `  i ) )
6160adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( Z `  i
)  e.  CC  /\  ( b `  i
)  e.  CC )  ->  ( ( Z `
 i )  +  0 )  =  ( Z `  i ) )
6259, 61eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( Z `  i
)  e.  CC  /\  ( b `  i
)  e.  CC )  ->  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
b `  i )
) )  =  ( Z `  i ) )
6352, 56, 62syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
6463eqeq1d 2446 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
6564ralbidva 2726 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
6650, 65bitr4d 256 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
6746, 66syl5ibr 221 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
6867expdimp 437 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
6935, 68sylan2 474 . . . . . . . . . . . . . . . . . . . . . 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 ) )
7069necon3d 2641 . . . . . . . . . . . . . . . . . . . . 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 ) )
7133, 70mpd 15 . . . . . . . . . . . . . . . . . . . 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 )
72 simp1l 1012 . . . . . . . . . . . . . . . . . . . . . . 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 )
73 simp2l 1014 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
7472, 73, 533jca 1168 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
75 simp2l 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
76 0re 9378 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  0  e.  RR
77 1re 9377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  1  e.  RR
7876, 77elicc2i 11353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  e.  ( 0 [,] 1 )  <->  ( t  e.  RR  /\  0  <_ 
t  /\  t  <_  1 ) )
7978simp1bi 1003 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  RR )
8075, 79syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
81 simp2r 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
8276, 77elicc2i 11353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( s  e.  ( 0 [,] 1 )  <->  ( s  e.  RR  /\  0  <_ 
s  /\  s  <_  1 ) )
8382simp1bi 1003 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( s  e.  ( 0 [,] 1 )  ->  s  e.  RR )
8481, 83syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
8580, 84letrid 9516 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
86 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
8780adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
8878simp2bi 1004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( t  e.  ( 0 [,] 1 )  ->  0  <_  t )
8975, 88syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  0  <_  t )
9089adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
9184adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
9276a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
93 simp3 990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  t  =/=  0 )
9480, 89, 93ne0gt0d 9503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  b  e.  ( EE `  N ) )  /\  ( t  e.  ( 0 [,] 1 )  /\  s  e.  ( 0 [,] 1 ) )  /\  t  =/=  0 )  ->  0  <  t )
9594adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
9692, 87, 91, 95, 86ltletrd 9523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
97 divelunit 11419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( t  e.  RR  /\  0  <_  t )  /\  ( s  e.  RR  /\  0  <  s ) )  ->  ( (
t  /  s )  e.  ( 0 [,] 1 )  <->  t  <_  s ) )
9887, 90, 91, 96, 97syl22anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
9986, 98mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
100 simp12 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
101100ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
102101, 51sylancom 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
103 simp13 1020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
104103ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
105104, 55sylancom 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
10679recnd 9404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( t  e.  ( 0 [,] 1 )  ->  t  e.  CC )
10775, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
108107ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
10983recnd 9404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( s  e.  ( 0 [,] 1 )  ->  s  e.  CC )
11081, 109syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
111110ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
11276a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
11380ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
11484ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
11589ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
116 simpll3 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
117113, 115, 116ne0gt0d 9503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
118 simplr 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
119112, 113, 114, 117, 118ltletrd 9523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
120119gt0ne0d 9896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
121 divcl 9992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
t  /  s )  e.  CC )
122121adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( t  /  s
)  e.  CC )
123 ax-1cn 9332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  1  e.  CC
124 simpr2 995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
s  e.  CC )
125 subcl 9601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 1  e.  CC  /\  s  e.  CC )  ->  ( 1  -  s
)  e.  CC )
126123, 124, 125sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( 1  -  s
)  e.  CC )
127 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( Z `  i
)  e.  CC )
128126, 127mulcld 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( b `  i
)  e.  CC )
130124, 129mulcld 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( s  x.  (
b `  i )
)  e.  CC )
131122, 128, 130adddid 9402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 1  e.  CC  /\  ( t  /  s
)  e.  CC )  ->  ( 1  -  ( t  /  s
) )  e.  CC )
134123, 122, 133sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( 1  -  (
t  /  s ) )  e.  CC )
135134, 127mulcld 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
136122, 128mulcld 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
137122, 130mulcld 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
139122, 126mulcld 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  s  e.  CC )
142 subdi 9770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( t  /  s
)  e.  CC  /\  1  e.  CC  /\  s  e.  CC )  ->  (
( t  /  s
)  x.  ( 1  -  s ) )  =  ( ( ( t  /  s )  x.  1 )  -  ( ( t  / 
s )  x.  s
) ) )
143123, 142mp3an2 1302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( t  /  s
)  e.  CC  /\  s  e.  CC )  ->  ( ( t  / 
s )  x.  (
1  -  s ) )  =  ( ( ( t  /  s
)  x.  1 )  -  ( ( t  /  s )  x.  s ) ) )
144121, 141, 143syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( t  /  s
)  x.  ( 1  -  s ) )  =  ( ( ( t  /  s )  x.  1 )  -  ( ( t  / 
s )  x.  s
) ) )
145121mulid1d 9395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( t  /  s
)  x.  1 )  =  ( t  / 
s ) )
146 divcan1 9995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( t  /  s
)  x.  s )  =  t )
147145, 146oveq12d 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( ( t  / 
s )  x.  1 )  -  ( ( t  /  s )  x.  s ) )  =  ( ( t  /  s )  -  t ) )
148144, 147eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( t  /  s
)  x.  ( 1  -  s ) )  =  ( ( t  /  s )  -  t ) )
149148oveq2d 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  t  e.  CC )
151 npncan 9622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( 1  e.  CC  /\  ( t  /  s
)  e.  CC  /\  t  e.  CC )  ->  ( ( 1  -  ( t  /  s
) )  +  ( ( t  /  s
)  -  t ) )  =  ( 1  -  t ) )
152123, 151mp3an1 1301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( t  /  s
)  e.  CC  /\  t  e.  CC )  ->  ( ( 1  -  ( t  /  s
) )  +  ( ( t  /  s
)  -  t ) )  =  ( 1  -  t ) )
153121, 150, 152syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( 1  -  (
t  /  s ) )  +  ( ( t  /  s )  -  t ) )  =  ( 1  -  t ) )
154149, 153eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 )  ->  (
( 1  -  (
t  /  s ) )  +  ( ( t  /  s )  x.  ( 1  -  s ) ) )  =  ( 1  -  t ) )
155154adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
157122, 126, 127mulassd 9401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
160122, 124, 129mulassd 9401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( t  e.  CC  /\  s  e.  CC  /\  s  =/=  0 ) )  -> 
( ( t  / 
s )  x.  s
)  =  t )
162161oveq1d 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
166102, 105, 108, 111, 120, 165syl23anc 1225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( r  =  ( t  / 
s )  ->  (
1  -  r )  =  ( 1  -  ( t  /  s
) ) )
169168oveq1d 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( r  =  ( t  / 
s )  ->  (
( 1  -  r
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( t  / 
s ) )  x.  ( Z `  i
) ) )
170 oveq1 6093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
17599, 167, 174syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
17782simp2bi 1004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( s  e.  ( 0 [,] 1 )  ->  0  <_  s )
17881, 177syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( s  e.  RR  /\  0  <_  s )  /\  ( t  e.  RR  /\  0  <  t ) )  ->  ( (
s  /  t )  e.  ( 0 [,] 1 )  <->  s  <_  t ) )
18084, 178, 80, 94, 179syl22anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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, 51syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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, 55syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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, 109syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
s  /  t )  e.  CC )
193192adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( s  /  t
)  e.  CC )
194 simpr2 995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
t  e.  CC )
195 subcl 9601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 1  e.  CC  /\  t  e.  CC )  ->  ( 1  -  t
)  e.  CC )
196123, 194, 195sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( 1  -  t
)  e.  CC )
197 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( Z `  i
)  e.  CC )
198196, 197mulcld 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( b `  i
)  e.  CC )
200194, 199mulcld 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 1  e.  CC  /\  ( s  /  t
)  e.  CC )  ->  ( 1  -  ( s  /  t
) )  e.  CC )
204123, 193, 203sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( Z `  i )  e.  CC  /\  ( b `  i
)  e.  CC )  /\  ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 ) )  -> 
( 1  -  (
s  /  t ) )  e.  CC )
205204, 197mulcld 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  t  e.  CC )
210 subdi 9770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( s  /  t
)  e.  CC  /\  1  e.  CC  /\  t  e.  CC )  ->  (
( s  /  t
)  x.  ( 1  -  t ) )  =  ( ( ( s  /  t )  x.  1 )  -  ( ( s  / 
t )  x.  t
) ) )
211123, 210mp3an2 1302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( s  /  t
)  e.  CC  /\  t  e.  CC )  ->  ( ( s  / 
t )  x.  (
1  -  t ) )  =  ( ( ( s  /  t
)  x.  1 )  -  ( ( s  /  t )  x.  t ) ) )
212192, 209, 211syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( s  /  t
)  x.  ( 1  -  t ) )  =  ( ( ( s  /  t )  x.  1 )  -  ( ( s  / 
t )  x.  t
) ) )
213192mulid1d 9395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( s  /  t
)  x.  1 )  =  ( s  / 
t ) )
214 divcan1 9995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( s  /  t
)  x.  t )  =  s )
215213, 214oveq12d 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( ( s  / 
t )  x.  1 )  -  ( ( s  /  t )  x.  t ) )  =  ( ( s  /  t )  -  s ) )
216212, 215eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( s  /  t
)  x.  ( 1  -  t ) )  =  ( ( s  /  t )  -  s ) )
217216oveq2d 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  s  e.  CC )
219 npncan 9622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( 1  e.  CC  /\  ( s  /  t
)  e.  CC  /\  s  e.  CC )  ->  ( ( 1  -  ( s  /  t
) )  +  ( ( s  /  t
)  -  s ) )  =  ( 1  -  s ) )
220123, 219mp3an1 1301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( s  /  t
)  e.  CC  /\  s  e.  CC )  ->  ( ( 1  -  ( s  /  t
) )  +  ( ( s  /  t
)  -  s ) )  =  ( 1  -  s ) )
221192, 218, 220syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( 1  -  (
s  /  t ) )  +  ( ( s  /  t )  -  s ) )  =  ( 1  -  s ) )
222217, 221eqtr2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
1  -  s )  =  ( ( 1  -  ( s  / 
t ) )  +  ( ( s  / 
t )  x.  (
1  -  t ) ) ) )
223222oveq1d 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( s  e.  CC  /\  t  e.  CC  /\  t  =/=  0 )  ->  (
( ( s  / 
t )  x.  t
)  x.  ( b `
 i ) )  =  ( s  x.  ( b `  i
) ) )
232231adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( r  =  ( s  / 
t )  ->  (
1  -  r )  =  ( 1  -  ( s  /  t
) ) )
240239oveq1d 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( r  =  ( s  / 
t )  ->  (
( 1  -  r
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( s  / 
t ) )  x.  ( Z `  i
) ) )
241 oveq1 6093 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. 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