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

Theorem axcontlem8 23229
Description: Lemma for axcont 23234. A point in  D is between two others if its function value falls in the middle. (Contributed by Scott Fenton, 18-Jun-2013.)
Hypotheses
Ref Expression
axcontlem8.1  |-  D  =  { p  e.  ( EE `  N )  |  ( U  Btwn  <. Z ,  p >.  \/  p  Btwn  <. Z ,  U >. ) }
axcontlem8.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
axcontlem8  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  ( P  e.  D  /\  Q  e.  D  /\  R  e.  D )
)  ->  ( (
( F `  P
)  <_  ( F `  Q )  /\  ( F `  Q )  <_  ( F `  R
) )  ->  Q  Btwn  <. P ,  R >. ) )
Distinct variable groups:    D, p, t, x    F, p, i, t    x, i, N, p, t    P, i, p, t, x    Q, i, p, t, x    R, i, p, t, x    U, i, p, t, x    i, Z, p, t, x
Allowed substitution hints:    D( i)    F( x)

Proof of Theorem axcontlem8
StepHypRef Expression
1 axcontlem8.1 . . . . . . . . 9  |-  D  =  { p  e.  ( EE `  N )  |  ( U  Btwn  <. Z ,  p >.  \/  p  Btwn  <. Z ,  U >. ) }
2 axcontlem8.2 . . . . . . . . 9  |-  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 )
) ) ) ) }
31, 2axcontlem6 23227 . . . . . . . 8  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  P  e.  D )  ->  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( P `  i )  =  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) ) )
43ex 434 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  -> 
( P  e.  D  ->  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( P `  i
)  =  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) ) ) )
51, 2axcontlem6 23227 . . . . . . . 8  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  Q  e.  D )  ->  (
( F `  Q
)  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( Q `  i )  =  ( ( ( 1  -  ( F `
 Q ) )  x.  ( Z `  i ) )  +  ( ( F `  Q )  x.  ( U `  i )
) ) ) )
65ex 434 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  -> 
( Q  e.  D  ->  ( ( F `  Q )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( Q `  i
)  =  ( ( ( 1  -  ( F `  Q )
)  x.  ( Z `
 i ) )  +  ( ( F `
 Q )  x.  ( U `  i
) ) ) ) ) )
71, 2axcontlem6 23227 . . . . . . . 8  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  R  e.  D )  ->  (
( F `  R
)  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( R `  i )  =  ( ( ( 1  -  ( F `
 R ) )  x.  ( Z `  i ) )  +  ( ( F `  R )  x.  ( U `  i )
) ) ) )
87ex 434 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  -> 
( R  e.  D  ->  ( ( F `  R )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( R `  i
)  =  ( ( ( 1  -  ( F `  R )
)  x.  ( Z `
 i ) )  +  ( ( F `
 R )  x.  ( U `  i
) ) ) ) ) )
94, 6, 83anim123d 1296 . . . . . 6  |-  ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  -> 
( ( P  e.  D  /\  Q  e.  D  /\  R  e.  D )  ->  (
( ( F `  P )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( P `  i
)  =  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  /\  ( ( F `
 Q )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N
) ( Q `  i )  =  ( ( ( 1  -  ( F `  Q
) )  x.  ( Z `  i )
)  +  ( ( F `  Q )  x.  ( U `  i ) ) ) )  /\  ( ( F `  R )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N
) ( R `  i )  =  ( ( ( 1  -  ( F `  R
) )  x.  ( Z `  i )
)  +  ( ( F `  R )  x.  ( U `  i ) ) ) ) ) ) )
109imp 429 . . . . 5  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  ( P  e.  D  /\  Q  e.  D  /\  R  e.  D )
)  ->  ( (
( F `  P
)  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( P `  i )  =  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) )  /\  ( ( F `  Q )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( Q `  i
)  =  ( ( ( 1  -  ( F `  Q )
)  x.  ( Z `
 i ) )  +  ( ( F `
 Q )  x.  ( U `  i
) ) ) )  /\  ( ( F `
 R )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N
) ( R `  i )  =  ( ( ( 1  -  ( F `  R
) )  x.  ( Z `  i )
)  +  ( ( F `  R )  x.  ( U `  i ) ) ) ) ) )
1110adantr 465 . . . 4  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  ( P  e.  D  /\  Q  e.  D  /\  R  e.  D )
)  /\  ( ( F `  P )  <_  ( F `  Q
)  /\  ( F `  Q )  <_  ( F `  R )
) )  ->  (
( ( F `  P )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( P `  i
)  =  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  /\  ( ( F `
 Q )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N
) ( Q `  i )  =  ( ( ( 1  -  ( F `  Q
) )  x.  ( Z `  i )
)  +  ( ( F `  Q )  x.  ( U `  i ) ) ) )  /\  ( ( F `  R )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N
) ( R `  i )  =  ( ( ( 1  -  ( F `  R
) )  x.  ( Z `  i )
)  +  ( ( F `  R )  x.  ( U `  i ) ) ) ) ) )
12 3an6 1299 . . . . 5  |-  ( ( ( ( F `  P )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N ) ( P `  i
)  =  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  /\  ( ( F `
 Q )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N
) ( Q `  i )  =  ( ( ( 1  -  ( F `  Q
) )  x.  ( Z `  i )
)  +  ( ( F `  Q )  x.  ( U `  i ) ) ) )  /\  ( ( F `  R )  e.  ( 0 [,) +oo )  /\  A. i  e.  ( 1 ... N
) ( R `  i )  =  ( ( ( 1  -  ( F `  R
) )  x.  ( Z `  i )
)  +  ( ( F `  R )  x.  ( U `  i ) ) ) ) )  <->  ( (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) )  /\  ( A. i  e.  (
1 ... N ) ( P `  i )  =  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( Q `  i )  =  ( ( ( 1  -  ( F `
 Q ) )  x.  ( Z `  i ) )  +  ( ( F `  Q )  x.  ( U `  i )
) )  /\  A. i  e.  ( 1 ... N ) ( R `  i )  =  ( ( ( 1  -  ( F `
 R ) )  x.  ( Z `  i ) )  +  ( ( F `  R )  x.  ( U `  i )
) ) ) ) )
13 0elunit 11415 . . . . . . . . . . . 12  |-  0  e.  ( 0 [,] 1
)
14 simplr1 1030 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) )  ->  ( F `  P )  e.  ( 0 [,) +oo )
)
1514ad2antlr 726 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  P )  e.  ( 0 [,) +oo ) )
16 elrege0 11404 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  P )  e.  ( 0 [,) +oo )  <->  ( ( F `
 P )  e.  RR  /\  0  <_ 
( F `  P
) ) )
1716simplbi 460 . . . . . . . . . . . . . . . 16  |-  ( ( F `  P )  e.  ( 0 [,) +oo )  ->  ( F `
 P )  e.  RR )
1815, 17syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  P )  e.  RR )
1918recnd 9424 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  P )  e.  CC )
20 simprrl 763 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  P
)  =  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  P )  <_  ( F `  Q )
)
2120adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  P )  <_  ( F `  Q
) )
22 simprrr 764 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  P
)  =  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  Q )  <_  ( F `  R )
)
23 simpl 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  P
)  =  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  P )  =  ( F `  R ) )
2422, 23breqtrrd 4330 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  P
)  =  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  Q )  <_  ( F `  P )
)
2524adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  Q )  <_  ( F `  P
) )
26 simplr2 1031 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) )  ->  ( F `  Q )  e.  ( 0 [,) +oo )
)
2726ad2antlr 726 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  Q )  e.  ( 0 [,) +oo ) )
28 elrege0 11404 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  Q )  e.  ( 0 [,) +oo )  <->  ( ( F `
 Q )  e.  RR  /\  0  <_ 
