Metamath Proof Explorer

Theorem axcontlem8

Description: Lemma for axcont . A point in D is between two others if its function value falls in the middle. (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypotheses 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 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 >. ) )

Proof

Step Hyp Ref Expression
1 axcontlem8.1 
 |-  D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
2 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 ) ) ) ) ) }
3 1 2 axcontlem6 
 |-  ( ( ( ( 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 ) ) ) ) )
4 3 ex 
 |-  ( ( ( 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 ) ) ) ) ) )
5 1 2 axcontlem6 
 |-  ( ( ( ( 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 ) ) ) ) )
6 5 ex 
 |-  ( ( ( 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 ) ) ) ) ) )
7 1 2 axcontlem6 
 |-  ( ( ( ( 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 ) ) ) ) )
8 7 ex 
 |-  ( ( ( 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 ) ) ) ) ) )
9 4 6 8 3anim123d 
 |-  ( ( ( 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 ) ) ) ) ) ) )
10 9 imp 
 |-  ( ( ( ( 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 ) ) ) ) ) )
11 10 adantr 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  0 e. ( 0 [,] 1 )
14 simplr1 
 |-  ( ( ( ( ( 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 ) )
15 14 ad2antlr 
 |-  ( ( ( ( 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 
 |-  ( ( F ` P ) e. ( 0 [,) +oo ) <-> ( ( F ` P ) e. RR /\ 0 <_ ( F ` P ) ) )
17 16 simplbi 
 |-  ( ( F ` P ) e. ( 0 [,) +oo ) -> ( F ` P ) e. RR )
18 15 17 syl 
 |-  ( ( ( ( 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 )
19 18 recnd 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 ) )
21 20 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 ) )
24 22 23 breqtrrd 
 |-  ( ( ( 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 ) )
25 24 adantr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( ( 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 ) )
27 26 ad2antlr 
 |-  ( ( ( ( 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 
 |-  ( ( F ` Q ) e. ( 0 [,) +oo ) <-> ( ( F ` Q ) e. RR /\ 0 <_ ( F ` Q ) ) )
29 28 simplbi 
 |-  ( ( F ` Q ) e. ( 0 [,) +oo ) -> ( F ` Q ) e. RR )
30 27 29 syl 
 |-  ( ( ( ( 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 )
31 18 30 letri3d 
 |-  ( ( ( ( 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 ) ) ) )
32 21 25 31 mpbir2and 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 ) )
35 34 adantr 
 |-  ( ( ( ( ( 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 ) )
36 35 ad2antlr 
 |-  ( ( ( ( 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 
 |-  ( ( Z e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
38 36 37 sylancom 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 ) )
40 39 adantr 
 |-  ( ( ( ( ( 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 ) )
41 40 ad2antlr 
 |-  ( ( ( ( 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 
 |-  ( ( U e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) e. CC )
43 41 42 sylancom 
 |-  ( ( ( ( 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 
 |-  1 e. CC
45 simpl 
 |-  ( ( ( F ` P ) e. CC /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( F ` P ) e. CC )
46 subcl 
 |-  ( ( 1 e. CC /\ ( F ` P ) e. CC ) -> ( 1 - ( F ` P ) ) e. CC )
47 44 45 46 sylancr 
 |-  ( ( ( F ` P ) e. CC /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( 1 - ( F ` P ) ) e. CC )
48 simprl 
 |-  ( ( ( F ` P ) e. CC /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( Z ` i ) e. CC )
49 47 48 mulcld 
 |-  ( ( ( F ` P ) e. CC /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) e. CC )
50 mulcl 
 |-  ( ( ( F ` P ) e. CC /\ ( U ` i ) e. CC ) -> ( ( F ` P ) x. ( U ` i ) ) e. CC )
51 50 adantrl 
 |-  ( ( ( F ` P ) e. CC /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( ( F ` P ) x. ( U ` i ) ) e. CC )
52 49 51 addcld 
 |-  ( ( ( 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 )
53 52 mullidd 
 |-  ( ( ( 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 ) ) ) )
54 52 mul02d 
 |-  ( ( ( 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 )
55 53 54 oveq12d 
 |-  ( ( ( 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 ) )
56 52 addridd 
 |-  ( ( ( 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 ) ) ) )
57 55 56 eqtr2d 
 |-  ( ( ( 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 ) ) ) ) ) )
58 57 3adant2 
 |-  ( ( ( 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 
 |-  ( ( F ` P ) = ( F ` Q ) -> ( 1 - ( F ` P ) ) = ( 1 - ( F ` Q ) ) )
60 59 oveq1d 
 |-  ( ( F ` P ) = ( F ` Q ) -> ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) = ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) )
61 oveq1 
 |-  ( ( F ` P ) = ( F ` Q ) -> ( ( F ` P ) x. ( U ` i ) ) = ( ( F ` Q ) x. ( U ` i ) ) )
62 60 61 oveq12d 
 |-  ( ( 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 
 |-  ( ( F ` P ) = ( F ` R ) -> ( 1 - ( F ` P ) ) = ( 1 - ( F ` R ) ) )
64 63 oveq1d 
 |-  ( ( F ` P ) = ( F ` R ) -> ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) = ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) )
65 oveq1 
 |-  ( ( F ` P ) = ( F ` R ) -> ( ( F ` P ) x. ( U ` i ) ) = ( ( F ` R ) x. ( U ` i ) ) )
66 64 65 oveq12d 
 |-  ( ( 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 ) ) ) )
67 66 oveq2d 
 |-  ( ( 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 ) ) ) ) )
68 67 oveq2d 
 |-  ( ( 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 ) ) ) ) ) )
69 62 68 eqeqan12d 
 |-  ( ( ( 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 ) ) ) ) ) ) )
70 69 3ad2ant2 
 |-  ( ( ( 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 ) ) ) ) ) ) )
71 58 70 mpbid 
 |-  ( ( ( 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 ) ) ) ) ) )
72 19 32 33 38 43 71 syl122anc 
 |-  ( ( ( ( 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 ) ) ) ) ) )
73 72 ralrimiva 
 |-  ( ( ( 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 
 |-  ( t = 0 -> ( 1 - t ) = ( 1 - 0 ) )
75 1m0e1 
 |-  ( 1 - 0 ) = 1
76 74 75 eqtrdi 
 |-  ( t = 0 -> ( 1 - t ) = 1 )
77 76 oveq1d 
 |-  ( 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 
 |-  ( 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 ) ) ) ) )
79 77 78 oveq12d 
 |-  ( 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 ) ) ) ) ) )
80 79 eqeq2d 
 |-  ( 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 ) ) ) ) ) ) )
