Metamath Proof Explorer

Theorem axcontlem7

Description: Lemma for axcont . Given two points in D , one preceeds the other iff its scaling constant is less than the other point's. (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypotheses axcontlem7.1 
|- D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
axcontlem7.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 axcontlem7 
|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( P e. D /\ Q e. D ) ) -> ( P Btwn <. Z , Q >. <-> ( F ` P ) <_ ( F ` Q ) ) )

Proof

Step Hyp Ref Expression
1 axcontlem7.1 
 |-  D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
2 axcontlem7.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 ssrab3 
 |-  D C_ ( EE ` N )
4 3 sseli 
 |-  ( P e. D -> P e. ( EE ` N ) )
5 4 ad2antrl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( P e. D /\ Q e. D ) ) -> P e. ( EE ` N ) )
6 simpll2 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( P e. D /\ Q e. D ) ) -> Z e. ( EE ` N ) )
7 3 sseli 
 |-  ( Q e. D -> Q e. ( EE ` N ) )
8 7 ad2antll 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( P e. D /\ Q e. D ) ) -> Q e. ( EE ` N ) )
9 brbtwn 
 |-  ( ( P e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ Q e. ( EE ` N ) ) -> ( P Btwn <. Z , Q >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) ) )
10 5 6 8 9 syl3anc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( P e. D /\ Q e. D ) ) -> ( P Btwn <. Z , Q >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) ) )
11 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 ) ) ) ) )
12 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 ) ) ) ) )
13 11 12 anim12dan 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( P e. D /\ Q 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 ) ) ) ) ) )
14 an4 
 |-  ( ( ( ( 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 ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) 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 ) ) ) ) ) )
15 r19.26 
 |-  ( 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 ) ) ) ) <-> ( 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 ) ) ) ) )
16 15 anbi2i 
 |-  ( ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ 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 ) ) ) ) ) <-> ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) 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 ) ) ) ) ) )
17 14 16 bitr4i 
 |-  ( ( ( ( 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 ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ 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 ) ) ) ) ) )
18 id 
 |-  ( ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) -> ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) )
19 oveq2 
 |-  ( ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) -> ( t x. ( Q ` i ) ) = ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) )
20 19 oveq2d 
 |-  ( ( Q ` i ) = ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) )
21 18 20 eqeqan12d 
 |-  ( ( ( 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 ) ) ) ) -> ( ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) <-> ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) ) )
22 21 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 ) ) ) ) -> A. i e. ( 1 ... N ) ( ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) <-> ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) ) )
23 ralbi 
 |-  ( A. i e. ( 1 ... N ) ( ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) <-> ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) ) -> ( A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) ) )
24 22 23 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 ) ) ) ) -> ( A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) ) )
25 24 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 ) ) ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) ) )
26 simpll2 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> Z e. ( EE ` N ) )
27 fveecn 
 |-  ( ( Z e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
28 26 27 sylan 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
29 simpll3 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> U e. ( EE ` N ) )
30 fveecn 
 |-  ( ( U e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) e. CC )
31 29 30 sylan 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( U ` i ) e. CC )
32 elicc01 
 |-  ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
33 32 simp1bi 
 |-  ( t e. ( 0 [,] 1 ) -> t e. RR )
34 33 recnd 
 |-  ( t e. ( 0 [,] 1 ) -> t e. CC )
35 34 ad2antll 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> t e. CC )
36 35 adantr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> t e. CC )
37 elrege0 
 |-  ( ( F ` P ) e. ( 0 [,) +oo ) <-> ( ( F ` P ) e. RR /\ 0 <_ ( F ` P ) ) )
38 37 simplbi 
 |-  ( ( F ` P ) e. ( 0 [,) +oo ) -> ( F ` P ) e. RR )
39 38 recnd 
 |-  ( ( F ` P ) e. ( 0 [,) +oo ) -> ( F ` P ) e. CC )
40 39 adantr 
 |-  ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( F ` P ) e. CC )