( F `  Q
) ) )
2928simplbi 460 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  Q )  e.  ( 0 [,) +oo )  ->  ( F `
 Q )  e.  RR )
3027, 29syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  Q )  e.  RR )
3118, 30letri3d 9528 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( F `  P
)  =  ( F `
 Q )  <->  ( ( F `  P )  <_  ( F `  Q
)  /\  ( F `  Q )  <_  ( F `  P )
) ) )
3221, 25, 31mpbir2and 913 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  P )  =  ( F `  Q ) )
33 simpll 753 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  P )  =  ( F `  R ) )
34 simpll2 1028 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  ->  Z  e.  ( EE `  N ) )
3534adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) )  ->  Z  e.  ( EE `  N ) )
3635ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  Z  e.  ( EE `  N
) )
37 fveecn 23160 . . . . . . . . . . . . . . 15  |-  ( ( Z  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( Z `  i )  e.  CC )
3836, 37sylancom 667 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( Z `  i )  e.  CC )
39 simpll3 1029 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  ->  U  e.  ( EE `  N ) )
4039adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) )  ->  U  e.  ( EE `  N ) )
4140ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  U  e.  ( EE `  N
) )
42 fveecn 23160 . . . . . . . . . . . . . . 15  |-  ( ( U  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( U `  i )  e.  CC )
4341, 42sylancom 667 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( U `  i )  e.  CC )
44 ax-1cn 9352 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  CC
45 simpl 457 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( F `  P )  e.  CC )
46 subcl 9621 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  e.  CC  /\  ( F `  P )  e.  CC )  -> 
( 1  -  ( F `  P )
)  e.  CC )
4744, 45, 46sylancr 663 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( 1  -  ( F `  P ) )  e.  CC )
48 simprl 755 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( Z `  i )  e.  CC )
4947, 48mulcld 9418 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( (
1  -  ( F `
 P ) )  x.  ( Z `  i ) )  e.  CC )
50 mulcl 9378 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F `  P
)  e.  CC  /\  ( U `  i )  e.  CC )  -> 
( ( F `  P )  x.  ( U `  i )
)  e.  CC )
5150adantrl 715 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( ( F `  P )  x.  ( U `  i
) )  e.  CC )
5249, 51addcld 9417 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( (
( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) )  e.  CC )
5352mulid2d 9416 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( 1  x.  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) )  =  ( ( ( 1  -  ( F `  P ) )  x.  ( Z `  i
) )  +  ( ( F `  P
)  x.  ( U `
 i ) ) ) )
5452mul02d 9579 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( 0  x.  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) )  =  0 )
5553, 54oveq12d 6121 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( (
1  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `  P ) )  x.  ( Z `  i
) )  +  ( ( F `  P
)  x.  ( U `
 i ) ) ) ) )  =  ( ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) )  +  0 ) )
5652addid1d 9581 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( (
( ( 1  -  ( F `  P
) )  x.  ( Z `  i )
)  +  ( ( F `  P )  x.  ( U `  i ) ) )  +  0 )  =  ( ( ( 1  -  ( F `  P ) )  x.  ( Z `  i
) )  +  ( ( F `  P
)  x.  ( U `
 i ) ) ) )
5755, 56eqtr2d 2476 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( (
( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) )  =  ( ( 1  x.  ( ( ( 1  -  ( F `  P ) )  x.  ( Z `  i
) )  +  ( ( F `  P
)  x.  ( U `
 i ) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) ) ) )
58573adant2 1007 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( F `  P )  =  ( F `  Q )  /\  ( F `  P )  =  ( F `  R ) )  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i )  e.  CC ) )  -> 
( ( ( 1  -  ( F `  P ) )  x.  ( Z `  i
) )  +  ( ( F `  P
)  x.  ( U `
 i ) ) )  =  ( ( 1  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `  P ) )  x.  ( Z `  i
) )  +  ( ( F `  P
)  x.  ( U `
 i ) ) ) ) ) )
59 oveq2 6111 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  P )  =  ( F `  Q )  ->  (
1  -  ( F `
 P ) )  =  ( 1  -  ( F `  Q
) ) )
6059oveq1d 6118 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  P )  =  ( F `  Q )  ->  (
( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( F `  Q ) )  x.  ( Z `  i
) ) )
61 oveq1 6110 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  P )  =  ( F `  Q )  ->  (
( F `  P
)  x.  ( U `
 i ) )  =  ( ( F `
 Q )  x.  ( U `  i
) ) )
6260, 61oveq12d 6121 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  P )  =  ( F `  Q )  ->  (
( ( 1  -  ( F `  P
) )  x.  ( Z `  i )
)  +  ( ( F `  P )  x.  ( U `  i ) ) )  =  ( ( ( 1  -  ( F `
 Q ) )  x.  ( Z `  i ) )  +  ( ( F `  Q )  x.  ( U `  i )
) ) )
63 oveq2 6111 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  P )  =  ( F `  R )  ->  (
1  -  ( F `
 P ) )  =  ( 1  -  ( F `  R
) ) )
6463oveq1d 6118 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  P )  =  ( F `  R )  ->  (
( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) ) )
65 oveq1 6110 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  P )  =  ( F `  R )  ->  (
( F `  P
)  x.  ( U `
 i ) )  =  ( ( F `
 R )  x.  ( U `  i
) ) )
6664, 65oveq12d 6121 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  P )  =  ( F `  R )  ->  (
( ( 1  -  ( F `  P
) )  x.  ( Z `  i )
)  +  ( ( F `  P )  x.  ( U `  i ) ) )  =  ( ( ( 1  -  ( F `
 R ) )  x.  ( Z `  i ) )  +  ( ( F `  R )  x.  ( U `  i )
) ) )
6766oveq2d 6119 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  P )  =  ( F `  R )  ->  (
0  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  =  ( 0  x.  ( ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) )  +  ( ( F `  R
)  x.  ( U `
 i ) ) ) ) )