81 80 ralbidv 
 |-  ( 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 ) ) ) ) ) ) )
82 81 rspcev 
 |-  ( ( 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 ) ) ) ) ) )
83 13 73 82 sylancr 
 |-  ( ( ( 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 ) ) ) ) ) )
84 83 ex 
 |-  ( ( 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 ) ) ) ) ) ) )
85 26 adantl 
 |-  ( ( ( 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 ) )
86 85 29 syl 
 |-  ( ( ( 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 
 |-  ( ( ( ( ( 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 ) )
88 87 adantl 
 |-  ( ( ( 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 
 |-  ( ( F ` R ) e. ( 0 [,) +oo ) <-> ( ( F ` R ) e. RR /\ 0 <_ ( F ` R ) ) )
90 89 simplbi 
 |-  ( ( F ` R ) e. ( 0 [,) +oo ) -> ( F ` R ) e. RR )
91 88 90 syl 
 |-  ( ( ( 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 )
92 14 adantl 
 |-  ( ( ( 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 ) )
93 92 17 syl 
 |-  ( ( ( 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 
 |-  ( ( ( 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 ) )
95 86 91 93 94 lesub1dd 
 |-  ( ( ( 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 ) ) )
96 86 93 resubcld 
 |-  ( ( ( 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 
 |-  ( ( ( 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 ) )
98 86 93 subge0d 
 |-  ( ( ( 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 ) ) )
99 97 98 mpbird 
 |-  ( ( ( 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 ) ) )
100 91 93 resubcld 
 |-  ( ( ( 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 )
101 93 86 91 97 94 letrd 
 |-  ( ( ( 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 
 |-  ( ( ( 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 ) )
103 102 necomd 
 |-  ( ( ( 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 ) )
104 93 91 101 103 leneltd 
 |-  ( ( ( 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 ) )
105 93 91 posdifd 
 |-  ( ( ( 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 ) ) ) )
106 104 105 mpbid 
 |-  ( ( ( 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 ) ) )
107 divelunit 
 |-  ( ( ( ( ( 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 ) ) ) )
108 96 99 100 106 107 syl22anc 
 |-  ( ( ( 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 ) ) ) )
109 95 108 mpbird 
 |-  ( ( ( 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 ) )
110 14 ad2antlr 
 |-  ( ( ( ( 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 ) )
111 17 recnd 
 |-  ( ( F ` P ) e. ( 0 [,) +oo ) -> ( F ` P ) e. CC )
112 110 111 syl 
 |-  ( ( ( ( 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 )
113 simpll 
 |-  ( ( ( ( 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 ) )
114 26 ad2antlr 
 |-  ( ( ( ( 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 ) )
115 29 recnd 
 |-  ( ( F ` Q ) e. ( 0 [,) +oo ) -> ( F ` Q ) e. CC )
116 114 115 syl 
 |-  ( ( ( ( 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 )
117 87 ad2antlr 
 |-  ( ( ( ( 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 ) )
118 90 recnd 
 |-  ( ( F ` R ) e. ( 0 [,) +oo ) -> ( F ` R ) e. CC )
119 117 118 syl 
 |-  ( ( ( ( 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 )
120 34 ad2antrl 
 |-  ( ( ( 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 ) )
121 120 37 sylan 
 |-  ( ( ( ( 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 )
122 39 ad2antrl 
 |-  ( ( ( 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 ) )
123 122 42 sylan 
 |-  ( ( ( ( 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 )
124 simp2r 
 |-  ( ( ( ( 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 )
125 simp2l 
 |-  ( ( ( ( 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 )
126 124 125 subcld 
 |-  ( ( ( ( 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 )
127 simp1l 
 |-  ( ( ( ( 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 )
128 44 127 46 sylancr 
 |-  ( ( ( ( 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 )
129 126 128 mulcld 
 |-  ( ( ( ( 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 )
130 125 127 subcld 
 |-  ( ( ( ( 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 )
131 subcl 
 |-  ( ( 1 e. CC /\ ( F ` R ) e. CC ) -> ( 1 - ( F ` R ) ) e. CC )
132 44 124 131 sylancr 
 |-  ( ( ( ( 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 )
133 130 132 mulcld 
 |-  ( ( ( ( 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 )
134 124 127 subcld 
 |-  ( ( ( ( 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 )
135 simp1r 
 |-  ( ( ( ( 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 ) )
136 135 necomd 
 |-  ( ( ( ( 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 ) )
137 124 127 136 subne0d 
 |-  ( ( ( ( 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 )
138 129 133 134 137 divdird 
 |-  ( ( ( ( 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 ) ) ) ) )
139 134 mulridd 
 |-  ( ( ( ( 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 ) ) )
140 134 125 mulcomd 
 |-  ( ( ( ( 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 ) ) ) )
141 125 124 127 subdid 
 |-  ( ( ( ( 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 ) ) ) )
142 140 141 eqtrd 
 |-  ( ( ( ( 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 ) ) ) )
143 139 142 oveq12d 
 |-  ( ( ( ( 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 ) ) ) ) )
144 subdi 
 |-  ( ( ( ( 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 ) ) ) )
145 44 144 mp3an2 
 |-  ( ( ( ( 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 ) ) ) )
146 134 125 145 syl2anc 
 |-  ( ( ( ( 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 ) ) ) )
147 subdi 
 |-  ( ( ( ( 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 ) ) ) )
148 44 147 mp3an2 
 |-  ( ( ( ( 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 ) ) ) )
149 126 127 148 syl2anc 
 |-  ( ( ( ( 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 ) ) ) )
150 126 mulridd 
 |-  ( ( ( ( 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 ) ) )
151 124 125 127 subdird 
 |-  ( ( ( ( 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 ) ) ) )
152 124 127 mulcomd 
 |-  ( ( ( ( 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 ) ) )
153 152 oveq1d 
 |-  ( ( ( ( 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 ` Q ) x. ( F ` P ) ) ) = ( ( ( F ` P ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) )
154 151 153 eqtrd 
 |-  ( ( ( ( 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 ` P ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) )
155 150 154 oveq12d 
 |-  ( ( ( ( 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 ) ) x. ( F ` P ) ) ) = ( ( ( F ` R ) - ( F ` Q ) ) - ( ( ( F ` P ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) ) )
156 149 155 eqtrd 
 |-  ( ( ( ( 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 ) ) - ( ( ( F ` P ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) ) )
157 subdi 
 |-  ( ( ( ( F ` Q ) - ( F ` P ) ) e. CC /\ 1 e. CC /\ ( F ` R ) e. CC ) -> ( ( ( F ` Q ) - ( F ` P ) ) x. ( 1 - ( F ` R ) ) ) = ( ( ( ( F ` Q ) - ( F ` P ) ) x. 1 ) - ( ( ( F ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) )
158 44 157 mp3an2 
 |-  ( ( ( ( F ` Q ) - ( F ` P ) ) e. CC /\ ( F ` R ) e. CC ) -> ( ( ( F ` Q ) - ( F ` P ) ) x. ( 1 - ( F ` R ) ) ) = ( ( ( ( F ` Q ) - ( F ` P ) ) x. 1 ) - ( ( ( F ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) )
159 130 124 158 syl2anc 
 |-  ( ( ( ( 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 ) ) ) = ( ( ( ( F ` Q ) - ( F ` P ) ) x. 1 ) - ( ( ( F ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) )
160 130 mulridd 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) )
161 125 127 124 subdird 
 |-  ( ( ( ( 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. ( F ` R ) ) = ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` P ) x. ( F ` R ) ) ) )
162 160 161 oveq12d 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) = ( ( ( F ` Q ) - ( F ` P ) ) - ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` P ) x. ( F ` R ) ) ) ) )
163 159 162 eqtrd 
 |-  ( ( ( ( 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 ) ) ) = ( ( ( F ` Q ) - ( F ` P ) ) - ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` P ) x. ( F ` R ) ) ) ) )
164 156 163 oveq12d 
 |-  ( ( ( ( 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 ` Q ) ) - ( ( ( F ` P ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) ) + ( ( ( F ` Q ) - ( F ` P ) ) - ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` P ) x. ( F ` R ) ) ) ) ) )
165 127 124 mulcld 
 |-  ( ( ( ( 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 ) x. ( F ` R ) ) e. CC )
166 125 127 mulcld 
 |-  ( ( ( ( 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 ` P ) ) e. CC )
167 165 166 subcld 
 |-  ( ( ( ( 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 ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) e. CC )
168 mulcl 
 |-  ( ( ( F ` Q ) e. CC /\ ( F ` R ) e. CC ) -> ( ( F ` Q ) x. ( F ` R ) ) e. CC )
169 168 3ad2ant2 
 |-  ( ( ( ( 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 ) ) e. CC )
170 169 165 subcld 
 |-  ( ( ( ( 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 ) x. ( F ` R ) ) ) e. CC )
171 126 130 167 170 addsub4d 
 |-  ( ( ( ( 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 ) ) + ( ( F ` Q ) - ( F ` P ) ) ) - ( ( ( ( F ` P ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) + ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` P ) x. ( F ` R ) ) ) ) ) = ( ( ( ( F ` R ) - ( F ` Q ) ) - ( ( ( F ` P ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) ) + ( ( ( F ` Q ) - ( F ` P ) ) - ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` P ) x. ( F ` R ) ) ) ) ) )
172 124 125 127 npncand 
 |-  ( ( ( ( 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 ) ) + ( ( F ` Q ) - ( F ` P ) ) ) = ( ( F ` R ) - ( F ` P ) ) )
173 165 166 169 npncan3d 
 |-  ( ( ( ( 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 ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) + ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` P ) x. ( F ` R ) ) ) ) = ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) )
174 172 173 oveq12d 
 |-  ( ( ( ( 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 ) ) + ( ( F ` Q ) - ( F ` P ) ) ) - ( ( ( ( F ` P ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) + ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` P ) x. ( F ` R ) ) ) ) ) = ( ( ( F ` R ) - ( F ` P ) ) - ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) ) )
175 164 171 174 3eqtr2d 
 |-  ( ( ( ( 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 ` Q ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) ) )
176 143 146 175 3eqtr4d 
 |-  ( ( ( ( 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 ` Q ) ) x. ( 1 - ( F ` P ) ) ) + ( ( ( F ` Q ) - ( F ` P ) ) x. ( 1 - ( F ` R ) ) ) ) )
177 129 133 addcld 
 |-  ( ( ( ( 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 ) ) ) ) e. CC )
178 subcl 
 |-  ( ( 1 e. CC /\ ( F ` Q ) e. CC ) -> ( 1 - ( F ` Q ) ) e. CC )
179 44 125 178 sylancr 
 |-  ( ( ( ( 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 ` Q ) ) e. CC )
180 177 134 179 137 divmuld 
 |-  ( ( ( ( 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 ) ) ) = ( 1 - ( F ` Q ) ) <-> ( ( ( F ` R ) - ( F ` P ) ) x. ( 1 - ( F ` Q ) ) ) = ( ( ( ( F ` R ) - ( F ` Q ) ) x. ( 1 - ( F ` P ) ) ) + ( ( ( F ` Q ) - ( F ` P ) ) x. ( 1 - ( F ` R ) ) ) ) ) )
181 176 180 mpbird 
 |-  ( ( ( ( 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 ) ) ) = ( 1 - ( F ` Q ) ) )
182 126 128 134 137 div23d 
 |-  ( ( ( ( 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 ` P ) ) ) = ( ( ( ( F ` R ) - ( F ` Q ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` P ) ) ) )
183 134 130 134 137 divsubdird 
 |-  ( ( ( ( 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 ) ) - ( ( F ` Q ) - ( F ` P ) ) ) / ( ( F ` R ) - ( F ` P ) ) ) = ( ( ( ( F ` R ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) )
184 124 125 127 nnncan2d 
 |-  ( ( ( ( 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 ) ) - ( ( F ` Q ) - ( F ` P ) ) ) = ( ( F ` R ) - ( F ` Q ) ) )
185 184 oveq1d 
 |-  ( ( ( ( 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 ) ) - ( ( F ` Q ) - ( F ` P ) ) ) / ( ( F ` R ) - ( F ` P ) ) ) = ( ( ( F ` R ) - ( F ` Q ) ) / ( ( F ` R ) - ( F ` P ) ) ) )
186 134 137 dividd 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) = 1 )
187 186 oveq1d 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) = ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) )
188 183 185 187 3eqtr3d 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) = ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) )
189 188 oveq1d 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` P ) ) ) = ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) )
190 182 189 eqtrd 
 |-  ( ( ( ( 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 ` P ) ) ) = ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) )
191 130 132 134 137 div23d 
 |-  ( ( ( ( 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 ) ) ) / ( ( F ` R ) - ( F ` P ) ) ) = ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) )
192 190 191 oveq12d 
 |-  ( ( ( ( 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 ` P ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) x. ( 1 - ( F ` R ) ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) ) )
193 138 181 192 3eqtr3d 
 |-  ( ( ( ( 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 ` Q ) ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) ) )
194 193 oveq1d 
 |-  ( ( ( ( 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 ` Q ) ) x. ( Z ` i ) ) = ( ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) ) x. ( Z ` i ) ) )
195 126 127 mulcld 
 |-  ( ( ( ( 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 ) ) e. CC )
196 130 124 mulcld 
 |-  ( ( ( ( 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. ( F ` R ) ) e. CC )
197 195 196 134 137 divdird 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) / ( ( F ` R ) - ( F ` P ) ) ) = ( ( ( ( ( F ` R ) - ( F ` Q ) ) x. ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) x. ( F ` R ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) )
198 154 161 oveq12d 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) = ( ( ( ( F ` P ) x. ( F ` R ) ) - ( ( F ` Q ) x. ( F ` P ) ) ) + ( ( ( F ` Q ) x. ( F ` R ) ) - ( ( F ` P ) x. ( F ` R ) ) ) ) )
199 173 198 142 3eqtr4rd 
 |-  ( ( ( ( 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 ` R ) - ( F ` Q ) ) x. ( F ` P ) ) + ( ( ( F ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) )
200 195 196 addcld 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) e. CC )
201 200 134 125 137 divmuld 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) / ( ( F ` R ) - ( F ` P ) ) ) = ( F ` Q ) <-> ( ( ( F ` R ) - ( F ` P ) ) x. ( F ` Q ) ) = ( ( ( ( F ` R ) - ( F ` Q ) ) x. ( F ` P ) ) + ( ( ( F ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) ) )
202 199 201 mpbird 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) x. ( F ` R ) ) ) / ( ( F ` R ) - ( F ` P ) ) ) = ( F ` Q ) )
203 126 127 134 137 div23d 
 |-  ( ( ( ( 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 ) - ( F ` P ) ) ) = ( ( ( ( F ` R ) - ( F ` Q ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` P ) ) )
204 188 oveq1d 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` P ) ) = ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) )
205 203 204 eqtrd 
 |-  ( ( ( ( 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 ) - ( F ` P ) ) ) = ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) )