41 40 ad2antrl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( F ` P ) e. CC )
42 41 adantr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( F ` P ) e. CC )
43 elrege0 
 |-  ( ( F ` Q ) e. ( 0 [,) +oo ) <-> ( ( F ` Q ) e. RR /\ 0 <_ ( F ` Q ) ) )
44 43 simplbi 
 |-  ( ( F ` Q ) e. ( 0 [,) +oo ) -> ( F ` Q ) e. RR )
45 44 recnd 
 |-  ( ( F ` Q ) e. ( 0 [,) +oo ) -> ( F ` Q ) e. CC )
46 45 adantl 
 |-  ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( F ` Q ) e. CC )
47 46 ad2antrl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( F ` Q ) e. CC )
48 47 adantr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( F ` Q ) e. CC )
49 ax-1cn 
 |-  1 e. CC
50 simpr1 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> t e. CC )
51 simpr3 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( F ` Q ) e. CC )
52 50 51 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( t x. ( F ` Q ) ) e. CC )
53 subcl 
 |-  ( ( 1 e. CC /\ ( t x. ( F ` Q ) ) e. CC ) -> ( 1 - ( t x. ( F ` Q ) ) ) e. CC )
54 49 52 53 sylancr 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( 1 - ( t x. ( F ` Q ) ) ) e. CC )
55 subcl 
 |-  ( ( 1 e. CC /\ ( F ` P ) e. CC ) -> ( 1 - ( F ` P ) ) e. CC )
56 49 55 mpan 
 |-  ( ( F ` P ) e. CC -> ( 1 - ( F ` P ) ) e. CC )
57 56 3ad2ant2 
 |-  ( ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) -> ( 1 - ( F ` P ) ) e. CC )
58 57 adantl 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( 1 - ( F ` P ) ) e. CC )
59 simpll 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( Z ` i ) e. CC )
60 54 58 59 subdird 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( 1 - ( t x. ( F ` Q ) ) ) - ( 1 - ( F ` P ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) - ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) )
61 simpr2 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( F ` P ) e. CC )
62 nnncan1 
 |-  ( ( 1 e. CC /\ ( t x. ( F ` Q ) ) e. CC /\ ( F ` P ) e. CC ) -> ( ( 1 - ( t x. ( F ` Q ) ) ) - ( 1 - ( F ` P ) ) ) = ( ( F ` P ) - ( t x. ( F ` Q ) ) ) )
63 49 52 61 62 mp3an2i 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( 1 - ( t x. ( F ` Q ) ) ) - ( 1 - ( F ` P ) ) ) = ( ( F ` P ) - ( t x. ( F ` Q ) ) ) )
64 63 oveq1d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( 1 - ( t x. ( F ` Q ) ) ) - ( 1 - ( F ` P ) ) ) x. ( Z ` i ) ) = ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) )
65 subdi 
 |-  ( ( t e. CC /\ 1 e. CC /\ ( F ` Q ) e. CC ) -> ( t x. ( 1 - ( F ` Q ) ) ) = ( ( t x. 1 ) - ( t x. ( F ` Q ) ) ) )
66 49 65 mp3an2 
 |-  ( ( t e. CC /\ ( F ` Q ) e. CC ) -> ( t x. ( 1 - ( F ` Q ) ) ) = ( ( t x. 1 ) - ( t x. ( F ` Q ) ) ) )
67 mulrid 
 |-  ( t e. CC -> ( t x. 1 ) = t )
68 67 adantr 
 |-  ( ( t e. CC /\ ( F ` Q ) e. CC ) -> ( t x. 1 ) = t )
69 68 oveq1d 
 |-  ( ( t e. CC /\ ( F ` Q ) e. CC ) -> ( ( t x. 1 ) - ( t x. ( F ` Q ) ) ) = ( t - ( t x. ( F ` Q ) ) ) )
