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

Theorem axcontlem2 25869
Description: Lemma for axcont 25880. The idea here is to set up a mapping  F that will allow us to transfer dedekind 25177 to two sets of points. Here, we set up  F and show its domain and range. (Contributed by Scott Fenton, 17-Jun-2013.)
Hypotheses
Ref Expression
axcontlem2.1  |-  D  =  { p  e.  ( EE `  N )  |  ( U  Btwn  <. Z ,  p >.  \/  p  Btwn  <. Z ,  U >. ) }
axcontlem2.2  |-  F  =  { <. x ,  t
>.  |  ( x  e.  D  /\  (
t  e.  ( 0 [,)  +oo )  /\  A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) ) ) ) }
Assertion
Ref Expression
axcontlem2  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  ->  F : D -1-1-onto-> ( 0 [,)  +oo ) )
Distinct variable groups:    Z, p, x, t, i    U, p, x, t, i    N, p, x, t, i    x, D, t
Allowed substitution hints:    D( i, p)    F( x, t, i, p)

Proof of Theorem axcontlem2
Dummy variables  k 
y  s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq2 3977 . . . . . . . . . 10  |-  ( p  =  x  ->  <. Z ,  p >.  =  <. Z ,  x >. )
21breq2d 4216 . . . . . . . . 9  |-  ( p  =  x  ->  ( U  Btwn  <. Z ,  p >.  <-> 
U  Btwn  <. Z ,  x >. ) )
3 breq1 4207 . . . . . . . . 9  |-  ( p  =  x  ->  (
p  Btwn  <. Z ,  U >. 
<->  x  Btwn  <. Z ,  U >. ) )
42, 3orbi12d 691 . . . . . . . 8  |-  ( p  =  x  ->  (
( U  Btwn  <. Z ,  p >.  \/  p  Btwn  <. Z ,  U >. )  <-> 
( U  Btwn  <. Z ,  x >.  \/  x  Btwn  <. Z ,  U >. ) ) )
5 axcontlem2.1 . . . . . . . 8  |-  D  =  { p  e.  ( EE `  N )  |  ( U  Btwn  <. Z ,  p >.  \/  p  Btwn  <. Z ,  U >. ) }
64, 5elrab2 3086 . . . . . . 7  |-  ( x  e.  D  <->  ( x  e.  ( EE `  N
)  /\  ( U  Btwn  <. Z ,  x >.  \/  x  Btwn  <. Z ,  U >. ) ) )
7 simpll3 998 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  ->  U  e.  ( EE `  N
) )
8 simpll2 997 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  ->  Z  e.  ( EE `  N
) )
9 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  ->  x  e.  ( EE `  N
) )
10 brbtwn 25803 . . . . . . . . . . . 12  |-  ( ( U  e.  ( EE
`  N )  /\  Z  e.  ( EE `  N )  /\  x  e.  ( EE `  N
) )  ->  ( U  Btwn  <. Z ,  x >.  <->  E. s  e.  (
0 [,] 1 ) A. i  e.  ( 1 ... N ) ( U `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( x `  i
) ) ) ) )
117, 8, 9, 10syl3anc 1184 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  ->  ( U  Btwn  <. Z ,  x >.  <->  E. s  e.  (
0 [,] 1 ) A. i  e.  ( 1 ... N ) ( U `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( x `  i
) ) ) ) )
1211biimpa 471 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  U  Btwn  <. Z ,  x >. )  ->  E. s  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... N
) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) ) )
13 simp-4r 744 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) )  ->  Z  =/=  U )
14 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  =  0  ->  (
1  -  s )  =  ( 1  -  0 ) )
15 ax-1cn 9038 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  e.  CC
1615subid1i 9362 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  -  0 )  =  1
1714, 16syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  =  0  ->  (
1  -  s )  =  1 )
1817oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  0  ->  (
( 1  -  s
)  x.  ( Z `
 i ) )  =  ( 1  x.  ( Z `  i
) ) )
19 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  0  ->  (
s  x.  ( x `
 i ) )  =  ( 0  x.  ( x `  i
) ) )
2018, 19oveq12d 6091 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  0  ->  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) )  =  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
x `  i )
) ) )
2120eqeq2d 2446 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  0  ->  (
( U `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( x `  i
) ) )  <->  ( U `  i )  =  ( ( 1  x.  ( Z `  i )
)  +  ( 0  x.  ( x `  i ) ) ) ) )
2221ralbidv 2717 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  0  ->  ( A. i  e.  (
1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) )  <->  A. i  e.  ( 1 ... N
) ( U `  i )  =  ( ( 1  x.  ( Z `  i )
)  +  ( 0  x.  ( x `  i ) ) ) ) )
2322biimpac 473 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. i  e.  ( 1 ... N ) ( U `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( x `  i
) ) )  /\  s  =  0 )  ->  A. i  e.  ( 1 ... N ) ( U `  i
)  =  ( ( 1  x.  ( Z `
 i ) )  +  ( 0  x.  ( x `  i
) ) ) )
24 eqcom 2437 . . . . . . . . . . . . . . . . . . 19  |-  ( Z  =  U  <->  U  =  Z )
257adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  ->  U  e.  ( EE `  N
) )
268adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  ->  Z  e.  ( EE `  N
) )
27 eqeefv 25807 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( U  e.  ( EE
`  N )  /\  Z  e.  ( EE `  N ) )  -> 
( U  =  Z  <->  A. i  e.  (
1 ... N ) ( U `  i )  =  ( Z `  i ) ) )
2825, 26, 27syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  ->  ( U  =  Z  <->  A. i  e.  ( 1 ... N
) ( U `  i )  =  ( Z `  i ) ) )
298ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  i  e.  ( 1 ... N
) )  ->  Z  e.  ( EE `  N
) )
30 fveecn 25806 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Z  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( Z `  i )  e.  CC )
3129, 30sylancom 649 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  i  e.  ( 1 ... N
) )  ->  ( Z `  i )  e.  CC )
32 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  i  e.  ( 1 ... N
) )  ->  x  e.  ( EE `  N
) )
33 fveecn 25806 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( x `  i )  e.  CC )
3432, 33sylancom 649 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  i  e.  ( 1 ... N
) )  ->  (
x `  i )  e.  CC )
35 mulid2 9079 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( Z `  i )  e.  CC  ->  (
1  x.  ( Z `
 i ) )  =  ( Z `  i ) )