206 130 124 134 137 div23d 
 |-  ( ( ( ( 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. ( F ` R ) ) / ( ( F ` R ) - ( F ` P ) ) ) = ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) )
207 205 206 oveq12d 
 |-  ( ( ( ( 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 ) - ( F ` P ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) x. ( F ` R ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) ) )
208 197 202 207 3eqtr3d 
 |-  ( ( ( ( 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 ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) ) )
209 208 oveq1d 
 |-  ( ( ( ( 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. ( U ` i ) ) = ( ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) ) x. ( U ` i ) ) )
210 194 209 oveq12d 
 |-  ( ( ( ( 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 ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) = ( ( ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) ) x. ( Z ` i ) ) + ( ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) ) x. ( U ` i ) ) ) )
211 130 134 137 divcld 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) e. CC )
212 subcl 
 |-  ( ( 1 e. CC /\ ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) e. CC ) -> ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) e. CC )
213 44 211 212 sylancr 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) e. CC )
214 simp3l 
 |-  ( ( ( ( F ` P ) e. CC /\ ( F ` P ) =/= ( F ` R ) ) /\ ( ( F ` Q ) e. CC /\ ( F ` R ) e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( Z ` i ) e. CC )
215 128 214 mulcld 
 |-  ( ( ( ( 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 ) ) x. ( Z ` i ) ) e. CC )
