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

Theorem axcontlem2 24593
Description: Lemma for axcont 24604. The idea here is to set up a mapping  F that will allow us to transfer dedekind 24082 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 3797 . . . . . . . . . 10  |-  ( p  =  x  ->  <. Z ,  p >.  =  <. Z ,  x >. )
21breq2d 4035 . . . . . . . . 9  |-  ( p  =  x  ->  ( U  Btwn  <. Z ,  p >.  <-> 
U  Btwn  <. Z ,  x >. ) )
3 breq1 4026 . . . . . . . . 9  |-  ( p  =  x  ->  (
p  Btwn  <. Z ,  U >. 
<->  x  Btwn  <. Z ,  U >. ) )
42, 3orbi12d 690 . . . . . . . 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 2925 . . . . . . 7  |-  ( x  e.  D  <->  ( x  e.  ( EE `  N
)  /\  ( U  Btwn  <. Z ,  x >.  \/  x  Btwn  <. Z ,  U >. ) ) )
7 simpll3 996 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  ->  U  e.  ( EE `  N
) )
8 simpll2 995 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  ->  Z  e.  ( EE `  N
) )
9 simpr 447 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  ->  x  e.  ( EE `  N
) )
10 brbtwn 24527 . . . . . . . . . . . 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 1182 . . . . . . . . . . 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 470 . . . . . . . . . 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 simpllr 735 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  ->  Z  =/=  U )
1413adantr 451 . . . . . . . . . . . . . . 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 )
15 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  =  0  ->  (
1  -  s )  =  ( 1  -  0 ) )
16 ax-1cn 8795 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  e.  CC
1716subid1i 9118 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  -  0 )  =  1
1815, 17syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  =  0  ->  (
1  -  s )  =  1 )
1918oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  0  ->  (
( 1  -  s
)  x.  ( Z `
 i ) )  =  ( 1  x.  ( Z `  i
) ) )
20 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  0  ->  (
s  x.  ( x `
 i ) )  =  ( 0  x.  ( x `  i
) ) )
2119, 20oveq12d 5876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  0  ->  (
( ( 1  -  s )  x.  ( Z `  i )
)  +  ( s  x.  ( x `  i ) ) )  =  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
x `  i )
) ) )
2221eqeq2d 2294 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  0  ->  (
( U `  i
)  =  ( ( ( 1  -  s
)  x.  ( Z `
 i ) )  +  ( s  x.  ( x `  i
) ) )  <->  ( U `  i )  =  ( ( 1  x.  ( Z `  i )
)  +  ( 0  x.  ( x `  i ) ) ) ) )
2322ralbidv 2563 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
2423biimpac 472 . . . . . . . . . . . . . . . . . 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
) ) ) )
25 eqcom 2285 . . . . . . . . . . . . . . . . . . 19  |-  ( Z  =  U  <->  U  =  Z )
267adantr 451 . . . . . . . . . . . . . . . . . . . . 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
) )
278adantr 451 . . . . . . . . . . . . . . . . . . . . 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
) )
28 eqeefv 24531 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( U  e.  ( EE
`  N )  /\  Z  e.  ( EE `  N ) )  -> 
( U  =  Z  <->  A. i  e.  (
1 ... N ) ( U `  i )  =  ( Z `  i ) ) )
2926, 27, 28syl2anc 642 . . . . . . . . . . . . . . . . . . . 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 ) ) )
308ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 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
) )
31 fveecn 24530 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Z  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( Z `  i )  e.  CC )
3230, 31sylancom 648 . . . . . . . . . . . . . . . . . . . . . 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 )
33 simpllr 735 . . . . . . . . . . . . . . . . . . . . . . 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
) )
34 fveecn 24530 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( x `  i )  e.  CC )
3533, 34sylancom 648 . . . . . . . . . . . . . . . . . . . . . 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 )
36 mulid2 8836 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( Z `  i )  e.  CC  ->  (
1  x.  ( Z `
 i ) )  =  ( Z `  i ) )
37 mul02 8990 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x `  i )  e.  CC  ->  (
0  x.  ( x `
 i ) )  =  0 )