6867oveq2d 6119 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  P )  =  ( F `  R )  ->  (
( 1  x.  (
( ( 1  -  ( F `  P
) )  x.  ( Z `  i )
)  +  ( ( F `  P )  x.  ( U `  i ) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) ) )  =  ( ( 1  x.  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) )  +  ( 0  x.  (
( ( 1  -  ( F `  R
) )  x.  ( Z `  i )
)  +  ( ( F `  R )  x.  ( U `  i ) ) ) ) ) )
6962, 68eqeqan12d 2458 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  P
)  =  ( F `
 Q )  /\  ( F `  P )  =  ( F `  R ) )  -> 
( ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) )  =  ( ( 1  x.  (
( ( 1  -  ( F `  P
) )  x.  ( Z `  i )
)  +  ( ( F `  P )  x.  ( U `  i ) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) ) )  <-> 
( ( ( 1  -  ( F `  Q ) )  x.  ( Z `  i
) )  +  ( ( F `  Q
)  x.  ( U `
 i ) ) )  =  ( ( 1  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) )  +  ( ( F `  R
)  x.  ( U `
 i ) ) ) ) ) ) )
70693ad2ant2 1010 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( F `  P )  =  ( F `  Q )  /\  ( F `  P )  =  ( F `  R ) )  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i )  e.  CC ) )  -> 
( ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) )  =  ( ( 1  x.  (
( ( 1  -  ( F `  P
) )  x.  ( Z `  i )
)  +  ( ( F `  P )  x.  ( U `  i ) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) ) )  <-> 
( ( ( 1  -  ( F `  Q ) )  x.  ( Z `  i
) )  +  ( ( F `  Q
)  x.  ( U `
 i ) ) )  =  ( ( 1  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) )  +  ( ( F `  R
)  x.  ( U `
 i ) ) ) ) ) ) )