216 213 215 mulcld 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) e. CC )
217 132 214 mulcld 
 |-  ( ( ( ( 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 ) ) x. ( Z ` i ) ) e. CC )
218 211 217 mulcld 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) ) e. CC )
219 simp3r 
 |-  ( ( ( ( F ` P ) e. CC /\ ( F ` P ) =/= ( F ` R ) ) /\ ( ( F ` Q ) e. CC /\ ( F ` R ) e. CC ) /\ ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) ) -> ( U ` i ) e. CC )
220 127 219 mulcld 
 |-  ( ( ( ( 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 ) x. ( U ` i ) ) e. CC )
221 213 220 mulcld 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( F ` P ) x. ( U ` i ) ) ) e. CC )
222 124 219 mulcld 
 |-  ( ( ( ( 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. ( U ` i ) ) e. CC )
223 211 222 mulcld 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( F ` R ) x. ( U ` i ) ) ) e. CC )
224 216 218 221 223 add4d 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) ) ) + ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( F ` P ) x. ( U ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( F ` R ) x. ( U ` i ) ) ) ) ) = ( ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) + ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( F ` R ) x. ( U ` i ) ) ) ) ) )
225 213 128 mulcld 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) e. CC )
226 211 132 mulcld 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) e. CC )
227 213 128 214 mulassd 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) x. ( Z ` i ) ) = ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) )
228 211 132 214 mulassd 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) x. ( Z ` i ) ) = ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) ) )
229 227 228 oveq12d 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) x. ( Z ` i ) ) + ( ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) x. ( Z ` i ) ) ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) ) ) )
230 225 214 226 229 joinlmuladdmuld 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) ) ) )
231 213 127 mulcld 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) e. CC )
232 211 124 mulcld 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) e. CC )
233 213 127 219 mulassd 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) x. ( U ` i ) ) = ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( F ` P ) x. ( U ` i ) ) ) )
234 211 124 219 mulassd 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) x. ( U ` i ) ) = ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( F ` R ) x. ( U ` i ) ) ) )
235 233 234 oveq12d 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) x. ( U ` i ) ) + ( ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) x. ( U ` i ) ) ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( F ` P ) x. ( U ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( F ` R ) x. ( U ` i ) ) ) ) )
236 231 219 232 235 joinlmuladdmuld 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) ) x. ( U ` i ) ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( F ` P ) x. ( U ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( F ` R ) x. ( U ` i ) ) ) ) )
237 230 236 oveq12d 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) ) x. ( Z ` i ) ) + ( ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) ) x. ( U ` i ) ) ) = ( ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) ) ) + ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( F ` P ) x. ( U ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( F ` R ) x. ( U ` i ) ) ) ) ) )
238 213 215 220 adddid 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) + ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( F ` P ) x. ( U ` i ) ) ) ) )
239 211 217 222 adddid 
 |-  ( ( ( ( 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 ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) = ( ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( F ` R ) x. ( U ` i ) ) ) ) )