36 mul02 9234 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x `  i )  e.  CC  ->  (
0  x.  ( x `
 i ) )  =  0 )
3735, 36oveqan12d 6092 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( Z `  i
)  e.  CC  /\  ( x `  i
)  e.  CC )  ->  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
x `  i )
) )  =  ( ( Z `  i
)  +  0 ) )
38 addid1 9236 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( Z `  i )  e.  CC  ->  (
( Z `  i
)  +  0 )  =  ( Z `  i ) )
3938adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( Z `  i
)  e.  CC  /\  ( x `  i
)  e.  CC )  ->  ( ( Z `
 i )  +  0 )  =  ( Z `  i ) )
4037, 39eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Z `  i
)  e.  CC  /\  ( x `  i
)  e.  CC )  ->  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
x `  i )
) )  =  ( Z `  i ) )
4140eqeq2d 2446 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Z `  i
)  e.  CC  /\  ( x `  i
)  e.  CC )  ->  ( ( U `
 i )  =  ( ( 1  x.  ( Z `  i
) )  +  ( 0  x.  ( x `
 i ) ) )  <->  ( U `  i )  =  ( Z `  i ) ) )
4231, 34, 41syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  i  e.  ( 1 ... N
) )  ->  (
( U `  i
)  =  ( ( 1  x.  ( Z `
 i ) )  +  ( 0  x.  ( x `  i
) ) )  <->  ( U `  i )  =  ( Z `  i ) ) )
4342ralbidva 2713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  ->  ( A. i  e.  (
1 ... N ) ( U `  i )  =  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
x `  i )
) )  <->  A. i  e.  ( 1 ... N
) ( U `  i )  =  ( Z `  i ) ) )
4428, 43bitr4d 248 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  ->  ( U  =  Z  <->  A. i  e.  ( 1 ... N
) ( U `  i )  =  ( ( 1  x.  ( Z `  i )
)  +  ( 0  x.  ( x `  i ) ) ) ) )
4524, 44syl5bb 249 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  ->  ( Z  =  U  <->  A. i  e.  ( 1 ... N
) ( U `  i )  =  ( ( 1  x.  ( Z `  i )
)  +  ( 0  x.  ( x `  i ) ) ) ) )
4623, 45syl5ibr 213 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  ->  (
( A. i  e.  ( 1 ... N
) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) )  /\  s  =  0 )  ->  Z  =  U ) )
4746expdimp 427 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) )  -> 
( s  =  0  ->  Z  =  U ) )
4847necon3d 2636 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) )  -> 
( Z  =/=  U  ->  s  =/=  0 ) )
4913, 48mpd 15 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) )  -> 
s  =/=  0 )
50 0re 9081 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
51 1re 9080 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  RR
5250, 51elicc2i 10966 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( 0 [,] 1 )  <->  ( s  e.  RR  /\  0  <_ 
s  /\  s  <_  1 ) )
5352simp1bi 972 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( 0 [,] 1 )  ->  s  e.  RR )
54 rereccl 9722 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  RR  /\  s  =/=  0 )  -> 
( 1  /  s
)  e.  RR )
5553, 54sylan 458 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
( 1  /  s
)  e.  RR )
5653adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
s  e.  RR )
5752simp2bi 973 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  e.  ( 0 [,] 1 )  ->  0  <_  s )
5857adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
0  <_  s )
59 simpr 448 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
s  =/=  0 )
6056, 58, 59ne0gt0d 9200 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
0  <  s )
61 0le1 9541 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <_  1
62 divge0 9869 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 1  e.  RR  /\  0  <_  1 )  /\  ( s  e.  RR  /\  0  < 
s ) )  -> 
0  <_  ( 1  /  s ) )
6351, 61, 62mpanl12 664 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  RR  /\  0  <  s )  -> 
0  <_  ( 1  /  s ) )
6456, 60, 63syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
0  <_  ( 1  /  s ) )
65 elrege0 10997 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  /  s )  e.  ( 0 [,) 
+oo )  <->  ( (
1  /  s )  e.  RR  /\  0  <_  ( 1  /  s
) ) )
6655, 64, 65sylanbrc 646 . . . . . . . . . . . . . . . . . 18  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
( 1  /  s
)  e.  ( 0 [,)  +oo ) )
6766adantll 695 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  s  =/=  0 )  ->  (
1  /  s )  e.  ( 0 [,) 
+oo ) )
6853ad3antlr 712 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N ) )  /\  s  e.  ( 0 [,] 1 ) )  /\  s  =/=  0
)  /\  i  e.  ( 1 ... N
) )  ->  s  e.  RR )
6968recnd 9104 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N ) )  /\  s  e.  ( 0 [,] 1 ) )  /\  s  =/=  0
)  /\  i  e.  ( 1 ... N
) )  ->  s  e.  CC )
70 simplr 732 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N ) )  /\  s  e.  ( 0 [,] 1 ) )  /\  s  =/=  0
)  /\  i  e.  ( 1 ... N
) )  ->  s  =/=  0 )
71 simp-4r 744 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N ) )  /\  s  e.  ( 0 [,] 1 ) )  /\  s  =/=  0
)  /\  i  e.  ( 1 ... N
) )  ->  x  e.  ( EE `  N
) )
7271, 33sylancom 649 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N ) )  /\  s  e.  ( 0 [,] 1 ) )  /\  s  =/=  0
)  /\  i  e.  ( 1 ... N
) )  ->  (
x `  i )  e.  CC )
738ad3antrrr 711 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N ) )  /\  s  e.  ( 0 [,] 1 ) )  /\  s  =/=  0
)  /\  i  e.  ( 1 ... N
) )  ->  Z  e.  ( EE `  N
) )
7473, 30sylancom 649 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N ) )  /\  s  e.  ( 0 [,] 1 ) )  /\  s  =/=  0
)  /\  i  e.  ( 1 ... N
) )  ->  ( Z `  i )  e.  CC )
75 reccl 9675 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( 1  /  s
)  e.  CC )
76 subcl 9295 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1  e.  CC  /\  ( 1  /  s
)  e.  CC )  ->  ( 1  -  ( 1  /  s
) )  e.  CC )
7715, 75, 76sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( 1  -  (
1  /  s ) )  e.  CC )
7877adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( 1  -  (
1  /  s ) )  e.  CC )
79 subcl 9295 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 1  e.  CC  /\  s  e.  CC )  ->  ( 1  -  s
)  e.  CC )
8015, 79mpan 652 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  e.  CC  ->  (
1  -  s )  e.  CC )
8180adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( 1  -  s
)  e.  CC )
8275, 81mulcld 9098 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  / 
s )  x.  (
1  -  s ) )  e.  CC )
8382adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  / 
s )  x.  (
1  -  s ) )  e.  CC )
84 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( Z `  i
)  e.  CC )
8578, 83, 84adddird 9103 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( 1  -  ( 1  / 
s ) )  +  ( ( 1  / 
s )  x.  (
1  -  s ) ) )  x.  ( Z `  i )
)  =  ( ( ( 1  -  (
1  /  s ) )  x.  ( Z `
 i ) )  +  ( ( ( 1  /  s )  x.  ( 1  -  s ) )  x.  ( Z `  i
) ) ) )
86 simpl 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
s  e.  CC )
87 subdi 9457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 1  /  s
)  e.  CC  /\  1  e.  CC  /\  s  e.  CC )  ->  (
( 1  /  s
)  x.  ( 1  -  s ) )  =  ( ( ( 1  /  s )  x.  1 )  -  ( ( 1  / 
s )  x.  s
) ) )
8815, 87mp3an2 1267 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 1  /  s
)  e.  CC  /\  s  e.  CC )  ->  ( ( 1  / 
s )  x.  (
1  -  s ) )  =  ( ( ( 1  /  s
)  x.  1 )  -  ( ( 1  /  s )  x.  s ) ) )
8975, 86, 88syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  / 
s )  x.  (
1  -  s ) )  =  ( ( ( 1  /  s
)  x.  1 )  -  ( ( 1  /  s )  x.  s ) ) )
9089oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( ( 1  /  s
)  x.  ( 1  -  s ) ) )  =  ( ( 1  -  ( 1  /  s ) )  +  ( ( ( 1  /  s )  x.  1 )  -  ( ( 1  / 
s )  x.  s
) ) ) )
9175mulid1d 9095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  / 
s )  x.  1 )  =  ( 1  /  s ) )
92 recid2 9683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  / 
s )  x.  s
)  =  1 )
9391, 92oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( ( 1  /  s )  x.  1 )  -  (
( 1  /  s
)  x.  s ) )  =  ( ( 1  /  s )  -  1 ) )
9493oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( ( ( 1  / 
s )  x.  1 )  -  ( ( 1  /  s )  x.  s ) ) )  =  ( ( 1  -  ( 1  /  s ) )  +  ( ( 1  /  s )  - 
1 ) ) )
95 addsubass 9305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 1  -  (
1  /  s ) )  e.  CC  /\  ( 1  /  s
)  e.  CC  /\  1  e.  CC )  ->  ( ( ( 1  -  ( 1  / 
s ) )  +  ( 1  /  s
) )  -  1 )  =  ( ( 1  -  ( 1  /  s ) )  +  ( ( 1  /  s )  - 
1 ) ) )
9615, 95mp3an3 1268 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 1  -  (
1  /  s ) )  e.  CC  /\  ( 1  /  s
)  e.  CC )  ->  ( ( ( 1  -  ( 1  /  s ) )  +  ( 1  / 
s ) )  - 
1 )  =  ( ( 1  -  (
1  /  s ) )  +  ( ( 1  /  s )  -  1 ) ) )
9777, 75, 96syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( ( 1  -  ( 1  / 
s ) )  +  ( 1  /  s
) )  -  1 )  =  ( ( 1  -  ( 1  /  s ) )  +  ( ( 1  /  s )  - 
1 ) ) )
9877, 75addcld 9097 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( 1  /  s ) )  e.  CC )
99 npcan 9304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 1  e.  CC  /\  ( 1  /  s
)  e.  CC )  ->  ( ( 1  -  ( 1  / 
s ) )  +  ( 1  /  s
) )  =  1 )
10015, 75, 99sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( 1  /  s ) )  =  1 )
10198, 100subeq0bd 9453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( ( 1  -  ( 1  / 
s ) )  +  ( 1  /  s
) )  -  1 )  =  0 )
10294, 97, 1013eqtr2d 2473 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( ( ( 1  / 
s )  x.  1 )  -  ( ( 1  /  s )  x.  s ) ) )  =  0 )
10390, 102eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( ( 1  /  s
)  x.  ( 1  -  s ) ) )  =  0 )
104103adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( ( 1  /  s
)  x.  ( 1  -  s ) ) )  =  0 )
105104oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( 1  -  ( 1  / 
s ) )  +  ( ( 1  / 
s )  x.  (
1  -  s ) ) )  x.  ( Z `  i )
)  =  ( 0  x.  ( Z `  i ) ) )
10675adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( 1  /  s
)  e.  CC )
10780ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( 1  -  s
)  e.  CC )
108106, 107, 84mulassd 9101 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( 1  /  s )  x.  ( 1  -  s
) )  x.  ( Z `  i )
)  =  ( ( 1  /  s )  x.  ( ( 1  -  s )  x.  ( Z `  i
) ) ) )
109108oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( 1  -  ( 1  / 
s ) )  x.  ( Z `  i
) )  +  ( ( ( 1  / 
s )  x.  (
1  -  s ) )  x.  ( Z `
 i ) ) )  =  ( ( ( 1  -  (
1  /  s ) )  x.  ( Z `
 i ) )  +  ( ( 1  /  s )  x.  ( ( 1  -  s )  x.  ( Z `  i )
) ) ) )
11085, 105, 1093eqtr3rd 2476 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( 1  -  ( 1  / 
s ) )  x.  ( Z `  i
) )  +  ( ( 1  /  s
)  x.  ( ( 1  -  s )  x.  ( Z `  i ) ) ) )  =  ( 0  x.  ( Z `  i ) ) )
111 mul02 9234 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Z `  i )  e.  CC  ->  (
0  x.  ( Z `
 i ) )  =  0 )