7158, 70mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( F `  P )  =  ( F `  Q )  /\  ( F `  P )  =  ( F `  R ) )  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i )  e.  CC ) )  -> 
( ( ( 1  -  ( F `  Q ) )  x.  ( Z `  i
) )  +  ( ( F `  Q
)  x.  ( U `
 i ) ) )  =  ( ( 1  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) )  +  ( ( F `  R
)  x.  ( U `
 i ) ) ) ) ) )
7219, 32, 33, 38, 43, 71syl122anc 1227 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  P )  =  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE
`  N )  /\  U  e.  ( EE `  N ) )  /\  Z  =/=  U )  /\  ( ( F `  P )  e.  ( 0 [,) +oo )  /\  ( F `  Q
)  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  (
( ( 1  -  ( F `  Q
) )  x.  ( Z `  i )
)  +  ( ( F `  Q )  x.  ( U `  i ) ) )  =  ( ( 1  x.  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) )  +  ( 0  x.  (
( ( 1  -  ( F `  R
) )  x.  ( Z `  i )
)  +  ( ( F `  R )  x.  ( U `  i ) ) ) ) ) )
7372ralrimiva 2811 . . . . . . . . . . . 12  |-  ( ( ( F `  P
)  =  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  A. i  e.  ( 1 ... N
) ( ( ( 1  -  ( F `
 Q ) )  x.  ( Z `  i ) )  +  ( ( F `  Q )  x.  ( U `  i )
) )  =  ( ( 1  x.  (
( ( 1  -  ( F `  P
) )  x.  ( Z `  i )
)  +  ( ( F `  P )  x.  ( U `  i ) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `
 R ) )  x.  ( Z `  i ) )  +  ( ( F `  R )  x.  ( U `  i )
) ) ) ) )
74 oveq2 6111 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  0  ->  (
1  -  t )  =  ( 1  -  0 ) )
75 1m0e1 10444 . . . . . . . . . . . . . . . . . 18  |-  ( 1  -  0 )  =  1
7674, 75syl6eq 2491 . . . . . . . . . . . . . . . . 17  |-  ( t  =  0  ->  (
1  -  t )  =  1 )
7776oveq1d 6118 . . . . . . . . . . . . . . . 16  |-  ( t  =  0  ->  (
( 1  -  t
)  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  =  ( 1  x.  ( ( ( 1  -  ( F `  P ) )  x.  ( Z `  i
) )  +  ( ( F `  P
)  x.  ( U `
 i ) ) ) ) )
78 oveq1 6110 . . . . . . . . . . . . . . . 16  |-  ( t  =  0  ->  (
t  x.  ( ( ( 1  -  ( F `  R )
)  x.  ( Z `
 i ) )  +  ( ( F `
 R )  x.  ( U `  i
) ) ) )  =  ( 0  x.  ( ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) )  +  ( ( F `  R
)  x.  ( U `
 i ) ) ) ) )
7977, 78oveq12d 6121 . . . . . . . . . . . . . . 15  |-  ( t  =  0  ->  (
( ( 1  -  t )  x.  (
( ( 1  -  ( F `  P
) )  x.  ( Z `  i )
)  +  ( ( F `  P )  x.  ( U `  i ) ) ) )  +  ( t  x.  ( ( ( 1  -  ( F `
 R ) )  x.  ( Z `  i ) )  +  ( ( F `  R )  x.  ( U `  i )
) ) ) )  =  ( ( 1  x.  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) )  +  ( 0  x.  (
( ( 1  -  ( F `  R
) )  x.  ( Z `  i )
)  +  ( ( F `  R )  x.  ( U `  i ) ) ) ) ) )
8079eqeq2d 2454 . . . . . . . . . . . . . 14  |-  ( t  =  0  ->  (
( ( ( 1  -  ( F `  Q ) )  x.  ( Z `  i
) )  +  ( ( F `  Q
)  x.  ( U `
 i ) ) )  =  ( ( ( 1  -  t
)  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  +  ( t  x.  ( ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) )  +  ( ( F `  R
)  x.  ( U `
 i ) ) ) ) )  <->  ( (
( 1  -  ( F `  Q )
)  x.  ( Z `
 i ) )  +  ( ( F `
 Q )  x.  ( U `  i
) ) )  =  ( ( 1  x.  ( ( ( 1  -  ( F `  P ) )  x.  ( Z `  i
) )  +  ( ( F `  P
)  x.  ( U `
 i ) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `  R )
)  x.  ( Z `
 i ) )  +  ( ( F `
 R )  x.  ( U `  i
) ) ) ) ) ) )
8180ralbidv 2747 . . . . . . . . . . . . 13  |-  ( t  =  0  ->  ( A. i  e.  (
1 ... N ) ( ( ( 1  -  ( F `  Q
) )  x.  ( Z `  i )
)  +  ( ( F `  Q )  x.  ( U `  i ) ) )  =  ( ( ( 1  -  t )  x.  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) )  +  ( t  x.  (
( ( 1  -  ( F `  R
) )  x.  ( Z `  i )
)  +  ( ( F `  R )  x.  ( U `  i ) ) ) ) )  <->  A. i  e.  ( 1 ... N
) ( ( ( 1  -  ( F `
 Q ) )  x.  ( Z `  i ) )  +  ( ( F `  Q )  x.  ( U `  i )
) )  =  ( ( 1  x.  (
( ( 1  -  ( F `  P
) )  x.  ( Z `  i )
)  +  ( ( F `  P )  x.  ( U `  i ) ) ) )  +  ( 0  x.  ( ( ( 1  -  ( F `
 R ) )  x.  ( Z `  i ) )  +  ( ( F `  R )  x.  ( U `  i )
) ) ) ) ) )
8281rspcev 3085 . . . . . . . . . . . 12  |-  ( ( 0  e.  ( 0 [,] 1 )  /\  A. i  e.  ( 1 ... N ) ( ( ( 1  -  ( F `  Q
) )  x.  ( Z `  i )
)  +  ( ( F `  Q )  x.  ( U `  i ) ) )  =  ( ( 1  x.  ( ( ( 1  -  ( F `
 P ) )  x.  ( Z `  i ) )  +  ( ( F `  P )  x.  ( U `  i )
) ) )  +  ( 0  x.  (
( ( 1  -  ( F `  R
) )  x.  ( Z `  i )
)  +  ( ( F `  R )  x.  ( U `  i ) ) ) ) ) )  ->  E. t  e.  (
0 [,] 1 ) A. i  e.  ( 1 ... N ) ( ( ( 1  -  ( F `  Q ) )  x.  ( Z `  i
) )  +  ( ( F `  Q
)  x.  ( U `
 i ) ) )  =  ( ( ( 1  -  t
)  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  +  ( t  x.  ( ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) )  +  ( ( F `  R
)  x.  ( U `
 i ) ) ) ) ) )
8313, 73, 82sylancr 663 . . . . . . . . . . 11  |-  ( ( ( F `  P
)  =  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  E. t  e.  ( 0 [,] 1
) A. i  e.  ( 1 ... N
) ( ( ( 1  -  ( F `
 Q ) )  x.  ( Z `  i ) )  +  ( ( F `  Q )  x.  ( U `  i )
) )  =  ( ( ( 1  -  t )  x.  (
( ( 1  -  ( F `  P
) )  x.  ( Z `  i )
)  +  ( ( F `  P )  x.  ( U `  i ) ) ) )  +  ( t  x.  ( ( ( 1  -  ( F `
 R ) )  x.  ( Z `  i ) )  +  ( ( F `  R )  x.  ( U `  i )
) ) ) ) )
8483ex 434 . . . . . . . . . 10  |-  ( ( F `  P )  =  ( F `  R )  ->  (
( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) )  ->  E. t  e.  ( 0 [,] 1 ) A. i  e.  ( 1 ... N ) ( ( ( 1  -  ( F `  Q ) )  x.  ( Z `  i
) )  +  ( ( F `  Q
)  x.  ( U `
 i ) ) )  =  ( ( ( 1  -  t
)  x.  ( ( ( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  +  ( ( F `
 P )  x.  ( U `  i
) ) ) )  +  ( t  x.  ( ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) )  +  ( ( F `  R
)  x.  ( U `
 i ) ) ) ) ) ) )
8526adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  Q )  e.  ( 0 [,) +oo )
)
8685, 29syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  Q )  e.  RR )
87 simplr3 1032 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N
)  /\  U  e.  ( EE `  N ) )  /\  Z  =/= 
U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) )  ->  ( F `  R )  e.  ( 0 [,) +oo )
)
8887adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  R )  e.  ( 0 [,) +oo )
)
89 elrege0 11404 . . . . . . . . . . . . . . . 16  |-  ( ( F `  R )  e.  ( 0 [,) +oo )  <->  ( ( F `
 R )  e.  RR  /\  0  <_ 
( F `  R
) ) )
9089simplbi 460 . . . . . . . . . . . . . . 15  |-  ( ( F `  R )  e.  ( 0 [,) +oo )  ->  ( F `
 R )  e.  RR )
9188, 90syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  R )  e.  RR )
9214adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  P )  e.  ( 0 [,) +oo )
)
9392, 17syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  P )  e.  RR )
94 simprrr 764 . . . . . . . . . . . . . 14  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  Q )  <_  ( F `  R )
)
9586, 91, 93, 94lesub1dd 9967 . . . . . . . . . . . . 13  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( ( F `  Q )  -  ( F `  P ) )  <_ 
( ( F `  R )  -  ( F `  P )
) )
9686, 93resubcld 9788 . . . . . . . . . . . . . 14  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( ( F `  Q )  -  ( F `  P ) )  e.  RR )
97 simprrl 763 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  P )  <_  ( F `  Q )
)
9886, 93subge0d 9941 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( 0  <_  ( ( F `
 Q )  -  ( F `  P ) )  <->  ( F `  P )  <_  ( F `  Q )
) )
9997, 98mpbird 232 . . . . . . . . . . . . . 14  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  0  <_  ( ( F `  Q
)  -  ( F `
 P ) ) )
10091, 93resubcld 9788 . . . . . . . . . . . . . 14  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( ( F `  R )  -  ( F `  P ) )  e.  RR )
10193, 86, 91, 97, 94letrd 9540 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  P )  <_  ( F `  R )
)
102 simpl 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  P )  =/=  ( F `  R )
)
103102necomd 2707 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  R )  =/=  ( F `  P )
)
10493, 91ltlend 9531 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( ( F `  P )  <  ( F `  R
)  <->  ( ( F `
 P )  <_ 
( F `  R
)  /\  ( F `  R )  =/=  ( F `  P )
) ) )
105101, 103, 104mpbir2and 913 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( F `  P )  <  ( F `  R )
)
10693, 91posdifd 9938 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( ( F `  P )  <  ( F `  R
)  <->  0  <  (
( F `  R
)  -  ( F `
 P ) ) ) )