3836, 37oveqan12d 5877 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( Z `  i
)  e.  CC  /\  ( x `  i
)  e.  CC )  ->  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
x `  i )
) )  =  ( ( Z `  i
)  +  0 ) )
39 addid1 8992 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( Z `  i )  e.  CC  ->  (
( Z `  i
)  +  0 )  =  ( Z `  i ) )
4039adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( Z `  i
)  e.  CC  /\  ( x `  i
)  e.  CC )  ->  ( ( Z `
 i )  +  0 )  =  ( Z `  i ) )
4138, 40eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( Z `  i
)  e.  CC  /\  ( x `  i
)  e.  CC )  ->  ( ( 1  x.  ( Z `  i ) )  +  ( 0  x.  (
x `  i )
) )  =  ( Z `  i ) )
4241eqeq2d 2294 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( Z `  i
)  e.  CC  /\  ( x `  i
)  e.  CC )  ->  ( ( U `
 i )  =  ( ( 1  x.  ( Z `  i
) )  +  ( 0  x.  ( x `
 i ) ) )  <->  ( U `  i )  =  ( Z `  i ) ) )
4332, 35, 42syl2anc 642 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
4443ralbidva 2559 . . . . . . . . . . . . . . . . . . . 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 ) ) )
4529, 44bitr4d 247 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
4625, 45syl5bb 248 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
4724, 46syl5ibr 212 . . . . . . . . . . . . . . . . 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 ) )
4847expdimp 426 . . . . . . . . . . . . . . . 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 ) )
4948necon3d 2484 . . . . . . . . . . . . . . 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 ) )
5014, 49mpd 14 . . . . . . . . . . . . . 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 )
51 0re 8838 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
52 1re 8837 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  RR
5351, 52elicc2i 10716 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  e.  ( 0 [,] 1 )  <->  ( s  e.  RR  /\  0  <_ 
s  /\  s  <_  1 ) )
5453simp1bi 970 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  e.  ( 0 [,] 1 )  ->  s  e.  RR )
55 rereccl 9478 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  RR  /\  s  =/=  0 )  -> 
( 1  /  s
)  e.  RR )
5654, 55sylan 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
( 1  /  s
)  e.  RR )
5754adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
s  e.  RR )
5853simp2bi 971 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  e.  ( 0 [,] 1 )  ->  0  <_  s )
5958adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
0  <_  s )
60 simpr 447 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
s  =/=  0 )
6157, 59, 60ne0gt0d 8956 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
0  <  s )
62 0le1 9297 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <_  1
63 divge0 9625 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 1  e.  RR  /\  0  <_  1 )  /\  ( s  e.  RR  /\  0  < 
s ) )  -> 
0  <_  ( 1  /  s ) )
6452, 62, 63mpanl12 663 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  RR  /\  0  <  s )  -> 
0  <_  ( 1  /  s ) )
6557, 61, 64syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
0  <_  ( 1  /  s ) )
66 elrege0 10746 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  /  s )  e.  ( 0 [,) 
+oo )  <->  ( (
1  /  s )  e.  RR  /\  0  <_  ( 1  /  s
) ) )
6756, 65, 66sylanbrc 645 . . . . . . . . . . . . . . . . . 18  |-  ( ( s  e.  ( 0 [,] 1 )  /\  s  =/=  0 )  -> 
( 1  /  s
)  e.  ( 0 [,)  +oo ) )
6867adantll 694 . . . . . . . . . . . . . . . . 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 ) )
6954ad2antlr 707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  x  e.  ( EE `  N
) )  /\  s  e.  ( 0 [,] 1
) )  /\  s  =/=  0 )  ->  s  e.  RR )
7069adantr 451 . . . . . . . . . . . . . . . . . . . 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 )
7170recnd 8861 . . . . . . . . . . . . . . . . . . 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 )
72 simplr 731 . . . . . . . . . . . . . . . . . . 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 )
7333adantlr 695 . . . . . . . . . . . . . . . . . . . 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
) )
7473, 34sylancom 648 . . . . . . . . . . . . . . . . . . 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 )
758ad3antrrr 710 . . . . . . . . . . . . . . . . . . . 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
) )
7675, 31sylancom 648 . . . . . . . . . . . . . . . . . . 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 )
77 reccl 9431 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( 1  /  s
)  e.  CC )
78 subcl 9051 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1  e.  CC  /\  ( 1  /  s
)  e.  CC )  ->  ( 1  -  ( 1  /  s
) )  e.  CC )
7916, 77, 78sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( 1  -  (
1  /  s ) )  e.  CC )
8079adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( 1  -  (
1  /  s ) )  e.  CC )
81 subcl 9051 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 1  e.  CC  /\  s  e.  CC )  ->  ( 1  -  s
)  e.  CC )
8216, 81mpan 651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( s  e.  CC  ->  (
1  -  s )  e.  CC )
8382adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( 1  -  s
)  e.  CC )
8477, 83mulcld 8855 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  / 
s )  x.  (
1  -  s ) )  e.  CC )
8584adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  / 
s )  x.  (
1  -  s ) )  e.  CC )
86 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( Z `  i
)  e.  CC )
8780, 85, 86adddird 8860 . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
88 simpl 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
s  e.  CC )
89 subdi 9213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 1  /  s
)  e.  CC  /\  1  e.  CC  /\  s  e.  CC )  ->  (
( 1  /  s
)  x.  ( 1  -  s ) )  =  ( ( ( 1  /  s )  x.  1 )  -  ( ( 1  / 
s )  x.  s
) ) )
9016, 89mp3an2 1265 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 1  /  s
)  e.  CC  /\  s  e.  CC )  ->  ( ( 1  / 
s )  x.  (
1  -  s ) )  =  ( ( ( 1  /  s
)  x.  1 )  -  ( ( 1  /  s )  x.  s ) ) )
9177, 88, 90syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  / 
s )  x.  (
1  -  s ) )  =  ( ( ( 1  /  s
)  x.  1 )  -  ( ( 1  /  s )  x.  s ) ) )
9291oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
9377mulid1d 8852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  / 
s )  x.  1 )  =  ( 1  /  s ) )
94 recid2 9439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  / 
s )  x.  s
)  =  1 )
9593, 94oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( ( 1  /  s )  x.  1 )  -  (
( 1  /  s
)  x.  s ) )  =  ( ( 1  /  s )  -  1 ) )
9695oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( ( ( 1  / 
s )  x.  1 )  -  ( ( 1  /  s )  x.  s ) ) )  =  ( ( 1  -  ( 1  /  s ) )  +  ( ( 1  /  s )  - 
1 ) ) )
97 addsubass 9061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
9816, 97mp3an3 1266 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 1  -  (
1  /  s ) )  e.  CC  /\  ( 1  /  s
)  e.  CC )  ->  ( ( ( 1  -  ( 1  /  s ) )  +  ( 1  / 
s ) )  - 
1 )  =  ( ( 1  -  (
1  /  s ) )  +  ( ( 1  /  s )  -  1 ) ) )
9979, 77, 98syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( ( 1  -  ( 1  / 
s ) )  +  ( 1  /  s
) )  -  1 )  =  ( ( 1  -  ( 1  /  s ) )  +  ( ( 1  /  s )  - 
1 ) ) )
100 npcan 9060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 1  e.  CC  /\  ( 1  /  s
)  e.  CC )  ->  ( ( 1  -  ( 1  / 
s ) )  +  ( 1  /  s
) )  =  1 )
10116, 77, 100sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( 1  /  s ) )  =  1 )
10279, 77addcld 8854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( 1  /  s ) )  e.  CC )
103 subeq0 9073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 1  -  ( 1  /  s
) )  +  ( 1  /  s ) )  e.  CC  /\  1  e.  CC )  ->  ( ( ( ( 1  -  ( 1  /  s ) )  +  ( 1  / 
s ) )  - 
1 )  =  0  <-> 
( ( 1  -  ( 1  /  s
) )  +  ( 1  /  s ) )  =  1 ) )
104102, 16, 103sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( ( ( 1  -  ( 1  /  s ) )  +  ( 1  / 
s ) )  - 
1 )  =  0  <-> 
( ( 1  -  ( 1  /  s
) )  +  ( 1  /  s ) )  =  1 ) )
105101, 104mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( ( 1  -  ( 1  / 
s ) )  +  ( 1  /  s
) )  -  1 )  =  0 )
10696, 99, 1053eqtr2d 2321 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( ( ( 1  / 
s )  x.  1 )  -  ( ( 1  /  s )  x.  s ) ) )  =  0 )
10792, 106eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( ( 1  /  s
)  x.  ( 1  -  s ) ) )  =  0 )
108107adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  -  ( 1  /  s
) )  +  ( ( 1  /  s
)  x.  ( 1  -  s ) ) )  =  0 )
109108oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
11077adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( 1  /  s
)  e.  CC )
11182ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( 1  -  s
)  e.  CC )
112110, 111, 86mulassd 8858 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
113112oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
11487, 109, 1133eqtr3rd 2324 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
115 mul02 8990 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Z `  i )  e.  CC  ->  (
0  x.  ( Z `
 i ) )  =  0 )
116115ad2antll 709 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( 0  x.  ( Z `  i )
)  =  0 )
117114, 116eqtrd 2315 . . . . . . . . . . . . . . . . . . . . 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 )
118 simpll 730 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
s  e.  CC )
119 simprl 732 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( x `  i
)  e.  CC )
120110, 118, 119mulassd 8858 . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
12194oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  e.  CC  /\  s  =/=  0 )  -> 
( ( ( 1  /  s )  x.  s )  x.  (
x `  i )
)  =  ( 1  x.  ( x `  i ) ) )
122 mulid2 8836 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x `  i )  e.  CC  ->  (
1  x.  ( x `
 i ) )  =  ( x `  i ) )
123122adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( x `  i
)  e.  CC  /\  ( Z `  i )  e.  CC )  -> 
( 1  x.  (
x `  i )
)  =  ( x `
 i ) )