112111ad2antll 710 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( 0  x.  ( Z `  i )
)  =  0 )
113110, 112eqtrd 2467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( 1  -  ( 1  / 
s ) )  x.  ( Z `  i
) )  +  ( ( 1  /  s
)  x.  ( ( 1  -  s )  x.  ( Z `  i ) ) ) )  =  0 )
114 simpll 731 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
s  e.  CC )
115 simprl 733 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( x `  i
)  e.  CC )
116106, 114, 115mulassd 9101 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( 1  /  s )  x.  s )  x.  (
x `  i )
)  =  ( ( 1  /  s )  x.  ( s  x.  ( x `  i
) ) ) )
11792oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( ( 1  /  s )  x.  s )  x.  (
x `  i )
)  =  ( 1  x.  ( x `  i ) ) )
118 mulid2 9079 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x `  i )  e.  CC  ->  (
1  x.  ( x `
 i ) )  =  ( x `  i ) )
119118adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( x `  i
)  e.  CC  /\  ( Z `  i )  e.  CC )  -> 
( 1  x.  (
x `  i )
)  =  ( x `
 i ) )
120117, 119sylan9eq 2487 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( 1  /  s )  x.  s )  x.  (
x `  i )
)  =  ( x `
 i ) )
121116, 120eqtr3d 2469 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  / 
s )  x.  (
s  x.  ( x `
 i ) ) )  =  ( x `
 i ) )
122113, 121oveq12d 6091 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( ( 1  -  ( 1  /  s ) )  x.  ( Z `  i ) )  +  ( ( 1  / 
s )  x.  (
( 1  -  s
)  x.  ( Z `
 i ) ) ) )  +  ( ( 1  /  s
)  x.  ( s  x.  ( x `  i ) ) ) )  =  ( 0  +  ( x `  i ) ) )
12378, 84mulcld 9098 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  -  ( 1  /  s
) )  x.  ( Z `  i )
)  e.  CC )
124 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( x `  i
)  e.  CC  /\  ( Z `  i )  e.  CC )  -> 
( Z `  i
)  e.  CC )
125 mulcl 9064 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 1  -  s
)  e.  CC  /\  ( Z `  i )  e.  CC )  -> 
( ( 1  -  s )  x.  ( Z `  i )
)  e.  CC )
12681, 124, 125syl2an 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  -  s )  x.  ( Z `  i )
)  e.  CC )
127106, 126mulcld 9098 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  / 
s )  x.  (
( 1  -  s
)  x.  ( Z `
 i ) ) )  e.  CC )
128 mulcl 9064 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  CC  /\  ( x `  i
)  e.  CC )  ->  ( s  x.  ( x `  i
) )  e.  CC )
129128ad2ant2r 728 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( s  x.  (
x `  i )
)  e.  CC )
130106, 129mulcld 9098 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  / 
s )  x.  (
s  x.  ( x `
 i ) ) )  e.  CC )
131123, 127, 130addassd 9100 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( ( 1  -  ( 1  /  s ) )  x.  ( Z `  i ) )  +  ( ( 1  / 
s )  x.  (
( 1  -  s
)  x.  ( Z `
 i ) ) ) )  +  ( ( 1  /  s
)  x.  ( s  x.  ( x `  i ) ) ) )  =  ( ( ( 1  -  (
1  /  s ) )  x.  ( Z `
 i ) )  +  ( ( ( 1  /  s )  x.  ( ( 1  -  s )  x.  ( Z `  i
) ) )  +  ( ( 1  / 
s )  x.  (
s  x.  ( x `
 i ) ) ) ) ) )
132106, 126, 129adddid 9102 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  / 
s )  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) ) )  =  ( ( ( 1  /  s
)  x.  ( ( 1  -  s )  x.  ( Z `  i ) ) )  +  ( ( 1  /  s )  x.  ( s  x.  (
x `  i )
) ) ) )
133132oveq2d 6089 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( 1  -  ( 1  / 
s ) )  x.  ( Z `  i
) )  +  ( ( 1  /  s
)  x.  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( x `  i
) ) ) ) )  =  ( ( ( 1  -  (
1  /  s ) )  x.  ( Z `
 i ) )  +  ( ( ( 1  /  s )  x.  ( ( 1  -  s )  x.  ( Z `  i
) ) )  +  ( ( 1  / 
s )  x.  (
s  x.  ( x `
 i ) ) ) ) ) )