107105, 106mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  0  <  ( ( F `  R
)  -  ( F `
 P ) ) )
108 divelunit 11439 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( F `
 Q )  -  ( F `  P ) )  e.  RR  /\  0  <_  ( ( F `
 Q )  -  ( F `  P ) ) )  /\  (
( ( F `  R )  -  ( F `  P )
)  e.  RR  /\  0  <  ( ( F `
 R )  -  ( F `  P ) ) ) )  -> 
( ( ( ( F `  Q )  -  ( F `  P ) )  / 
( ( F `  R )  -  ( F `  P )
) )  e.  ( 0 [,] 1 )  <-> 
( ( F `  Q )  -  ( F `  P )
)  <_  ( ( F `  R )  -  ( F `  P ) ) ) )
10996, 99, 100, 107, 108syl22anc 1219 . . . . . . . . . . . . 13  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( (
( ( F `  Q )  -  ( F `  P )
)  /  ( ( F `  R )  -  ( F `  P ) ) )  e.  ( 0 [,] 1 )  <->  ( ( F `  Q )  -  ( F `  P ) )  <_ 
( ( F `  R )  -  ( F `  P )
) ) )
11095, 109mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  ( (
( F `  Q
)  -  ( F `
 P ) )  /  ( ( F `
 R )  -  ( F `  P ) ) )  e.  ( 0 [,] 1 ) )