240 238 239 oveq12d 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) ) = ( ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) + ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( F ` R ) x. ( U ` i ) ) ) ) ) )
241 224 237 240 3eqtr4rd 
 |-  ( ( ( ( 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 ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) ) = ( ( ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( 1 - ( F ` P ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( 1 - ( F ` R ) ) ) ) x. ( Z ` i ) ) + ( ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( F ` P ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( F ` R ) ) ) x. ( U ` i ) ) ) )
242 210 241 eqtr4d 
 |-  ( ( ( ( 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 ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) ) )
243 112 113 116 119 121 123 242 syl222anc 
 |-  ( ( ( ( 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 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) ) )
244 243 ralrimiva 
 |-  ( ( ( 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 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) ) )
245 oveq2 
 |-  ( t = ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) -> ( 1 - t ) = ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) )
246 245 oveq1d 
 |-  ( t = ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) -> ( ( 1 - t ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) = ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) )
247 oveq1 
 |-  ( t = ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) -> ( t x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) = ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) )
248 246 247 oveq12d 
 |-  ( t = ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) -> ( ( ( 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 ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) ) )
249 248 eqeq2d 
 |-  ( t = ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) -> ( ( ( ( 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 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) ) ) )
250 249 ralbidv 
 |-  ( t = ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) -> ( 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 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) ) ) )