124121, 123sylan9eq 2335 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( ( 1  /  s )  x.  s )  x.  (
x `  i )
)  =  ( x `
 i ) )
125120, 124eqtr3d 2317 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  / 
s )  x.  (
s  x.  ( x `
 i ) ) )  =  ( x `
 i ) )
126117, 125oveq12d 5876 . . . . . . . . . . . . . . . . . . . 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 ) ) )
12780, 86mulcld 8855 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  -  ( 1  /  s
) )  x.  ( Z `  i )
)  e.  CC )
128 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( x `  i
)  e.  CC  /\  ( Z `  i )  e.  CC )  -> 
( Z `  i
)  e.  CC )
129 mulcl 8821 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 1  -  s
)  e.  CC  /\  ( Z `  i )  e.  CC )  -> 
( ( 1  -  s )  x.  ( Z `  i )
)  e.  CC )
13083, 128, 129syl2an 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  -  s )  x.  ( Z `  i )
)  e.  CC )
131110, 130mulcld 8855 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  / 
s )  x.  (
( 1  -  s
)  x.  ( Z `
 i ) ) )  e.  CC )
132 mulcl 8821 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( s  e.  CC  /\  ( x `  i
)  e.  CC )  ->  ( s  x.  ( x `  i
) )  e.  CC )
133132ad2ant2r 727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( s  x.  (
x `  i )
)  e.  CC )
134110, 133mulcld 8855 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( ( 1  / 
s )  x.  (
s  x.  ( x `
 i ) ) )  e.  CC )