11114ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F `  P )  =/=  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  P )  e.  ( 0 [,) +oo ) )
11217recnd 9424 . . . . . . . . . . . . . . 15  |-  ( ( F `  P )  e.  ( 0 [,) +oo )  ->  ( F `
 P )  e.  CC )
113111, 112syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =/=  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  P )  e.  CC )
114 simpll 753 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =/=  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  P )  =/=  ( F `  R
) )
11526ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F `  P )  =/=  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  Q )  e.  ( 0 [,) +oo ) )
11629recnd 9424 . . . . . . . . . . . . . . 15  |-  ( ( F `  Q )  e.  ( 0 [,) +oo )  ->  ( F `
 Q )  e.  CC )
117115, 116syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =/=  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  Q )  e.  CC )
11887ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F `  P )  =/=  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  R )  e.  ( 0 [,) +oo ) )
11990recnd 9424 . . . . . . . . . . . . . . 15  |-  ( ( F `  R )  e.  ( 0 [,) +oo )  ->  ( F `
 R )  e.  CC )
120118, 119syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =/=  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( F `  R )  e.  CC )
12134ad2antrl 727 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  Z  e.  ( EE `  N ) )
122121, 37sylan 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =/=  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( Z `  i )  e.  CC )
12339ad2antrl 727 . . . . . . . . . . . . . . 15  |-  ( ( ( F `  P
)  =/=  ( F `
 R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  ->  U  e.  ( EE `  N ) )