70 66 69 eqtrd 
 |-  ( ( t e. CC /\ ( F ` Q ) e. CC ) -> ( t x. ( 1 - ( F ` Q ) ) ) = ( t - ( t x. ( F ` Q ) ) ) )
71 50 51 70 syl2anc 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( t x. ( 1 - ( F ` Q ) ) ) = ( t - ( t x. ( F ` Q ) ) ) )
72 71 oveq2d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( 1 - t ) + ( t x. ( 1 - ( F ` Q ) ) ) ) = ( ( 1 - t ) + ( t - ( t x. ( F ` Q ) ) ) ) )
73 npncan 
 |-  ( ( 1 e. CC /\ t e. CC /\ ( t x. ( F ` Q ) ) e. CC ) -> ( ( 1 - t ) + ( t - ( t x. ( F ` Q ) ) ) ) = ( 1 - ( t x. ( F ` Q ) ) ) )
74 49 50 52 73 mp3an2i 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( 1 - t ) + ( t - ( t x. ( F ` Q ) ) ) ) = ( 1 - ( t x. ( F ` Q ) ) ) )
75 72 74 eqtr2d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( 1 - ( t x. ( F ` Q ) ) ) = ( ( 1 - t ) + ( t x. ( 1 - ( F ` Q ) ) ) ) )
76 75 oveq1d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( 1 - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - t ) + ( t x. ( 1 - ( F ` Q ) ) ) ) x. ( Z ` i ) ) )
77 subcl 
 |-  ( ( 1 e. CC /\ t e. CC ) -> ( 1 - t ) e. CC )
78 49 77 mpan 
 |-  ( t e. CC -> ( 1 - t ) e. CC )
79 78 3ad2ant1 
 |-  ( ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) -> ( 1 - t ) e. CC )
80 79 adantl 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( 1 - t ) e. CC )
81 subcl 
 |-  ( ( 1 e. CC /\ ( F ` Q ) e. CC ) -> ( 1 - ( F ` Q ) ) e. CC )
82 49 81 mpan 
 |-  ( ( F ` Q ) e. CC -> ( 1 - ( F ` Q ) ) e. CC )
