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

Theorem axcontlem8 24599
Description: Lemma for axcont 24604. 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 24597 . . . . . . . 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 423 . . . . . . 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 24597 . . . . . . . 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 423 . . . . . . 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 24597 . . . . . . . 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 423 . . . . . . 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 1259 . . . . . 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 418 . . . . 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 451 . . . 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 1262 . . . . 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 10754 . . . . . . . . . . . 12  |-  0  e.  ( 0 [,] 1
)
14 simplr1 997 . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . 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 10746 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  P )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  P )  e.  RR  /\  0  <_ 
( F `  P
) ) )
1716simplbi 446 . . . . . . . . . . . . . . . 16  |-  ( ( F `  P )  e.  ( 0 [,) 
+oo )  ->  ( F `  P )  e.  RR )
1815, 17syl 15 . . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . 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 741 . . . . . . . . . . . . . . . . 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 443 . . . . . . . . . . . . . . . . 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 4049 . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . 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 998 . . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . 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 10746 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  Q )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  Q )  e.  RR  /\  0  <_ 
( F `  Q
) ) )
2928simplbi 446 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  Q )  e.  ( 0 [,) 
+oo )  ->  ( F `  Q )  e.  RR )
3027, 29syl 15 . . . . . . . . . . . . . . . 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 8961 . . . . . . . . . . . . . . 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 888 . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . 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 995 . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . 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 24530 . . . . . . . . . . . . . . 15  |-  ( ( Z  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( Z `  i )  e.  CC )
3836, 37sylancom 648 . . . . . . . . . . . . . 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 996 . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . 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 24530 . . . . . . . . . . . . . . 15  |-  ( ( U  e.  ( EE
`  N )  /\  i  e.  ( 1 ... N ) )  ->  ( U `  i )  e.  CC )
4341, 42sylancom 648 . . . . . . . . . . . . . 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 8795 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  CC
45 simpl 443 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( F `  P )  e.  CC )
46 subcl 9051 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  e.  CC  /\  ( F `  P )  e.  CC )  -> 
( 1  -  ( F `  P )
)  e.  CC )
4744, 45, 46sylancr 644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( 1  -  ( F `  P ) )  e.  CC )
48 simprl 732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( Z `  i )  e.  CC )
4947, 48mulcld 8855 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( (
1  -  ( F `
 P ) )  x.  ( Z `  i ) )  e.  CC )
50 mulcl 8821 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F `  P
)  e.  CC  /\  ( U `  i )  e.  CC )  -> 
( ( F `  P )  x.  ( U `  i )
)  e.  CC )
5150adantrl 696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  P
)  e.  CC  /\  ( ( Z `  i )  e.  CC  /\  ( U `  i
)  e.  CC ) )  ->  ( ( F `  P )  x.  ( U `  i
) )  e.  CC )
5249, 51addcld 8854 . . . . . . . . . . . . . . . . . . 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 8853 . . . . . . . . . . . . . . . . . 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 9010 . . . . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . . . . 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 9012 . . . . . . . . . . . . . . . . 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 2316 . . . . . . . . . . . . . . . 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 974 . . . . . . . . . . . . . . 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 5866 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  P )  =  ( F `  Q )  ->  (
1  -  ( F `
 P ) )  =  ( 1  -  ( F `  Q
) ) )
6059oveq1d 5873 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  P )  =  ( F `  Q )  ->  (
( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( F `  Q ) )  x.  ( Z `  i
) ) )
61 oveq1 5865 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  P )  =  ( F `  Q )  ->  (
( F `  P
)  x.  ( U `
 i ) )  =  ( ( F `
 Q )  x.  ( U `  i
) ) )
6260, 61oveq12d 5876 . . . . . . . . . . . . . . . . 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 5866 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  P )  =  ( F `  R )  ->  (
1  -  ( F `
 P ) )  =  ( 1  -  ( F `  R
) ) )
6463oveq1d 5873 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  P )  =  ( F `  R )  ->  (
( 1  -  ( F `  P )
)  x.  ( Z `
 i ) )  =  ( ( 1  -  ( F `  R ) )  x.  ( Z `  i
) ) )
65 oveq1 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  P )  =  ( F `  R )  ->  (
( F `  P
)  x.  ( U `
 i ) )  =  ( ( F `
 R )  x.  ( U `  i
) ) )
6664, 65oveq12d 5876 . . . . . . . . . . . . . . . . . . 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 5874 . . . . . . . . . . . . . . . . . 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 5874 . . . . . . . . . . . . . . . . 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 2298 . . . . . . . . . . . . . . . 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 977 . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . 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 1191 . . . . . . . . . . . . 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 2626 . . . . . . . . . . . 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 5866 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  0  ->  (
1  -  t )  =  ( 1  -  0 ) )
7544subid1i 9118 . . . . . . . . . . . . . . . . . 18  |-  ( 1  -  0 )  =  1
7674, 75syl6eq 2331 . . . . . . . . . . . . . . . . 17  |-  ( t  =  0  ->  (
1  -  t )  =  1 )
7776oveq1d 5873 . . . . . . . . . . . . . . . 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 5865 . . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . . 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 2294 . . . . . . . . . . . . . 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 2563 . . . . . . . . . . . . 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 2884 . . . . . . . . . . . 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 644 . . . . . . . . . . 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 423 . . . . . . . . . 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 452 . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . 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 999 . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . 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 10746 . . . . . . . . . . . . . . . 16  |-  ( ( F `  R )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  R )  e.  RR  /\  0  <_ 
( F `  R
) ) )
9089simplbi 446 . . . . . . . . . . . . . . 15  |-  ( ( F `  R )  e.  ( 0 [,) 
+oo )  ->  ( F `  R )  e.  RR )
9188, 90syl 15 . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . 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 741 . . . . . . . . . . . . . 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 9388 . . . . . . . . . . . . 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 9211 . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . 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 9362 . . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . . 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 9211 . . . . . . . . . . . . . 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 8973 . . . . . . . . . . . . . . . 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 443 . . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . 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 8964 . . . . . . . . . . . . . . . 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 888 . . . . . . . . . . . . . . 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 9359 . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . 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 24080 . . . . . . . . . . . . . 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 1183 . . . . . . . . . . . . 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 223 . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . . 15  |-  ( ( F `  P )  e.  ( 0 [,) 
+oo )  ->  ( F `  P )  e.  CC )
113111, 112syl 15 . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . . 15  |-  ( ( F `  Q )  e.  ( 0 [,) 
+oo )  ->  ( F `  Q )  e.  CC )
117115, 116syl 15 . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . . 15  |-  ( ( F `  R )  e.  ( 0 [,) 
+oo )  ->  ( F `  R )  e.  CC )
120118, 119syl 15 . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . 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 457 . . . . . . . . . . . . . 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 982 . . . . . . . . . . . . . . . . . . . . 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 981 . . . . . . . . . . . . . . . . . . . . 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 9157 . . . . . . . . . . . . . . . . . . . 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 979 . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . 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 8855 . . . . . . . . . . . . . . . . . . 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 9157 . . . . . . . . . . . . . . . . . . . 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 9051 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  CC  /\  ( F `  R )  e.  CC )  -> 
( 1  -  ( F `  R )
)  e.  CC )
13344, 125, 132sylancr 644 . . . . . . . . . . . . . . . . . . . 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 8855 . . . . . . . . . . . . . . . . . . 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 9157 . . . . . . . . . . . . . . . . . . 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 980 . . . . . . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . . . . . 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 )
)
138 subeq0 9073 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( F `  R
)  e.  CC  /\  ( F `  P )  e.  CC )  -> 
( ( ( F `
 R )  -  ( F `  P ) )  =  0  <->  ( F `  R )  =  ( F `  P ) ) )
139125, 128, 138syl2anc 642 . . . . . . . . . . . . . . . . . . . . 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 ) )  =  0  <->  ( F `  R )  =  ( F `  P ) ) )
140139necon3bid 2481 . . . . . . . . . . . . . . . . . . . 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 ) )  =/=  0  <->  ( F `  R )  =/=  ( F `  P )
) )
141137, 140mpbird 223 . . . . . . . . . . . . . . . . . . 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 )
142130, 134, 135, 141divdird 9574 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
143135mulid1d 8852 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
144135, 126mulcomd 8856 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
145126, 125, 128subdid 9235 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
146144, 145eqtrd 2315 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
147143, 146oveq12d 5876 . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
148 subdi 9213 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
14944, 148mp3an2 1265 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
150135, 126, 149syl2anc 642 . . . . . . . . . . . . . . . . . . . 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
) ) ) )
151 subdi 9213 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
15244, 151mp3an2 1265 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
153127, 128, 152syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
154127mulid1d 8852 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
155125, 126, 128subdird 9236 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( F `  P )  e.  CC  /\  ( F `