124123, 42sylan 471 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  P )  =/=  ( F `  R )  /\  ( ( ( ( N  e.  NN  /\  Z  e.  ( EE `  N )  /\  U  e.  ( EE `  N
) )  /\  Z  =/=  U )  /\  (
( F `  P
)  e.  ( 0 [,) +oo )  /\  ( F `  Q )  e.  ( 0 [,) +oo )  /\  ( F `  R )  e.  ( 0 [,) +oo ) ) )  /\  ( ( F `  P )  <_  ( F `  Q )  /\  ( F `  Q
)  <_  ( F `  R ) ) ) )  /\  i  e.  ( 1 ... N
) )  ->  ( U `  i )  e.  CC )
125 simp2r 1015 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( F `  R )  e.  CC )
126 simp2l 1014 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( F `  Q )  e.  CC )
127125, 126subcld 9731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( F `
 R )  -  ( F `  Q ) )  e.  CC )
128 simp1l 1012 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( F `  P )  e.  CC )
12944, 128, 46sylancr 663 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( 1  -  ( F `  P
) )  e.  CC )
130127, 129mulcld 9418 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( F `  R )  -  ( F `  Q ) )  x.  ( 1  -  ( F `  P )
) )  e.  CC )
131126, 128subcld 9731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( F `
 Q )  -  ( F `  P ) )  e.  CC )
132 subcl 9621 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  CC  /\  ( F `  R )  e.  CC )  -> 
( 1  -  ( F `  R )
)  e.  CC )
13344, 125, 132sylancr 663 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( 1  -  ( F `  R
) )  e.  CC )
134131, 133mulcld 9418 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( F `  Q )  -  ( F `  P ) )  x.  ( 1  -  ( F `  R )
) )  e.  CC )
135125, 128subcld 9731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( F `
 R )  -  ( F `  P ) )  e.  CC )
136 simp1r 1013 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( F `  P )  =/=  ( F `  R )
)
137136necomd 2707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( F `  R )  =/=  ( F `  P )
)
138125, 128, 137subne0d 9740 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( F `
 R )  -  ( F `  P ) )  =/=  0 )
139130, 134, 135, 138divdird 10157 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( ( ( F `  R )  -  ( F `  Q )
)  x.  ( 1  -  ( F `  P ) ) )  +  ( ( ( F `  Q )  -  ( F `  P ) )  x.  ( 1  -  ( F `  R )
) ) )  / 
( ( F `  R )  -  ( F `  P )
) )  =  ( ( ( ( ( F `  R )  -  ( F `  Q ) )  x.  ( 1  -  ( F `  P )
) )  /  (
( F `  R
)  -  ( F `
 P ) ) )  +  ( ( ( ( F `  Q )  -  ( F `  P )
)  x.  ( 1  -  ( F `  R ) ) )  /  ( ( F `
 R )  -  ( F `  P ) ) ) ) )
140135mulid1d 9415 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( F `  R )  -  ( F `  P ) )  x.  1 )  =  ( ( F `  R
)  -  ( F `
 P ) ) )