134131, 133eqtr4d 2470 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( ( 1  -  ( 1  /  s ) )  x.  ( Z `  i ) )  +  ( ( 1  / 
s )  x.  (
( 1  -  s
)  x.  ( Z `
 i ) ) ) )  +  ( ( 1  /  s
)  x.  ( s  x.  ( x `  i ) ) ) )  =  ( ( ( 1  -  (
1  /  s ) )  x.  ( Z `
 i ) )  +  ( ( 1  /  s )  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( x `
 i ) ) ) ) ) )
135 addid2 9239 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x `  i )  e.  CC  ->  (
0  +  ( x `
 i ) )  =  ( x `  i ) )
136135ad2antrl 709 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( 0  +  ( x `  i ) )  =  ( x `
 i ) )
137122, 134, 1363eqtr3rd 2476 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( x `  i
)  =  ( ( ( 1  -  (
1  /  s ) )  x.  ( Z `
 i ) )  +  ( ( 1  /  s )  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( x `
 i ) ) ) ) ) )
13869, 70, 72, 74, 137syl22anc 1185 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N ) )  /\  s  e.  ( 0 [,] 1 ) )  /\  s  =/=  0
)  /\  i  e.  ( 1 ... N
) )  ->  (
x `  i )  =  ( ( ( 1  -  ( 1  /  s ) )  x.  ( Z `  i ) )  +  ( ( 1  / 
s )  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) ) ) ) )
139138ralrimiva 2781 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  s  =/=  0 )  ->  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  ( 1  /  s
) )  x.  ( Z `  i )
)  +  ( ( 1  /  s )  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) ) ) )
140 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( 1  / 
s )  ->  (
1  -  t )  =  ( 1  -  ( 1  /  s
) ) )
141140oveq1d 6088 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( 1  / 
s )  ->  (
( 1  -  t
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( 1  / 
s ) )  x.  ( Z `  i
) ) )
142 oveq1 6080 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( 1  / 
s )  ->  (
t  x.  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( x `  i
) ) ) )  =  ( ( 1  /  s )  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( x `
 i ) ) ) ) )
143141, 142oveq12d 6091 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  ( 1  / 
s )  ->  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) ) )  =  ( ( ( 1  -  ( 1  /  s ) )  x.  ( Z `  i ) )  +  ( ( 1  / 
s )  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) ) ) ) )
144143eqeq2d 2446 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  ( 1  / 
s )  ->  (
( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( x `
 i ) ) ) ) )  <->  ( x `  i )  =  ( ( ( 1  -  ( 1  /  s
) )  x.  ( Z `  i )
)  +  ( ( 1  /  s )  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) ) ) ) )
145144ralbidv 2717 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  ( 1  / 
s )  ->  ( A. i  e.  (
1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) ) ) )  <->  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  ( 1  /  s
) )  x.  ( Z `  i )
)  +  ( ( 1  /  s )  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) ) ) ) )
146145rspcev 3044 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1  /  s
)  e.  ( 0 [,)  +oo )  /\  A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  ( 1  /  s ) )  x.  ( Z `  i ) )  +  ( ( 1  / 
s )  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) ) ) ) )  ->  E. t  e.  (
0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) ) ) ) )
14767, 139, 146syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  s  =/=  0 )  ->  E. t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( x `
 i ) ) ) ) ) )
