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

Theorem axcontlem8 24997
Description: Lemma for axcont 25002. 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 24995 . . . . . . . 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 436 . . . . . . 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 24995 . . . . . . . 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 436 . . . . . . 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 24995 . . . . . . . 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 436 . . . . . . 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 1343 . . . . . 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 431 . . . . 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 467 . . . 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 1346 . . . . 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 11756 . . . . . . . . . . . 12  |-  0  e.  ( 0 [,] 1
)
14 simplr1 1048 . . . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . 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 11744 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  P )  e.  ( 0 [,) +oo )  <->  ( ( F `
 P )  e.  RR  /\  0  <_ 
( F `  P
) ) )
1716simplbi 462 . . . . . . . . . . . . . . . 16  |-  ( ( F `  P )  e.  ( 0 [,) +oo )  ->  ( F `
 P )  e.  RR )
1815, 17syl 17 . . . . . . . . . . . . . . 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 9675 . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . 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 4449 . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . 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 1049 . . . . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . . 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 11744 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  Q )  e.  ( 0 [,) +oo )  <->  ( ( F `
 Q )  e.  RR  /\  0  <_ 
( F `  Q
) ) )
2928simplbi 462 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  Q )  e.  ( 0 [,) +oo )  ->  ( F `
 Q )  e.  RR )
3027, 29syl 17 . . . . . . . . . . . . . . . 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 9783 . . . . . . . . . . . . . . 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 931 . . . . . . . . . . . . . 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 759 . . . . . . . . . . . . . 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 1046 . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 24928 . . . . . . . . . . . . . . 15  |-  ( ( Z  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( Z `  i )  e.  CC )
3836, 37sylancom 672 . . . . . . . . . . . . . 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 1047 . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 24928 . . . . . . . . . . . . . . 15  |-  ( ( U  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( U `  i )  e.  CC )
4341, 42sylancom 672 . . . . . . . . . . . . . 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 9603 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  CC
45 simpl 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( F `  P )  e.  CC )
46 subcl 9880 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  e.  CC  /\  ( F `  P )  e.  CC )  -> 
( 1  -  ( F `  P )
)  e.  CC )
4744, 45, 46sylancr 668 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( 1  -  ( F `  P ) )  e.  CC )
48 simprl 763 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( Z `  i )  e.  CC )
4947, 48mulcld 9669 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( (
1  -  ( F `
 P ) )  x.  ( Z `  i ) )  e.  CC )