251 250 rspcev 
 |-  ( ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) = ( ( ( 1 - ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) + ( ( ( ( F ` Q ) - ( F ` P ) ) / ( ( F ` R ) - ( F ` P ) ) ) 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 ) ) ) ) ) )
252 109 244 251 syl2anc 
 |-  ( ( ( 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 ) ) ) ) ) )
253 252 ex 
 |-  ( ( 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 ) ) ) ) ) ) )
254 84 253 pm2.61ine 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
255 r19.26-3 
 |-  ( A. i e. ( 1 ... N ) ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) /\ ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) /\ ( R ` i ) = ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) <-> ( 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 ) ) ) ) )
256 simp2 
 |-  ( ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) /\ ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) /\ ( R ` i ) = ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) -> ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) )
257 oveq2 
 |-  ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) -> ( ( 1 - t ) x. ( P ` i ) ) = ( ( 1 - t ) x. ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) )
258 oveq2 
 |-  ( ( R ` i ) = ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) -> ( t x. ( R ` i ) ) = ( t x. ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) )
259 257 258 oveqan12d 
 |-  ( ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) /\ ( R ` i ) = ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) -> ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` 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 ) ) ) ) ) )
260 259 3adant2 
 |-  ( ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) /\ ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) /\ ( R ` i ) = ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) -> ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` 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 ) ) ) ) ) )
261 256 260 eqeq12d 
 |-  ( ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) /\ ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) /\ ( R ` i ) = ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) -> ( ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) <-> ( ( ( 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 ) ) ) ) ) ) )