148 oveq2 6081 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) )  ->  (
t  x.  ( U `
 i ) )  =  ( t  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( x `
 i ) ) ) ) )
149148oveq2d 6089 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) )  ->  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) ) ) ) )
150149eqeq2d 2446 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) )  ->  (
( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) )  <->  ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) ) ) ) )
151150ralimi 2773 . . . . . . . . . . . . . . . . . 18  |-  ( A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) )  ->  A. i  e.  ( 1 ... N
) ( ( x `
 i )  =  ( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( U `
 i ) ) )  <->  ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) ) ) ) )
152 ralbi 2834 . . . . . . . . . . . . . . . . . 18  |-  ( A. i  e.  ( 1 ... N ) ( ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) )  <->  ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) ) ) )  ->  ( A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) )  <->  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) ) ) ) )
153151, 152syl 16 . . . . . . . . . . . . . . . . 17  |-  ( A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) )  ->  ( A. i  e.  (
1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) )  <->  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) ) ) ) )
154153rexbidv 2718 . . . . . . . . . . . . . . . 16  |-  ( A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) )  ->  ( E. t  e.  (
0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) )  <->  E. t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( ( ( 1  -  s )  x.  ( Z `  i
) )  +  ( s  x.  ( x `
 i ) ) ) ) ) ) )
155147, 154syl5ibrcom 214 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  s  =/=  0 )  ->  ( A. i  e.  (
1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) )  ->  E. t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) ) ) )
156155impancom 428 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) )  -> 
( s  =/=  0  ->  E. t  e.  ( 0 [,)  +oo ) A. i  e.  (
1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) ) ) )
15749, 156mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) )  ->  E. t  e.  (
0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) ) )
158157ex 424 . . . . . . . . . . . 12  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  ->  ( A. i  e.  (
1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) )  ->  E. t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) ) ) )
159158rexlimdva 2822 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  ->  ( E. s  e.  (
0 [,] 1 ) A. i  e.  ( 1 ... N ) ( U `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( x `  i
) ) )  ->  E. t  e.  (
0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) ) ) )
160159imp 419 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  E. s  e.  ( 0 [,] 1 ) A. i  e.  ( 1 ... N ) ( U `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  (
x `  i )
) ) )  ->  E. t  e.  (
0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) ) )
16112, 160syldan 457 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  U  Btwn  <. Z ,  x >. )  ->  E. t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) ) )
162 3simpa 954 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  /\  0  <_  x  /\  x  <_  1 )  ->  (
x  e.  RR  /\  0  <_  x ) )
16350, 51elicc2i 10966 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,] 1 )  <->  ( x  e.  RR  /\  0  <_  x  /\  x  <_  1
) )
164 elrege0 10997 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
165162, 163, 1643imtr4i 258 . . . . . . . . . . 11  |-  ( x  e.  ( 0 [,] 1 )  ->  x  e.  ( 0 [,)  +oo ) )
166165ssriv 3344 . . . . . . . . . 10  |-  ( 0 [,] 1 )  C_  ( 0 [,)  +oo )
167 brbtwn 25803 . . . . . . . . . . . 12  |-  ( ( x  e.  ( EE
`  N )  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  ->  (
x  Btwn  <. Z ,  U >. 
<->  E. t  e.  ( 0 [,] 1 ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) ) ) )
1689, 8, 7, 167syl3anc 1184 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  ->  (
x  Btwn  <. Z ,  U >. 
<->  E. t  e.  ( 0 [,] 1 ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) ) ) )
169168biimpa 471 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  x  Btwn  <. Z ,  U >. )  ->  E. t  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) ) )
170 ssrexv 3400 . . . . . . . . . 10  |-  ( ( 0 [,] 1 ) 
C_  ( 0 [,) 
+oo )  ->  ( E. t  e.  (
0 [,] 1 ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) )  ->  E. t  e.  (
0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) ) ) )
171166, 169, 170mpsyl 61 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  x  Btwn  <. Z ,  U >. )  ->  E. t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) ) )
172161, 171jaodan 761 . . . . . . . 8  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  ( U  Btwn  <. Z ,  x >.  \/  x  Btwn  <. Z ,  U >. ) )  ->  E. t  e.  (
0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) ) )
173172anasss 629 . . . . . . 7  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
x  e.  ( EE
`  N )  /\  ( U  Btwn  <. Z ,  x >.  \/  x  Btwn  <. Z ,  U >. ) ) )  ->  E. t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) ) )
1746, 173sylan2b 462 . . . . . 6  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  D )  ->  E. t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) ) )
175 r19.26 2830 . . . . . . . . . 10  |-  ( A. i  e.  ( 1 ... N ) ( ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) )  /\  ( x `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( U `  i
) ) ) )  <-> 
( A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  /\  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( U `  i ) ) ) ) )
176 eqtr2 2453 . . . . . . . . . . 11  |-  ( ( ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) )  /\  ( x `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( U `  i
) ) ) )  ->  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( U `  i ) ) ) )
177176ralimi 2773 . . . . . . . . . 10  |-  ( A. i  e.  ( 1 ... N ) ( ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) )  /\  ( x `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( U `  i
) ) ) )  ->  A. i  e.  ( 1 ... N ) ( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( U `
 i ) ) )  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( U `  i
) ) ) )
178175, 177sylbir 205 . . . . . . . . 9  |-  ( ( A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) )  /\  A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  ( U `  i )
) ) )  ->  A. i  e.  (
1 ... N ) ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  ( U `  i )
) ) )
179 elrege0 10997 . . . . . . . . . . . . 13  |-  ( t  e.  ( 0 [,) 
+oo )  <->  ( t  e.  RR  /\  0  <_ 
t ) )
180179simplbi 447 . . . . . . . . . . . 12  |-  ( t  e.  ( 0 [,) 
+oo )  ->  t  e.  RR )
181180recnd 9104 . . . . . . . . . . 11  |-  ( t  e.  ( 0 [,) 
+oo )  ->  t  e.  CC )
182 elrege0 10997 . . . . . . . . . . . . 13  |-  ( s  e.  ( 0 [,) 
+oo )  <->  ( s  e.  RR  /\  0  <_ 
s ) )
183182simplbi 447 . . . . . . . . . . . 12  |-  ( s  e.  ( 0 [,) 
+oo )  ->  s  e.  RR )
184183recnd 9104 . . . . . . . . . . 11  |-  ( s  e.  ( 0 [,) 
+oo )  ->  s  e.  CC )
185181, 184anim12i 550 . . . . . . . . . 10  |-  ( ( t  e.  ( 0 [,)  +oo )  /\  s  e.  ( 0 [,)  +oo ) )  ->  (
t  e.  CC  /\  s  e.  CC )
)
186 simplr 732 . . . . . . . . . . . . 13  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  /\  i  e.  ( 1 ... N
) )  ->  (
t  e.  CC  /\  s  e.  CC )
)
187 simpl2 961 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  ->  Z  e.  ( EE `  N ) )
188187ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  /\  i  e.  ( 1 ... N
) )  ->  Z  e.  ( EE `  N
) )
189188, 30sylancom 649 . . . . . . . . . . . . 13  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  /\  i  e.  ( 1 ... N
) )  ->  ( Z `  i )  e.  CC )
190 simpl3 962 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  ->  U  e.  ( EE `  N ) )
191190ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  /\  i  e.  ( 1 ... N
) )  ->  U  e.  ( EE `  N
) )
192 fveecn 25806 . . . . . . . . . . . . . 14  |-  ( ( U  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( U `  i )  e.  CC )
193191, 192sylancom 649 . . . . . . . . . . . . 13  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  /\  i  e.  ( 1 ... N
) )  ->  ( U `  i )  e.  CC )
194 subcl 9295 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  CC  /\  t  e.  CC )  ->  ( 1  -  t
)  e.  CC )
19515, 194mpan 652 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  CC  ->  (
1  -  t )  e.  CC )
196195adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( 1  -  t
)  e.  CC )
197 simpl 444 . . . . . . . . . . . . . . . 16  |-  ( ( ( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC )  -> 
( Z `  i
)  e.  CC )
198 mulcl 9064 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  -  t
)  e.  CC  /\  ( Z `  i )  e.  CC )  -> 
( ( 1  -  t )  x.  ( Z `  i )
)  e.  CC )
199196, 197, 198syl2an 464 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( 1  -  t )  x.  ( Z `  i )
)  e.  CC )
200 mulcl 9064 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  CC  /\  ( U `  i )  e.  CC )  -> 
( t  x.  ( U `  i )
)  e.  CC )
201200ad2ant2rl 730 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( t  x.  ( U `  i )
)  e.  CC )
20280adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( 1  -  s
)  e.  CC )
203202, 197, 125syl2an 464 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( 1  -  s )  x.  ( Z `  i )
)  e.  CC )
204 mulcl 9064 . . . . . . . . . . . . . . . 16  |-  ( ( s  e.  CC  /\  ( U `  i )  e.  CC )  -> 
( s  x.  ( U `  i )
)  e.  CC )
205204ad2ant2l 727 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( s  x.  ( U `  i )
)  e.  CC )
206199, 201, 203, 205addsubeq4d 9452 . . . . . . . . . . . . . 14  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( U `  i ) ) )  <-> 
( ( ( 1  -  s )  x.  ( Z `  i
) )  -  (
( 1  -  t
)  x.  ( Z `
 i ) ) )  =  ( ( t  x.  ( U `
 i ) )  -  ( s  x.  ( U `  i
) ) ) ) )
207 nnncan1 9327 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  s  e.  CC  /\  t  e.  CC )  ->  (
( 1  -  s
)  -  ( 1  -  t ) )  =  ( t  -  s ) )
20815, 207mp3an1 1266 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  CC  /\  t  e.  CC )  ->  ( ( 1  -  s )  -  (
1  -  t ) )  =  ( t  -  s ) )
209208ancoms 440 . . . . . . . . . . . . . . . . . 18  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( ( 1  -  s )  -  (
1  -  t ) )  =  ( t  -  s ) )
210209oveq1d 6088 . . . . . . . . . . . . . . . . 17  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( ( ( 1  -  s )  -  ( 1  -  t
) )  x.  ( Z `  i )
)  =  ( ( t  -  s )  x.  ( Z `  i ) ) )
211210adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( ( 1  -  s )  -  ( 1  -  t
) )  x.  ( Z `  i )
)  =  ( ( t  -  s )  x.  ( Z `  i ) ) )
21280ad2antlr 708 . . . . . . . . . . . . . . . . 17  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( 1  -  s
)  e.  CC )
213195ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( 1  -  t
)  e.  CC )
214 simprl 733 . . . . . . . . . . . . . . . . 17  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( Z `  i
)  e.  CC )
215212, 213, 214subdird 9480 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( ( 1  -  s )  -  ( 1  -  t
) )  x.  ( Z `  i )
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  -  ( ( 1  -  t )  x.  ( Z `  i
) ) ) )
216211, 215eqtr3d 2469 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( t  -  s )  x.  ( Z `  i )
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  -  ( ( 1  -  t )  x.  ( Z `  i
) ) ) )
217 simpll 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
t  e.  CC )
218 simplr 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
s  e.  CC )
219 simprr 734 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( U `  i
)  e.  CC )
220217, 218, 219subdird 9480 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( t  -  s )  x.  ( U `  i )
)  =  ( ( t  x.  ( U `
 i ) )  -  ( s  x.  ( U `  i
) ) ) )
221216, 220eqeq12d 2449 . . . . . . . . . . . . . 14  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( ( t  -  s )  x.  ( Z `  i
) )  =  ( ( t  -  s
)  x.  ( U `
 i ) )  <-> 