135127, 131, 134addassd 8857 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
136110, 130, 133adddid 8859 . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
137136oveq2d 5874 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
138135, 137eqtr4d 2318 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
139 addid2 8995 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x `  i )  e.  CC  ->  (
0  +  ( x `
 i ) )  =  ( x `  i ) )
140139ad2antrl 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( s  e.  CC  /\  s  =/=  0 )  /\  ( ( x `
 i )  e.  CC  /\  ( Z `
 i )  e.  CC ) )  -> 
( 0  +  ( x `  i ) )  =  ( x `
 i ) )
141126, 138, 1403eqtr3rd 2324 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
14271, 72, 74, 76, 141syl22anc 1183 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
143142ralrimiva 2626 . . . . . . . . . . . . . . . . 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 )
) ) ) ) )
144 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  ( 1  / 
s )  ->  (
1  -  t )  =  ( 1  -  ( 1  /  s
) ) )
145144oveq1d 5873 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  ( 1  / 
s )  ->  (
( 1  -  t
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( 1  / 
s ) )  x.  ( Z `  i
) ) )
146 oveq1 5865 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
147145, 146oveq12d 5876 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
148147eqeq2d 2294 . . . . . . . . . . . . . . . . . . 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 )
) ) ) ) ) )
149148ralbidv 2563 . . . . . . . . . . . . . . . . . 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 )
) ) ) ) ) )
150149rspcev 2884 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
15168, 143, 150syl2anc 642 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
152 oveq2 5866 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
153152oveq2d 5874 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
154153eqeq2d 2294 . . . . . . . . . . . . . . . . . . 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 )
) ) ) ) ) )
155154ralimi 2618 . . . . . . . . . . . . . . . . . 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 )
) ) ) ) ) )
156 ralbi 2679 . . . . . . . . . . . . . . . . . 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 )
) ) ) ) ) )
157155, 156syl 15 . . . . . . . . . . . . . . . . 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 )
) ) ) ) ) )
158157rexbidv 2564 . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
159151, 158syl5ibrcom 213 . . . . . . . . . . . . . . 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
) ) ) ) )
160159impancom 427 . . . . . . . . . . . . . 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 )
) ) ) )
16150, 160mpd 14 . . . . . . . . . . . . 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 )
) ) )
162161ex 423 . . . . . . . . . . . 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
) ) ) ) )
163162rexlimdva 2667 . . . . . . . . . . 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 )
) ) ) )
164163imp 418 . . . . . . . . . 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 )
) ) )
16512, 164syldan 456 . . . . . . . . 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
) ) ) )
166 3simpa 952 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  /\  0  <_  x  /\  x  <_  1 )  ->  (
x  e.  RR  /\  0  <_  x ) )
16751, 52elicc2i 10716 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,] 1 )  <->  ( x  e.  RR  /\  0  <_  x  /\  x  <_  1
) )
168 elrege0 10746 . . . . . . . . . . . 12  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
169166, 167, 1683imtr4i 257 . . . . . . . . . . 11  |-  ( x  e.  ( 0 [,] 1 )  ->  x  e.  ( 0 [,)  +oo ) )
170169ssriv 3184 . . . . . . . . . 10  |-  ( 0 [,] 1 )  C_  ( 0 [,)  +oo )
171 brbtwn 24527 . . . . . . . . . . . 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
) ) ) ) )
1729, 8, 7, 171syl3anc 1182 . . . . . . . . . . 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
) ) ) ) )
173172biimpa 470 . . . . . . . . . 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 ) ) ) )
174 ssrexv 3238 . . . . . . . . . 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 )
) ) ) )
175170, 173, 174mpsyl 59 . . . . . . . . 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
) ) ) )
176165, 175jaodan 760 . . . . . . . 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 )
) ) )
177176anasss 628 . . . . . . 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
) ) ) )
1786, 177sylan2b 461 . . . . . 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
) ) ) )
179 r19.26 2675 . . . . . . . . . 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 ) ) ) ) )
180 eqtr2 2301 . . . . . . . . . . 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 ) ) ) )
181180ralimi 2618 . . . . . . . . . 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
) ) ) )
182179, 181sylbir 204 . . . . . . . . 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 )
) ) )
183 elrege0 10746 . . . . . . . . . . . . 13  |-  ( t  e.  ( 0 [,) 
+oo )  <->  ( t  e.  RR  /\  0  <_ 
t ) )
184183simplbi 446 . . . . . . . . . . . 12  |-  ( t  e.  ( 0 [,) 
+oo )  ->  t  e.  RR )
185184recnd 8861 . . . . . . . . . . 11  |-  ( t  e.  ( 0 [,) 
+oo )  ->  t  e.  CC )
186 elrege0 10746 . . . . . . . . . . . . 13  |-  ( s  e.  ( 0 [,) 
+oo )  <->  ( s  e.  RR  /\  0  <_ 
s ) )
187186simplbi 446 . . . . . . . . . . . 12  |-  ( s  e.  ( 0 [,) 
+oo )  ->  s  e.  RR )
188187recnd 8861 . . . . . . . . . . 11  |-  ( s  e.  ( 0 [,) 
+oo )  ->  s  e.  CC )
189185, 188anim12i 549 . . . . . . . . . 10  |-  ( ( t  e.  ( 0 [,)  +oo )  /\  s  e.  ( 0 [,)  +oo ) )  ->  (
t  e.  CC  /\  s  e.  CC )
)
190 simplr 731 . . . . . . . . . . . . 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 )
)
191 simpl2 959 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  ->  Z  e.  ( EE `  N ) )
192191ad2antrr 706 . . . . . . . . . . . . . 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
) )
193192, 31sylancom 648 . . . . . . . . . . . . 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 )
194 simpl3 960 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  ->  U  e.  ( EE `  N ) )
195194ad2antrr 706 . . . . . . . . . . . . . 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
) )
196 fveecn 24530 . . . . . . . . . . . . . 14  |-  ( ( U  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( U `  i )  e.  CC )
197195, 196sylancom 648 . . . . . . . . . . . . 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 )
198 subcl 9051 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  CC  /\  t  e.  CC )  ->  ( 1  -  t
)  e.  CC )
19916, 198mpan 651 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  CC  ->  (
1  -  t )  e.  CC )
200199adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( 1  -  t
)  e.  CC )
201 simpl 443 . . . . . . . . . . . . . . . 16  |-  ( ( ( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC )  -> 
( Z `  i
)  e.  CC )
202 mulcl 8821 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1  -  t
)  e.  CC  /\  ( Z `  i )  e.  CC )  -> 
( ( 1  -  t )  x.  ( Z `  i )
)  e.  CC )
203200, 201, 202syl2an 463 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( 1  -  t )  x.  ( Z `  i )
)  e.  CC )
204 mulcl 8821 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  CC  /\  ( U `  i )  e.  CC )  -> 
( t  x.  ( U `  i )
)  e.  CC )
205204ad2ant2rl 729 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( t  x.  ( U `  i )
)  e.  CC )
20682adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( 1  -  s
)  e.  CC )
207206, 201, 129syl2an 463 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( ( 1  -  s )  x.  ( Z `  i )
)  e.  CC )
208 mulcl 8821 . . . . . . . . . . . . . . . 16  |-  ( ( s  e.  CC  /\  ( U `  i )  e.  CC )  -> 
( s  x.  ( U `  i )
)  e.  CC )
209208ad2ant2l 726 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( s  x.  ( U `  i )
)  e.  CC )
210203, 205, 207, 209addsubeq4d 9208 . . . . . . . . . . . . . 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
) ) ) ) )
211 nnncan1 9083 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  CC  /\  s  e.  CC  /\  t  e.  CC )  ->  (
( 1  -  s
)  -  ( 1  -  t ) )  =  ( t  -  s ) )
21216, 211mp3an1 1264 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  CC  /\  t  e.  CC )  ->  ( ( 1  -  s )  -  (
1  -  t ) )  =  ( t  -  s ) )
213212ancoms 439 . . . . . . . . . . . . . . . . . 18  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( ( 1  -  s )  -  (
1  -  t ) )  =  ( t  -  s ) )
214213oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( ( ( 1  -  s )  -  ( 1  -  t
) )  x.  ( Z `  i )
)  =  ( ( t  -  s )  x.  ( Z `  i ) ) )
215214adantr 451 . . . . . . . . . . . . . . . 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 ) ) )
21682ad2antlr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( 1  -  s
)  e.  CC )
217199ad2antrr 706 . . . . . . . . . . . . . . . . 17  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( 1  -  t
)  e.  CC )
218 simprl 732 . . . . . . . . . . . . . . . . 17  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( Z `  i
)  e.  CC )
219216, 217, 218subdird 9236 . . . . . . . . . . . . . . . 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
) ) ) )
220215, 219eqtr3d 2317 . . . . . . . . . . . . . . 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
) ) ) )
221 simpll 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
t  e.  CC )
222 simplr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
s  e.  CC )
223 simprr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( U `  i
)  e.  CC )
224221, 222, 223subdird 9236 . . . . . . . . . . . . . . 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
) ) ) )
225220, 224eqeq12d 2297 . . . . . . . . . . . . . 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
) ) ) ) )
226 subcl 9051 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( t  -  s
)  e.  CC )
227226adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  CC  /\  s  e.  CC )  /\  ( ( Z `
 i )  e.  CC  /\  ( U `
 i )  e.  CC ) )  -> 