83 82 3ad2ant3 
 |-  ( ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) -> ( 1 - ( F ` Q ) ) e. CC )
84 83 adantl 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( 1 - ( F ` Q ) ) e. CC )
85 50 84 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( t x. ( 1 - ( F ` Q ) ) ) e. CC )
86 80 85 59 adddird 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( 1 - t ) + ( t x. ( 1 - ( F ` Q ) ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( ( t x. ( 1 - ( F ` Q ) ) ) x. ( Z ` i ) ) ) )
87 50 84 59 mulassd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( t x. ( 1 - ( F ` Q ) ) ) x. ( Z ` i ) ) = ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) )
88 87 oveq2d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( ( t x. ( 1 - ( F ` Q ) ) ) x. ( Z ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) )
89 76 86 88 3eqtrd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( 1 - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) )
90 89 oveq1d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( 1 - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) - ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) = ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) - ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) )
91 60 64 90 3eqtr3d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) = ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) - ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) )
92 simplr 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( U ` i ) e. CC )
93 61 52 92 subdird 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( U ` i ) ) = ( ( ( F ` P ) x. ( U ` i ) ) - ( ( t x. ( F ` Q ) ) x. ( U ` i ) ) ) )
94 50 51 92 mulassd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( t x. ( F ` Q ) ) x. ( U ` i ) ) = ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) )
95 94 oveq2d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( F ` P ) x. ( U ` i ) ) - ( ( t x. ( F ` Q ) ) x. ( U ` i ) ) ) = ( ( ( F ` P ) x. ( U ` i ) ) - ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) )
96 93 95 eqtrd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( U ` i ) ) = ( ( ( F ` P ) x. ( U ` i ) ) - ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) )
97 91 96 eqeq12d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) = ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( U ` i ) ) <-> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) - ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) = ( ( ( F ` P ) x. ( U ` i ) ) - ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) ) )
98 58 59 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) e. CC )
99 61 92 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( F ` P ) x. ( U ` i ) ) e. CC )
100 80 59 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( 1 - t ) x. ( Z ` i ) ) e. CC )
101 84 59 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) e. CC )
102 50 101 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) e. CC )
103 100 102 addcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) e. CC )
104 51 92 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( F ` Q ) x. ( U ` i ) ) e. CC )
105 50 104 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) e. CC )
106 98 99 103 105 addsubeq4d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) + ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) <-> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) - ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) ) = ( ( ( F ` P ) x. ( U ` i ) ) - ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) ) )
107 100 102 105 addassd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) + ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) + ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) ) )
108 50 101 104 adddid 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) = ( ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) + ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) )
109 108 oveq2d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) + ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) ) )
110 107 109 eqtr4d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) + ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) )
111 110 eqeq2d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) ) ) + ( t x. ( ( F ` Q ) x. ( U ` i ) ) ) ) <-> ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) ) )
112 97 106 111 3bitr2rd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) /\ ( t e. CC /\ ( F ` P ) e. CC /\ ( F ` Q ) e. CC ) ) -> ( ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) <-> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) = ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( U ` i ) ) ) )
113 28 31 36 42 48 112 syl23anc 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) <-> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) = ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( U ` i ) ) ) )
114 113 ralbidva 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) = ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( U ` i ) ) ) )
115 36 48 mulcld 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( t x. ( F ` Q ) ) e. CC )
116 42 115 subcld 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( F ` P ) - ( t x. ( F ` Q ) ) ) e. CC )
117 mulcan1g 
 |-  ( ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) e. CC /\ ( Z ` i ) e. CC /\ ( U ` i ) e. CC ) -> ( ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) = ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( U ` i ) ) <-> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
118 116 28 31 117 syl3anc 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) = ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( U ` i ) ) <-> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
119 118 ralbidva 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( A. i e. ( 1 ... N ) ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( Z ` i ) ) = ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) x. ( U ` i ) ) <-> A. i e. ( 1 ... N ) ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ ( Z ` i ) = ( U ` i ) ) ) )
120 r19.32v 
 |-  ( A. i e. ( 1 ... N ) ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ ( Z ` i ) = ( U ` i ) ) <-> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
121 simplr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> Z =/= U )
122 121 neneqd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> -. Z = U )
123 biorf 
 |-  ( -. Z = U -> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 <-> ( Z = U \/ ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 ) ) )
124 orcom 
 |-  ( ( Z = U \/ ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 ) <-> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ Z = U ) )
125 123 124 bitrdi 
 |-  ( -. Z = U -> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 <-> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ Z = U ) ) )