( ( ( 1  -  s )  x.  ( Z `  i
) )  -  (
( 1  -  t
)  x.  ( Z `
 i ) ) )  =  ( ( t  x.  ( U `
 i ) )  -  ( s  x.  ( U `  i
) ) ) ) )
222 subcl 9295 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( t  -  s
)  e.  CC )
223222adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( t  -  s
)  e.  CC )
224 mulcan1g 25179 . . . . . . . . . . . . . . 15  |-  ( ( ( t  -  s
)  e.  CC  /\  ( Z `  i )  e.  CC  /\  ( U `  i )  e.  CC )  ->  (
( ( t  -  s )  x.  ( Z `  i )
)  =  ( ( t  -  s )  x.  ( U `  i ) )  <->  ( (
t  -  s )  =  0  \/  ( Z `  i )  =  ( U `  i ) ) ) )
225223, 214, 219, 224syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( ( t  -  s )  x.  ( Z `  i
) )  =  ( ( t  -  s
)  x.  ( U `
 i ) )  <-> 
( ( t  -  s )  =  0  \/  ( Z `  i )  =  ( U `  i ) ) ) )
226206, 221, 2253bitr2d 273 . . . . . . . . . . . . 13  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( U `  i ) ) )  <-> 
( ( t  -  s )  =  0  \/  ( Z `  i )  =  ( U `  i ) ) ) )
227186, 189, 193, 226syl12anc 1182 . . . . . . . . . . . 12  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  /\  i  e.  ( 1 ... N
) )  ->  (
( ( ( 1  -  t )  x.  ( Z `  i
) )  +  ( t  x.  ( U `
 i ) ) )  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( U `  i
) ) )  <->  ( (
t  -  s )  =  0  \/  ( Z `  i )  =  ( U `  i ) ) ) )
228227ralbidva 2713 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  ( A. i  e.  ( 1 ... N ) ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  ( U `  i )
) )  <->  A. i  e.  ( 1 ... N
) ( ( t  -  s )  =  0  \/  ( Z `
 i )  =  ( U `  i
) ) ) )
229 r19.32v 2846 . . . . . . . . . . . 12  |-  ( A. i  e.  ( 1 ... N ) ( ( t  -  s
)  =  0  \/  ( Z `  i
)  =  ( U `
 i ) )  <-> 
( ( t  -  s )  =  0  \/  A. i  e.  ( 1 ... N
) ( Z `  i )  =  ( U `  i ) ) )
230 simplr 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  Z  =/=  U )
231230neneqd 2614 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  -.  Z  =  U )
232 simpll2 997 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  Z  e.  ( EE `  N ) )
233 simpll3 998 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  U  e.  ( EE `  N ) )
234 eqeefv 25807 . . . . . . . . . . . . . . . 16  |-  ( ( Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  -> 
( Z  =  U  <->  A. i  e.  (
1 ... N ) ( Z `  i )  =  ( U `  i ) ) )
235232, 233, 234syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  ( Z  =  U  <->  A. i  e.  ( 1 ... N ) ( Z `  i
)  =  ( U `
 i ) ) )
236231, 235mtbid 292 . . . . . . . . . . . . . 14  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  -.  A. i  e.  ( 1 ... N
) ( Z `  i )  =  ( U `  i ) )
237 orel2 373 . . . . . . . . . . . . . 14  |-  ( -. 
A. i  e.  ( 1 ... N ) ( Z `  i
)  =  ( U `
 i )  -> 
( ( ( t  -  s )  =  0  \/  A. i  e.  ( 1 ... N
) ( Z `  i )  =  ( U `  i ) )  ->  ( t  -  s )  =  0 ) )
238236, 237syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  ( (
( t  -  s
)  =  0  \/ 
A. i  e.  ( 1 ... N ) ( Z `  i
)  =  ( U `
 i ) )  ->  ( t  -  s )  =  0 ) )
239 subeq0 9317 . . . . . . . . . . . . . 14  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( ( t  -  s )  =  0  <-> 
t  =  s ) )
240239adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  ( (
t  -  s )  =  0  <->  t  =  s ) )
241238, 240sylibd 206 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  ( (
( t  -  s
)  =  0  \/ 
A. i  e.  ( 1 ... N ) ( Z `  i
)  =  ( U `
 i ) )  ->  t  =  s ) )
242229, 241syl5bi 209 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  ( A. i  e.  ( 1 ... N ) ( ( t  -  s
)  =  0  \/  ( Z `  i
)  =  ( U `
 i ) )  ->  t  =  s ) )
243228, 242sylbid 207 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  ( A. i  e.  ( 1 ... N ) ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  ( U `  i )
) )  ->  t  =  s ) )
244185, 243sylan2 461 . . . . . . . . 9  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  ( 0 [,)  +oo )  /\  s  e.  ( 0 [,)  +oo ) ) )  -> 
( A. i  e.  ( 1 ... N
) ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( U `  i ) ) )  ->  t  =  s ) )
245178, 244syl5 30 . . . . . . . 8  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  ( 0 [,)  +oo )  /\  s  e.  ( 0 [,)  +oo ) ) )  -> 
( ( A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  /\  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( U `  i ) ) ) )  ->  t  =  s ) )
246245ralrimivva 2790 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  ->  A. t  e.  (
0 [,)  +oo ) A. s  e.  ( 0 [,)  +oo ) ( ( A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) )  /\  A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  ( U `  i )
) ) )  -> 
t  =  s ) )
247246adantr 452 . . . . . 6  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  D )  ->  A. t  e.  ( 0 [,)  +oo ) A. s  e.  ( 0 [,)  +oo )
( ( A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  /\  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( U `  i ) ) ) )  ->  t  =  s ) )
248 oveq2 6081 . . . . . . . . . . 11  |-  ( t  =  s  ->  (
1  -  t )  =  ( 1  -  s ) )
249248oveq1d 6088 . . . . . . . . . 10  |-  ( t  =  s  ->  (
( 1  -  t
)  x.  ( Z `
 i ) )  =  ( ( 1  -  s )  x.  ( Z `  i
) ) )
250 oveq1 6080 . . . . . . . . . 10  |-  ( t  =  s  ->  (
t  x.  ( U `
 i ) )  =  ( s  x.  ( U `  i
) ) )
251249, 250oveq12d 6091 . . . . . . . . 9  |-  ( t  =  s  ->  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  ( U `  i )
) ) )
252251eqeq2d 2446 . . . . . . . 8  |-  ( t  =  s  ->  (
( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) )  <->  ( x `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( U `  i ) ) ) ) )
253252ralbidv 2717 . . . . . . 7  |-  ( t  =  s  ->  ( A. i  e.  (
1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) )  <->  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( U `  i ) ) ) ) )
254253reu4 3120 . . . . . 6  |-  ( E! t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  <-> 
( E. t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N ) ( x `  i
)  =  ( ( ( 1  -  t
)  x.  ( Z `
 i ) )  +  ( t  x.  ( U `  i
) ) )  /\  A. t  e.  ( 0 [,)  +oo ) A. s  e.  ( 0 [,)  +oo ) ( ( A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  ( U `  i )
) ) )  -> 
t  =  s ) ) )
255174, 247, 254sylanbrc 646 . . . . 5  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  D )  ->  E! t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) ) )
256 df-reu 2704 . . . . 5  |-  ( E! t  e.  ( 0 [,)  +oo ) A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  <-> 
E! t ( t  e.  ( 0 [,) 
+oo )  /\  A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) ) ) )
257255, 256sylib 189 . . . 4  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  D )  ->  E! t ( t  e.  ( 0 [,)  +oo )  /\  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) ) ) )
258257ralrimiva 2781 . . 3  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  ->  A. x  e.  D  E! t ( t  e.  ( 0 [,)  +oo )  /\  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) ) ) )
259 axcontlem2.2 . . . 4  |-  F  =  { <. x ,  t
>.  |  ( x  e.  D  /\  (
t  e.  ( 0 [,)  +oo )  /\  A. i  e.  ( 1 ... N ) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i ) )  +  ( t  x.  ( U `  i )
) ) ) ) }
260259fnopabg 5560 . . 3  |-  ( A. x  e.  D  E! t ( t  e.  ( 0 [,)  +oo )  /\  A. i  e.  ( 1 ... N
) ( x `  i )  =  ( ( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) ) )  <->  F  Fn  D
)
261258, 260sylib 189 . 2  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  ->  F  Fn  D )
262180ad2antlr 708 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  t  e.  ( 0 [,)  +oo ) )  /\  k  e.  ( 1 ... N
) )  ->  t  e.  RR )
263187ad2antrr 707 . . . . . . . . . . 11  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  t  e.  ( 0 [,)  +oo ) )  /\  k  e.  ( 1 ... N
) )  ->  Z  e.  ( EE `  N
) )
264 fveere 25805 . . . . . . . . . . 11  |-  ( ( Z  e.  ( EE
`  N )  /\  k  e.  ( 1 ... N ) )  ->  ( Z `  k )  e.  RR )
265263, 264sylancom 649 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  NN