( t  -  s
)  e.  CC )
228 mulcan1g 24084 . . . . . . . . . . . . . . 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 ) ) ) )
229227, 218, 223, 228syl3anc 1182 . . . . . . . . . . . . . 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 ) ) ) )
230210, 225, 2293bitr2d 272 . . . . . . . . . . . . 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 ) ) ) )
231190, 193, 197, 230syl12anc 1180 . . . . . . . . . . . 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 ) ) ) )
232231ralbidva 2559 . . . . . . . . . . 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
) ) ) )
233 r19.32v 2686 . . . . . . . . . . . 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 ) ) )
234 simplr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  Z  =/=  U )
235234neneqd 2462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  -.  Z  =  U )
236 simpll2 995 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  Z  e.  ( EE `  N ) )
237 simpll3 996 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
t  e.  CC  /\  s  e.  CC )
)  ->  U  e.  ( EE `  N ) )
238 eqeefv 24531 . . . . . . . . . . . . . . . 16  |-  ( ( Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  -> 
( Z  =  U  <->  A. i  e.  (
1 ... N ) ( Z `  i )  =  ( U `  i ) ) )
239236, 237, 238syl2anc 642 . . . . . . . . . . . . . . 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 ) ) )
240235, 239mtbid 291 . . . . . . . . . . . . . 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 ) )
241 orel2 372 . . . . . . . . . . . . . 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 ) )
242240, 241syl 15 . . . . . . . . . . . . 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 ) )
243 subeq0 9073 . . . . . . . . . . . . . 14  |-  ( ( t  e.  CC  /\  s  e.  CC )  ->  ( ( t  -  s )  =  0  <-> 
t  =  s ) )
244243adantl 452 . . . . . . . . . . . . 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 ) )
245242, 244sylibd 205 . . . . . . . . . . . 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 ) )
246233, 245syl5bi 208 . . . . . . . . . . 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 ) )
247232, 246sylbid 206 . . . . . . . . . 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 ) )
248189, 247sylan2 460 . . . . . . . . 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 ) )
249182, 248syl5 28 . . . . . . . 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 ) )
250249ralrimivva 2635 . . . . . . 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 ) )
251250adantr 451 . . . . . 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 ) )
252 oveq2 5866 . . . . . . . . . . 11  |-  ( t  =  s  ->  (
1  -  t )  =  ( 1  -  s ) )
253252oveq1d 5873 . . . . . . . . . 10  |-  ( t  =  s  ->  (
( 1  -  t
)  x.  ( Z `
 i ) )  =  ( ( 1  -  s )  x.  ( Z `  i
) ) )
254 oveq1 5865 . . . . . . . . . 10  |-  ( t  =  s  ->  (
t  x.  ( U `
 i ) )  =  ( s  x.  ( U `  i
) ) )
255253, 254oveq12d 5876 . . . . . . . . 9  |-  ( t  =  s  ->  (
( ( 1  -  t )  x.  ( Z `  i )
)  +  ( t  x.  ( U `  i ) ) )  =  ( ( ( 1  -  s )  x.  ( Z `  i ) )  +  ( s  x.  ( U `  i )
) ) )
256255eqeq2d 2294 . . . . . . . 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 ) ) ) ) )
257256ralbidv 2563 . . . . . . 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 ) ) ) ) )
258257reu4 2959 . . . . . 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 ) ) )
259178, 251, 258sylanbrc 645 . . . . 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 ) ) ) )
260 df-reu 2550 . . . . 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 )
) ) ) )
261259, 260sylib 188 . . . 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 ) ) ) ) )
262261ralrimiva 2626 . . 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 ) ) ) ) )
263 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 )
) ) ) ) }
264263