126 122 125 syl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 <-> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ Z = U ) ) )
127 35 47 mulcld 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( t x. ( F ` Q ) ) e. CC )
128 41 127 subeq0ad 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 <-> ( F ` P ) = ( t x. ( F ` Q ) ) ) )
129 eqeefv 
 |-  ( ( Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
130 129 3adant1 
 |-  ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
131 130 adantr 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
132 131 adantr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
133 132 orbi2d 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ Z = U ) <-> ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) ) )
134 126 128 133 3bitr3rd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) <-> ( F ` P ) = ( t x. ( F ` Q ) ) ) )
135 120 134 bitrid 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( A. i e. ( 1 ... N ) ( ( ( F ` P ) - ( t x. ( F ` Q ) ) ) = 0 \/ ( Z ` i ) = ( U ` i ) ) <-> ( F ` P ) = ( t x. ( F ` Q ) ) ) )
136 114 119 135 3bitrd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) <-> ( F ` P ) = ( t x. ( F ` Q ) ) ) )
137 136 anassrs 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) ) /\ t e. ( 0 [,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) <-> ( F ` P ) = ( t x. ( F ` Q ) ) ) )
138 137 rexbidva 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) <-> E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) ) )
139 33 adantl 
 |-  ( ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) -> t e. RR )
140 1red 
 |-  ( ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) -> 1 e. RR )
141 43 biimpi 
 |-  ( ( F ` Q ) e. ( 0 [,) +oo ) -> ( ( F ` Q ) e. RR /\ 0 <_ ( F ` Q ) ) )
142 141 ad2antlr 
 |-  ( ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( F ` Q ) e. RR /\ 0 <_ ( F ` Q ) ) )
143 32 simp3bi 
 |-  ( t e. ( 0 [,] 1 ) -> t <_ 1 )
144 143 adantl 
 |-  ( ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) -> t <_ 1 )
145 lemul1a 
 |-  ( ( ( t e. RR /\ 1 e. RR /\ ( ( F ` Q ) e. RR /\ 0 <_ ( F ` Q ) ) ) /\ t <_ 1 ) -> ( t x. ( F ` Q ) ) <_ ( 1 x. ( F ` Q ) ) )
146 139 140 142 144 145 syl31anc 
 |-  ( ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) -> ( t x. ( F ` Q ) ) <_ ( 1 x. ( F ` Q ) ) )
147 45 ad2antlr 
 |-  ( ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) -> ( F ` Q ) e. CC )
148 147 mullidd 
 |-  ( ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) -> ( 1 x. ( F ` Q ) ) = ( F ` Q ) )
149 146 148 breqtrd 
 |-  ( ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) -> ( t x. ( F ` Q ) ) <_ ( F ` Q ) )
150 breq1 
 |-  ( ( F ` P ) = ( t x. ( F ` Q ) ) -> ( ( F ` P ) <_ ( F ` Q ) <-> ( t x. ( F ` Q ) ) <_ ( F ` Q ) ) )
151 149 150 syl5ibrcom 
 |-  ( ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( F ` P ) = ( t x. ( F ` Q ) ) -> ( F ` P ) <_ ( F ` Q ) ) )
152 151 rexlimdva 
 |-  ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) -> ( F ` P ) <_ ( F ` Q ) ) )
153 0elunit 
 |-  0 e. ( 0 [,] 1 )
154 simpl 
 |-  ( ( ( F ` P ) = 0 /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( F ` P ) = 0 )
155 45 mul02d 
 |-  ( ( F ` Q ) e. ( 0 [,) +oo ) -> ( 0 x. ( F ` Q ) ) = 0 )
156 155 adantl 
 |-  ( ( ( F ` P ) = 0 /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( 0 x. ( F ` Q ) ) = 0 )
157 154 156 eqtr4d 
 |-  ( ( ( F ` P ) = 0 /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( F ` P ) = ( 0 x. ( F ` Q ) ) )
158 oveq1 
 |-  ( t = 0 -> ( t x. ( F ` Q ) ) = ( 0 x. ( F ` Q ) ) )
159 158 rspceeqv 
 |-  ( ( 0 e. ( 0 [,] 1 ) /\ ( F ` P ) = ( 0 x. ( F ` Q ) ) ) -> E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) )
160 153 157 159 sylancr 
 |-  ( ( ( F ` P ) = 0 /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) )
161 160 adantrl 
 |-  ( ( ( F ` P ) = 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) ) -> E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) )
162 161 a1d 
 |-  ( ( ( F ` P ) = 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) ) -> ( ( F ` P ) <_ ( F ` Q ) -> E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) ) )
163 162 ex 
 |-  ( ( F ` P ) = 0 -> ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( ( F ` P ) <_ ( F ` Q ) -> E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) ) ) )
164 simp3 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( F ` P ) <_ ( F ` Q ) )
165 38 adantr 
 |-  ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( F ` P ) e. RR )
166 165 3ad2ant2 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( F ` P ) e. RR )
167 37 simprbi 
 |-  ( ( F ` P ) e. ( 0 [,) +oo ) -> 0 <_ ( F ` P ) )