141135, 126mulcomd 9419 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( F `  R )  -  ( F `  P ) )  x.  ( F `  Q
) )  =  ( ( F `  Q
)  x.  ( ( F `  R )  -  ( F `  P ) ) ) )
142126, 125, 128subdid 9812 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( F `
 Q )  x.  ( ( F `  R )  -  ( F `  P )
) )  =  ( ( ( F `  Q )  x.  ( F `  R )
)  -  ( ( F `  Q )  x.  ( F `  P ) ) ) )
143141, 142eqtrd 2475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( F `  R )  -  ( F `  P ) )  x.  ( F `  Q
) )  =  ( ( ( F `  Q )  x.  ( F `  R )
)  -  ( ( F `  Q )  x.  ( F `  P ) ) ) )
144140, 143oveq12d 6121 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( ( F `  R
)  -  ( F `
 P ) )  x.  1 )  -  ( ( ( F `
 R )  -  ( F `  P ) )  x.  ( F `
 Q ) ) )  =  ( ( ( F `  R
)  -  ( F `
 P ) )  -  ( ( ( F `  Q )  x.  ( F `  R ) )  -  ( ( F `  Q )  x.  ( F `  P )
) ) ) )
145 subdi 9790 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F `  R )  -  ( F `  P )
)  e.  CC  /\  1  e.  CC  /\  ( F `  Q )  e.  CC )  ->  (
( ( F `  R )  -  ( F `  P )
)  x.  ( 1  -  ( F `  Q ) ) )  =  ( ( ( ( F `  R
)  -  ( F `
 P ) )  x.  1 )  -  ( ( ( F `
 R )  -  ( F `  P ) )  x.  ( F `
 Q ) ) ) )
14644, 145mp3an2 1302 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F `  R )  -  ( F `  P )
)  e.  CC  /\  ( F `  Q )  e.  CC )  -> 
( ( ( F `
 R )  -  ( F `  P ) )  x.  ( 1  -  ( F `  Q ) ) )  =  ( ( ( ( F `  R
)  -  ( F `
 P ) )  x.  1 )  -  ( ( ( F `
 R )  -  ( F `  P ) )  x.  ( F `
 Q ) ) ) )
147135, 126, 146syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( F `  R )  -  ( F `  P ) )  x.  ( 1  -  ( F `  Q )
) )  =  ( ( ( ( F `
 R )  -  ( F `  P ) )  x.  1 )  -  ( ( ( F `  R )  -  ( F `  P ) )  x.  ( F `  Q
) ) ) )
148 subdi 9790 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( F `  R )  -  ( F `  Q )
)  e.  CC  /\  1  e.  CC  /\  ( F `  P )  e.  CC )  ->  (
( ( F `  R )  -  ( F `  Q )
)  x.  ( 1  -  ( F `  P ) ) )  =  ( ( ( ( F `  R
)  -  ( F `
 Q ) )  x.  1 )  -  ( ( ( F `
 R )  -  ( F `  Q ) )  x.  ( F `
 P ) ) ) )
14944, 148mp3an2 1302 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( F `  R )  -  ( F `  Q )
)  e.  CC  /\  ( F `  P )  e.  CC )  -> 
( ( ( F `
 R )  -  ( F `  Q ) )  x.  ( 1  -  ( F `  P ) ) )  =  ( ( ( ( F `  R
)  -  ( F `
 Q ) )  x.  1 )  -  ( ( ( F `
 R )  -  ( F `  Q ) )  x.  ( F `
 P ) ) ) )
150127, 128, 149syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( F `  R )  -  ( F `  Q ) )  x.  ( 1  -  ( F `  P )
) )  =  ( ( ( ( F `
 R )  -  ( F `  Q ) )  x.  1 )  -  ( ( ( F `  R )  -  ( F `  Q ) )  x.  ( F `  P
) ) ) )
151127mulid1d 9415 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( F `  R )  -  ( F `  Q ) )  x.  1 )  =  ( ( F `  R
)  -  ( F `
 Q ) ) )
152125, 126, 128subdird 9813 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( F `  R )  -  ( F `  Q ) )  x.  ( F `  P
) )  =  ( ( ( F `  R )  x.  ( F `  P )
)  -  ( ( F `  Q )  x.  ( F `  P ) ) ) )
153125, 128mulcomd 9419 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( F `
 R )  x.  ( F `  P
) )  =  ( ( F `  P
)  x.  ( F `
 R ) ) )
154153oveq1d 6118 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `  P
)  =/=  ( F `
 R ) )  /\  ( ( F `
 Q )  e.  CC  /\  ( F `
 R )  e.  CC )  /\  (
( Z `  i
)  e.  CC  /\  ( U `  i )  e.  CC ) )  ->  ( ( ( F