262 261 ralimi 
 |-  ( A. i e. ( 1 ... N ) ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) /\ ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) /\ ( R ` i ) = ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) <-> ( ( ( 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 ) ) ) ) ) ) )
263 ralbi 
 |-  ( A. i e. ( 1 ... N ) ( ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) <-> ( ( ( 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 ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) <-> 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 ) ) ) ) ) ) )
264 262 263 syl 
 |-  ( A. i e. ( 1 ... N ) ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) /\ ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) /\ ( R ` i ) = ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) -> ( A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) <-> 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 ) ) ) ) ) ) )
265 264 rexbidv 
 |-  ( A. i e. ( 1 ... N ) ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) /\ ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) /\ ( R ` i ) = ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` 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 ) ) ) ) ) ) )
266 265 biimprcd 
 |-  ( 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 ) ) ) ) ) -> ( A. i e. ( 1 ... N ) ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) /\ ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) /\ ( R ` i ) = ( ( ( 1 - ( F ` R ) ) x. ( Z ` i ) ) + ( ( F ` R ) x. ( U ` i ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
267 255 266 biimtrrid 
 |-  ( 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 ) ) ) ) ) -> ( ( 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 ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
268 254 267 syl 
 |-  ( ( ( ( ( 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 ) ( 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 ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
269 268 an32s 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( F ` P ) <_ ( F ` Q ) /\ ( F ` Q ) <_ ( F ` R ) ) ) /\ ( ( 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 ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
270 269 expimpd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( F ` P ) <_ ( F ` Q ) /\ ( F ` Q ) <_ ( F ` R ) ) ) -> ( ( ( ( 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 ) ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
271 270 adantlr 
 |-  ( ( ( ( ( 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 ) /\ ( 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 ) ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
272 12 271 biimtrid 
 |-  ( ( ( ( ( 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 ) ) ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
273 11 272 mpd 
 |-  ( ( ( ( ( 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 ) ) ) -> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) )
274 simpl1 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> N e. NN )
275 1 ssrab3 
 |-  D C_ ( EE ` N )