168 167 adantr 
 |-  ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> 0 <_ ( F ` P ) )
169 168 3ad2ant2 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> 0 <_ ( F ` P ) )
170 44 adantl 
 |-  ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( F ` Q ) e. RR )
171 170 3ad2ant2 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( F ` Q ) e. RR )
172 0red 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> 0 e. RR )
173 simp1 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( F ` P ) =/= 0 )
174 166 169 173 ne0gt0d 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> 0 < ( F ` P ) )
175 172 166 171 174 164 ltletrd 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> 0 < ( F ` Q ) )
176 divelunit 
 |-  ( ( ( ( F ` P ) e. RR /\ 0 <_ ( F ` P ) ) /\ ( ( F ` Q ) e. RR /\ 0 < ( F ` Q ) ) ) -> ( ( ( F ` P ) / ( F ` Q ) ) e. ( 0 [,] 1 ) <-> ( F ` P ) <_ ( F ` Q ) ) )
177 166 169 171 175 176 syl22anc 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( ( ( F ` P ) / ( F ` Q ) ) e. ( 0 [,] 1 ) <-> ( F ` P ) <_ ( F ` Q ) ) )
178 164 177 mpbird 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( ( F ` P ) / ( F ` Q ) ) e. ( 0 [,] 1 ) )
179 40 3ad2ant2 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( F ` P ) e. CC )
180 46 3ad2ant2 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( F ` Q ) e. CC )
181 175 gt0ne0d 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( F ` Q ) =/= 0 )
182 179 180 181 divcan1d 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( ( ( F ` P ) / ( F ` Q ) ) x. ( F ` Q ) ) = ( F ` P ) )
183 182 eqcomd 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> ( F ` P ) = ( ( ( F ` P ) / ( F ` Q ) ) x. ( F ` Q ) ) )
184 oveq1 
 |-  ( t = ( ( F ` P ) / ( F ` Q ) ) -> ( t x. ( F ` Q ) ) = ( ( ( F ` P ) / ( F ` Q ) ) x. ( F ` Q ) ) )
185 184 rspceeqv 
 |-  ( ( ( ( F ` P ) / ( F ` Q ) ) e. ( 0 [,] 1 ) /\ ( F ` P ) = ( ( ( F ` P ) / ( F ` Q ) ) x. ( F ` Q ) ) ) -> E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) )
186 178 183 185 syl2anc 
 |-  ( ( ( F ` P ) =/= 0 /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ ( F ` P ) <_ ( F ` Q ) ) -> E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) )
187 186 3exp 
 |-  ( ( F ` P ) =/= 0 -> ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( ( F ` P ) <_ ( F ` Q ) -> E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) ) ) )
188 163 187 pm2.61ine 
 |-  ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( ( F ` P ) <_ ( F ` Q ) -> E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) ) )
189 152 188 impbid 
 |-  ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) -> ( E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) <-> ( F ` P ) <_ ( F ` Q ) ) )
190 189 adantl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) ) -> ( E. t e. ( 0 [,] 1 ) ( F ` P ) = ( t x. ( F ` Q ) ) <-> ( F ` P ) <_ ( F ` Q ) ) )
191 138 190 bitrd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( ( ( 1 - ( F ` Q ) ) x. ( Z ` i ) ) + ( ( F ` Q ) x. ( U ` i ) ) ) ) ) <-> ( F ` P ) <_ ( F ` Q ) ) )
192 25 191 sylan9bbr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) ) /\ 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 ) ) ) ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) <-> ( F ` P ) <_ ( F ` Q ) ) )
193 192 anasss 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ ( F ` Q ) e. ( 0 [,) +oo ) ) /\ 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 ) ) ) ) ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) <-> ( F ` P ) <_ ( F ` Q ) ) )
194 17 193 sylan2b 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( ( ( 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 ) ) ) ) ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) <-> ( F ` P ) <_ ( F ` Q ) ) )
195 13 194 syldan 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( P e. D /\ Q e. D ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( Q ` i ) ) ) <-> ( F ` P ) <_ ( F ` Q ) ) )
196 10 195 bitrd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( P e. D /\ Q e. D ) ) -> ( P Btwn <. Z , Q >. <-> ( F ` P ) <_ ( F ` Q ) ) )