50 mulcl 9629 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F `  P
)  e.  CC  /\  ( U `  i )  e.  CC )  -> 
( ( F `  P )  x.  ( U `  i )
)  e.  CC )
5150adantrl 721 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( ( F `  P )  x.  ( U `  i
) )  e.  CC )
5249, 51addcld 9668 . . . . . . . . . . . . . . . . . . 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 9667 . . . . . . . . . . . . . . . . . 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 9837 . . . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . 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 9839 . . . . . . . . . . . . . . . . 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 2465 . . . . . . . . . . . . . . . 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 1025 . . . . . . . . . . . . . . 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 6312 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  P )  =  ( F `  Q )  ->  (
1  -  ( F `
 P ) )  =  ( 1  -  ( F `  Q
) ) )
6059oveq1d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  P )  =  ( F `  Q )  ->  (
( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( F `  Q ) )  x.  ( Z `  i
) ) )
61 oveq1 6311 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  P )  =  ( F `  Q )  ->  (
( F `  P
)  x.  ( U `
 i ) )  =  ( ( F `
 Q )  x.  ( U `  i
) ) )
6260, 61oveq12d 6322 . . . . . . . . . . . . . . . . 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 6312 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  P )  =  ( F `  R )  ->  (
1  -  ( F `
 P ) )  =  ( 1  -  ( F `  R
) ) )
6463oveq1d 6319 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  P )  =  ( F `  R )  ->  (
( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) ) )
65 oveq1 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  P )  =  ( F `  R )  ->  (
( F `  P
)  x.  ( U `
 i ) )  =  ( ( F `
 R )  x.  ( U `  i
) ) )
6664, 65oveq12d 6322 . . . . . . . . . . . . . . . . . . 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 6320 . . . . . . . . . . . . . . . . . 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 6320 . . . . . . . . . . . . . . . . 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 2446 . . . . . . . . . . . . . . . 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 1028 . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . 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 1274 . . . . . . . . . . . . 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 2840 . . . . . . . . . . . 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 6312 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  0  ->  (
1  -  t )  =  ( 1  -  0 ) )
75 1m0e1 10726 . . . . . . . . . . . . . . . . . 18  |-  ( 1  -  0 )  =  1
7674, 75syl6eq 2480 . . . . . . . . . . . . . . . . 17  |-  ( t  =  0  ->  (
1  -  t )  =  1 )
7776oveq1d 6319 . . . . . . . . . . . . . . . 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 6311 . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . 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 2437 . . . . . . . . . . . . . 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 2865 . . . . . . . . . . . . 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 3183 . . . . . . . . . . . 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 668 . . . . . . . . . . 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 436 . . . . . . . . . 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 468 . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . 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 1050 . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . 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 11744 . . . . . . . . . . . . . . . 16  |-  ( ( F `  R )  e.  ( 0 [,) +oo )  <->  ( ( F `
 R )  e.  RR  /\  0  <_ 
( F `  R
) ) )
9089simplbi 462 . . . . . . . . . . . . . . 15  |-  ( ( F `  R )  e.  ( 0 [,) +oo )  ->  ( F `
 R )  e.  RR )
9188, 90syl 17 . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . 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 10235 . . . . . . . . . . . . 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 10053 . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . 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 10209 . . . . . . . . . . . . . . 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 236 . . . . . . . . . . . . . 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 10053 . . . . . . . . . . . . . 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 9798 . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . 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 2696 . . . . . . . . . . . . . . . 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 9786 . . . . . . . . . . . . . . . 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 931 . . . . . . . . . . . . . . 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 10206 . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . 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 11780 . . . . . . . . . . . . . 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 1266 . . . . . . . . . . . . 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 236 . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 9675 . . . . . . . . . . . . . . 15  |-  ( ( F `  P )  e.  ( 0 [,) +oo )  ->  ( F `
 P )  e.  CC )
113111, 112syl 17 . . . . . . . . . . . . . 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 759 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 9675 . . . . . . . . . . . . . . 15  |-  ( ( F `  Q )  e.  ( 0 [,) +oo )  ->  ( F `
 Q )  e.  CC )
117115, 116syl 17 . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . 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 9675 . . . . . . . . . . . . . . 15  |-  ( ( F `  R )  e.  ( 0 [,) +oo )  ->  ( F `
 R )  e.  CC )
120118, 119syl 17 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . 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 1033 . . . . . . . . . . . . . . . . . . . . 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 1032 . . . . . . . . . . . . . . . . . . . . 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 9992 . . . . . . . . . . . . . . . . . . . 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 1030 . . . . . . . . . . . . . . . . . . . . 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 668 . . . . . . . . . . . . . . . . . . . 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 9669 . . . . . . . . . . . . . . . . . . 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 9992 . . . . . . . . . . . . . . . . . . . 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 9880 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  CC  /\  ( F `  R )  e.  CC )  -> 
( 1  -  ( F `  R )
)  e.  CC )
13344, 125, 132sylancr 668 . . . . . . . . . . . . . . . . . . . 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 9669 . . . . . . . . . . . . . . . . . . 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 9992 . . . . . . . . . . . . . . . . . . 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 1031 . . . . . . . . . . . . . . . . . . . . 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 2696 . . . . . . . . . . . . . . . . . . . 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 10001 . . . . . . . . . . . . . . . . . . 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 10427 . . . . . . . . . . . . . . . . . 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 9666 . . . . . . . . . . . . . . . . . . . . 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 9670 . . . . . . . . . . . . . . . . . . . . . 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 10080 . . . . . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . . . . 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 6322 . . . . . . . . . . . . . . . . . . . 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 10058 . . . . . . . . . . . . . . . . . . . . . 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 1349 . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . 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 10058 . . . . . . . . . . . . . . . . . . . . . . . . 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 1349 . . . . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . . . . 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 9666 . . . . . . . . . . . . . . . . . . . . . . . 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 10081 . . . . . . . . . . . . . . . . . . . . . . . . 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 9670 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6319 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )  ->  ( ( (