276 275 sseli 
 |-  ( Q e. D -> Q e. ( EE ` N ) )
277 275 sseli 
 |-  ( P e. D -> P e. ( EE ` N ) )
278 275 sseli 
 |-  ( R e. D -> R e. ( EE ` N ) )
279 276 277 278 3anim123i 
 |-  ( ( Q e. D /\ P e. D /\ R e. D ) -> ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) /\ R e. ( EE ` N ) ) )
280 279 3com12 
 |-  ( ( P e. D /\ Q e. D /\ R e. D ) -> ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) /\ R e. ( EE ` N ) ) )
281 brbtwn 
 |-  ( ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) /\ R e. ( EE ` N ) ) -> ( Q Btwn <. P , R >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
282 281 adantl 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( Q Btwn <. P , R >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
283 274 280 282 syl2an 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( P e. D /\ Q e. D /\ R e. D ) ) -> ( Q Btwn <. P , R >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
284 283 adantr 
 |-  ( ( ( ( ( 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 >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( Q ` i ) = ( ( ( 1 - t ) x. ( P ` i ) ) + ( t x. ( R ` i ) ) ) ) )
285 273 284 mpbird 
 |-  ( ( ( ( ( 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 >. )
286 285 ex 
 |-  ( ( ( ( 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 >. ) )