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 mulid1
 |-  ( 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 syl5bb
 |-  ( ( ( ( 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 mulid2d
 |-  ( ( ( ( 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 ) ) )