Metamath Proof Explorer

Theorem axcontlem4

Description: Lemma for axcont . Given the separation assumption, A is a subset of D . (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypothesis axcontlem4.1 
|- D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
Assertion axcontlem4 
|- ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> A C_ D )

Proof

Step Hyp Ref Expression
1 axcontlem4.1 
 |-  D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
2 simplr1 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> A C_ ( EE ` N ) )
3 n0 
 |-  ( B =/= (/) <-> E. b b e. B )
4 idd 
 |-  ( b e. B -> ( A C_ ( EE ` N ) -> A C_ ( EE ` N ) ) )
5 ssel 
 |-  ( B C_ ( EE ` N ) -> ( b e. B -> b e. ( EE ` N ) ) )
6 5 com12 
 |-  ( b e. B -> ( B C_ ( EE ` N ) -> b e. ( EE ` N ) ) )
7 opeq2 
 |-  ( y = b -> <. Z , y >. = <. Z , b >. )
8 7 breq2d 
 |-  ( y = b -> ( x Btwn <. Z , y >. <-> x Btwn <. Z , b >. ) )
9 8 rspcv 
 |-  ( b e. B -> ( A. y e. B x Btwn <. Z , y >. -> x Btwn <. Z , b >. ) )
10 9 ralimdv 
 |-  ( b e. B -> ( A. x e. A A. y e. B x Btwn <. Z , y >. -> A. x e. A x Btwn <. Z , b >. ) )
11 4 6 10 3anim123d 
 |-  ( b e. B -> ( ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) -> ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) )
12 11 anim2d 
 |-  ( b e. B -> ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) -> ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) ) )
13 simplr1 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> A C_ ( EE ` N ) )
14 13 adantr 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> A C_ ( EE ` N ) )
15 simplr2 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> U e. A )
16 14 15 sseldd 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> U e. ( EE ` N ) )
17 simpr3 
 |-  ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) -> A. x e. A x Btwn <. Z , b >. )
18 simp2 
 |-  ( ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) -> U e. A )
19 breq1 
 |-  ( x = U -> ( x Btwn <. Z , b >. <-> U Btwn <. Z , b >. ) )
20 19 rspccva 
 |-  ( ( A. x e. A x Btwn <. Z , b >. /\ U e. A ) -> U Btwn <. Z , b >. )
21 17 18 20 syl2an 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> U Btwn <. Z , b >. )
22 21 adantr 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> U Btwn <. Z , b >. )
23 16 22 jca 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> ( U e. ( EE ` N ) /\ U Btwn <. Z , b >. ) )
24 13 sselda 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> p e. ( EE ` N ) )
25 17 adantr 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> A. x e. A x Btwn <. Z , b >. )
26 breq1 
 |-  ( x = p -> ( x Btwn <. Z , b >. <-> p Btwn <. Z , b >. ) )
27 26 rspccva 
 |-  ( ( A. x e. A x Btwn <. Z , b >. /\ p e. A ) -> p Btwn <. Z , b >. )
28 25 27 sylan 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> p Btwn <. Z , b >. )
29 23 24 28 jca32 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> ( ( U e. ( EE ` N ) /\ U Btwn <. Z , b >. ) /\ ( p e. ( EE ` N ) /\ p Btwn <. Z , b >. ) ) )
30 an4 
 |-  ( ( ( U e. ( EE ` N ) /\ U Btwn <. Z , b >. ) /\ ( p e. ( EE ` N ) /\ p Btwn <. Z , b >. ) ) <-> ( ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) /\ ( U Btwn <. Z , b >. /\ p Btwn <. Z , b >. ) ) )
31 29 30 sylib 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> ( ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) /\ ( U Btwn <. Z , b >. /\ p Btwn <. Z , b >. ) ) )
32 simp2 
 |-  ( ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) -> b e. ( EE ` N ) )
33 simpl2r 
 |-  ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> Z =/= U )
34 33 adantr 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) -> Z =/= U )
35 simpl 
 |-  ( ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) )
36 35 ralimi 
 |-  ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) )
37 eqcom 
 |-  ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) <-> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( U ` i ) )
38 oveq2 
 |-  ( t = 0 -> ( 1 - t ) = ( 1 - 0 ) )
39 1m0e1 
 |-  ( 1 - 0 ) = 1
40 38 39 eqtrdi 
 |-  ( t = 0 -> ( 1 - t ) = 1 )
41 40 oveq1d 
 |-  ( t = 0 -> ( ( 1 - t ) x. ( Z ` i ) ) = ( 1 x. ( Z ` i ) ) )
42 oveq1 
 |-  ( t = 0 -> ( t x. ( b ` i ) ) = ( 0 x. ( b ` i ) ) )
43 41 42 oveq12d 
 |-  ( t = 0 -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) )
44 43 eqeq1d 
 |-  ( t = 0 -> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( U ` i ) <-> ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) = ( U ` i ) ) )
45 37 44 bitrid 
 |-  ( t = 0 -> ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) <-> ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) = ( U ` i ) ) )
46 45 ralbidv 
 |-  ( t = 0 -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) = ( U ` i ) ) )
47 46 biimpac 
 |-  ( ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ t = 0 ) -> A. i e. ( 1 ... N ) ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) = ( U ` i ) )
48 simpl2l 
 |-  ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> Z e. ( EE ` N ) )
49 simpl3l 
 |-  ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> U e. ( EE ` N ) )
50 eqeefv 
 |-  ( ( Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
51 48 49 50 syl2anc 
 |-  ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
52 fveecn 
 |-  ( ( Z e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
53 48 52 sylan 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
54 simp1r 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> b e. ( EE ` N ) )
55 54 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> b e. ( EE ` N ) )
56 fveecn 
 |-  ( ( b e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( b ` i ) e. CC )
57 55 56 sylancom 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( b ` i ) e. CC )
58 mullid 
 |-  ( ( Z ` i ) e. CC -> ( 1 x. ( Z ` i ) ) = ( Z ` i ) )
59 mul02 
 |-  ( ( b ` i ) e. CC -> ( 0 x. ( b ` i ) ) = 0 )
60 58 59 oveqan12d 
 |-  ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) -> ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) = ( ( Z ` i ) + 0 ) )
61 addrid 
 |-  ( ( Z ` i ) e. CC -> ( ( Z ` i ) + 0 ) = ( Z ` i ) )
62 61 adantr 
 |-  ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) -> ( ( Z ` i ) + 0 ) = ( Z ` i ) )
63 60 62 eqtrd 
 |-  ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) -> ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) = ( Z ` i ) )
64 53 57 63 syl2anc 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) = ( Z ` i ) )
65 64 eqeq1d 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) = ( U ` i ) <-> ( Z ` i ) = ( U ` i ) ) )
66 65 ralbidva 
 |-  ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( A. i e. ( 1 ... N ) ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) = ( U ` i ) <-> A. i e. ( 1 ... N ) ( Z ` i ) = ( U ` i ) ) )
67 51 66 bitr4d 
 |-  ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( Z = U <-> A. i e. ( 1 ... N ) ( ( 1 x. ( Z ` i ) ) + ( 0 x. ( b ` i ) ) ) = ( U ` i ) ) )
68 47 67 imbitrrid 
 |-  ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ t = 0 ) -> Z = U ) )
69 68 expdimp 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) -> ( t = 0 -> Z = U ) )
70 36 69 sylan2 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) -> ( t = 0 -> Z = U ) )
71 70 necon3d 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) -> ( Z =/= U -> t =/= 0 ) )
72 34 71 mpd 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) -> t =/= 0 )
73 simp1l 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> N e. NN )
74 simp2l 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> Z e. ( EE ` N ) )
75 73 74 54 3jca 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) )
76 simp2l 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> t e. ( 0 [,] 1 ) )
77 elicc01 
 |-  ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
78 77 simp1bi 
 |-  ( t e. ( 0 [,] 1 ) -> t e. RR )
79 76 78 syl 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> t e. RR )
80 simp2r 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> s e. ( 0 [,] 1 ) )
81 elicc01 
 |-  ( s e. ( 0 [,] 1 ) <-> ( s e. RR /\ 0 <_ s /\ s <_ 1 ) )
82 81 simp1bi 
 |-  ( s e. ( 0 [,] 1 ) -> s e. RR )
83 80 82 syl 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> s e. RR )
84 79 83 letrid 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> ( t <_ s \/ s <_ t ) )
85 simpr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> t <_ s )
86 79 adantr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> t e. RR )
87 77 simp2bi 
 |-  ( t e. ( 0 [,] 1 ) -> 0 <_ t )
88 76 87 syl 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> 0 <_ t )
89 88 adantr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> 0 <_ t )
90 83 adantr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> s e. RR )
91 0red 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> 0 e. RR )
92 simp3 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> t =/= 0 )
93 79 88 92 ne0gt0d 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> 0 < t )
94 93 adantr 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> 0 < t )
95 91 86 90 94 85 ltletrd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> 0 < s )
96 divelunit 
 |-  ( ( ( t e. RR /\ 0 <_ t ) /\ ( s e. RR /\ 0 < s ) ) -> ( ( t / s ) e. ( 0 [,] 1 ) <-> t <_ s ) )
97 86 89 90 95 96 syl22anc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> ( ( t / s ) e. ( 0 [,] 1 ) <-> t <_ s ) )
98 85 97 mpbird 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> ( t / s ) e. ( 0 [,] 1 ) )
99 simp12 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> Z e. ( EE ` N ) )
100 99 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
101 100 52 sylancom 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
102 simp13 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> b e. ( EE ` N ) )
103 102 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> b e. ( EE ` N ) )
104 103 56 sylancom 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> ( b ` i ) e. CC )
105 78 recnd 
 |-  ( t e. ( 0 [,] 1 ) -> t e. CC )
106 76 105 syl 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> t e. CC )
107 106 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> t e. CC )
108 82 recnd 
 |-  ( s e. ( 0 [,] 1 ) -> s e. CC )
109 80 108 syl 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> s e. CC )
110 109 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> s e. CC )
111 0red 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> 0 e. RR )
112 79 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> t e. RR )
113 83 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> s e. RR )
114 88 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> 0 <_ t )
115 simpll3 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> t =/= 0 )
116 112 114 115 ne0gt0d 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> 0 < t )
117 simplr 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> t <_ s )
118 111 112 113 116 117 ltletrd 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> 0 < s )
119 118 gt0ne0d 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> s =/= 0 )
120 divcl 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> ( t / s ) e. CC )
121 120 adantl 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( t / s ) e. CC )
122 ax-1cn 
 |-  1 e. CC
123 simpr2 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> s e. CC )
124 subcl 
 |-  ( ( 1 e. CC /\ s e. CC ) -> ( 1 - s ) e. CC )
125 122 123 124 sylancr 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( 1 - s ) e. CC )
126 simpll 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( Z ` i ) e. CC )
127 125 126 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( 1 - s ) x. ( Z ` i ) ) e. CC )
128 simplr 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( b ` i ) e. CC )
129 123 128 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( s x. ( b ` i ) ) e. CC )
130 121 127 129 adddid 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( t / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) = ( ( ( t / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) + ( ( t / s ) x. ( s x. ( b ` i ) ) ) ) )
131 130 oveq2d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( ( t / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) + ( ( t / s ) x. ( s x. ( b ` i ) ) ) ) ) )
132 subcl 
 |-  ( ( 1 e. CC /\ ( t / s ) e. CC ) -> ( 1 - ( t / s ) ) e. CC )
133 122 121 132 sylancr 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( 1 - ( t / s ) ) e. CC )
134 133 126 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) e. CC )
135 121 127 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( t / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) e. CC )
136 121 129 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( t / s ) x. ( s x. ( b ` i ) ) ) e. CC )
137 134 135 136 addassd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) + ( ( t / s ) x. ( s x. ( b ` i ) ) ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( ( t / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) + ( ( t / s ) x. ( s x. ( b ` i ) ) ) ) ) )
138 121 125 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( t / s ) x. ( 1 - s ) ) e. CC )
139 133 138 126 adddird 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( 1 - ( t / s ) ) + ( ( t / s ) x. ( 1 - s ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( ( t / s ) x. ( 1 - s ) ) x. ( Z ` i ) ) ) )
140 simp2 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> s e. CC )
141 subdi 
 |-  ( ( ( t / s ) e. CC /\ 1 e. CC /\ s e. CC ) -> ( ( t / s ) x. ( 1 - s ) ) = ( ( ( t / s ) x. 1 ) - ( ( t / s ) x. s ) ) )
142 122 141 mp3an2 
 |-  ( ( ( t / s ) e. CC /\ s e. CC ) -> ( ( t / s ) x. ( 1 - s ) ) = ( ( ( t / s ) x. 1 ) - ( ( t / s ) x. s ) ) )
143 120 140 142 syl2anc 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> ( ( t / s ) x. ( 1 - s ) ) = ( ( ( t / s ) x. 1 ) - ( ( t / s ) x. s ) ) )
144 120 mulridd 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> ( ( t / s ) x. 1 ) = ( t / s ) )
145 divcan1 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> ( ( t / s ) x. s ) = t )
146 144 145 oveq12d 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> ( ( ( t / s ) x. 1 ) - ( ( t / s ) x. s ) ) = ( ( t / s ) - t ) )
147 143 146 eqtrd 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> ( ( t / s ) x. ( 1 - s ) ) = ( ( t / s ) - t ) )
148 147 oveq2d 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> ( ( 1 - ( t / s ) ) + ( ( t / s ) x. ( 1 - s ) ) ) = ( ( 1 - ( t / s ) ) + ( ( t / s ) - t ) ) )
149 simp1 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> t e. CC )
150 npncan 
 |-  ( ( 1 e. CC /\ ( t / s ) e. CC /\ t e. CC ) -> ( ( 1 - ( t / s ) ) + ( ( t / s ) - t ) ) = ( 1 - t ) )
151 122 120 149 150 mp3an2i 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> ( ( 1 - ( t / s ) ) + ( ( t / s ) - t ) ) = ( 1 - t ) )
152 148 151 eqtrd 
 |-  ( ( t e. CC /\ s e. CC /\ s =/= 0 ) -> ( ( 1 - ( t / s ) ) + ( ( t / s ) x. ( 1 - s ) ) ) = ( 1 - t ) )
153 152 adantl 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( 1 - ( t / s ) ) + ( ( t / s ) x. ( 1 - s ) ) ) = ( 1 - t ) )
154 153 oveq1d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( 1 - ( t / s ) ) + ( ( t / s ) x. ( 1 - s ) ) ) x. ( Z ` i ) ) = ( ( 1 - t ) x. ( Z ` i ) ) )
155 121 125 126 mulassd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( t / s ) x. ( 1 - s ) ) x. ( Z ` i ) ) = ( ( t / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) )
156 155 oveq2d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( ( t / s ) x. ( 1 - s ) ) x. ( Z ` i ) ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) )
157 139 154 156 3eqtr3rd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) = ( ( 1 - t ) x. ( Z ` i ) ) )
158 121 123 128 mulassd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( t / s ) x. s ) x. ( b ` i ) ) = ( ( t / s ) x. ( s x. ( b ` i ) ) ) )
159 145 adantl 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( t / s ) x. s ) = t )
160 159 oveq1d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( t / s ) x. s ) x. ( b ` i ) ) = ( t x. ( b ` i ) ) )
161 158 160 eqtr3d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( t / s ) x. ( s x. ( b ` i ) ) ) = ( t x. ( b ` i ) ) )
162 157 161 oveq12d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( 1 - s ) x. ( Z ` i ) ) ) ) + ( ( t / s ) x. ( s x. ( b ` i ) ) ) ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) )
163 131 137 162 3eqtr2rd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( t e. CC /\ s e. CC /\ s =/= 0 ) ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) )
164 101 104 107 110 119 163 syl23anc 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) )
165 164 ralrimiva 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) )
166 oveq2 
 |-  ( r = ( t / s ) -> ( 1 - r ) = ( 1 - ( t / s ) ) )
167 166 oveq1d 
 |-  ( r = ( t / s ) -> ( ( 1 - r ) x. ( Z ` i ) ) = ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) )
168 oveq1 
 |-  ( r = ( t / s ) -> ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) = ( ( t / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) )
169 167 168 oveq12d 
 |-  ( r = ( t / s ) -> ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) )
170 169 eqeq2d 
 |-  ( r = ( t / s ) -> ( ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) <-> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) ) )
171 170 ralbidv 
 |-  ( r = ( t / s ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) ) )
172 171 rspcev 
 |-  ( ( ( t / s ) e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - ( t / s ) ) x. ( Z ` i ) ) + ( ( t / s ) x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) ) -> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) )
173 98 165 172 syl2anc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ t <_ s ) -> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) )
174 173 ex 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> ( t <_ s -> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) ) )
175 81 simp2bi 
 |-  ( s e. ( 0 [,] 1 ) -> 0 <_ s )
176 80 175 syl 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> 0 <_ s )
177 divelunit 
 |-  ( ( ( s e. RR /\ 0 <_ s ) /\ ( t e. RR /\ 0 < t ) ) -> ( ( s / t ) e. ( 0 [,] 1 ) <-> s <_ t ) )
178 83 176 79 93 177 syl22anc 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> ( ( s / t ) e. ( 0 [,] 1 ) <-> s <_ t ) )
179 178 biimpar 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t ) -> ( s / t ) e. ( 0 [,] 1 ) )
180 simp112 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> Z e. ( EE ` N ) )
181 simp3 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> i e. ( 1 ... N ) )
182 180 181 52 syl2anc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> ( Z ` i ) e. CC )
183 simp113 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> b e. ( EE ` N ) )
184 183 181 56 syl2anc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> ( b ` i ) e. CC )
185 simp12r 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> s e. ( 0 [,] 1 ) )
186 185 108 syl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> s e. CC )
187 simp12l 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> t e. ( 0 [,] 1 ) )
188 187 105 syl 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> t e. CC )
189 simp13 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> t =/= 0 )
190 divcl 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( s / t ) e. CC )
191 190 adantl 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( s / t ) e. CC )
192 simpr2 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> t e. CC )
193 subcl 
 |-  ( ( 1 e. CC /\ t e. CC ) -> ( 1 - t ) e. CC )
194 122 192 193 sylancr 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( 1 - t ) e. CC )
195 simpll 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( Z ` i ) e. CC )
196 194 195 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( 1 - t ) x. ( Z ` i ) ) e. CC )
197 simplr 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( b ` i ) e. CC )
198 192 197 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( t x. ( b ` i ) ) e. CC )
199 191 196 198 adddid 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) = ( ( ( s / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) + ( ( s / t ) x. ( t x. ( b ` i ) ) ) ) )
200 199 oveq2d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( ( s / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) + ( ( s / t ) x. ( t x. ( b ` i ) ) ) ) ) )
201 subcl 
 |-  ( ( 1 e. CC /\ ( s / t ) e. CC ) -> ( 1 - ( s / t ) ) e. CC )
202 122 191 201 sylancr 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( 1 - ( s / t ) ) e. CC )
203 202 195 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) e. CC )
204 191 196 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( s / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) e. CC )
205 191 198 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( s / t ) x. ( t x. ( b ` i ) ) ) e. CC )
206 203 204 205 addassd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) + ( ( s / t ) x. ( t x. ( b ` i ) ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( ( s / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) + ( ( s / t ) x. ( t x. ( b ` i ) ) ) ) ) )
207 simp2 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> t e. CC )
208 subdi 
 |-  ( ( ( s / t ) e. CC /\ 1 e. CC /\ t e. CC ) -> ( ( s / t ) x. ( 1 - t ) ) = ( ( ( s / t ) x. 1 ) - ( ( s / t ) x. t ) ) )
209 122 208 mp3an2 
 |-  ( ( ( s / t ) e. CC /\ t e. CC ) -> ( ( s / t ) x. ( 1 - t ) ) = ( ( ( s / t ) x. 1 ) - ( ( s / t ) x. t ) ) )
210 190 207 209 syl2anc 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( ( s / t ) x. ( 1 - t ) ) = ( ( ( s / t ) x. 1 ) - ( ( s / t ) x. t ) ) )
211 190 mulridd 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( ( s / t ) x. 1 ) = ( s / t ) )
212 divcan1 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( ( s / t ) x. t ) = s )
213 211 212 oveq12d 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( ( ( s / t ) x. 1 ) - ( ( s / t ) x. t ) ) = ( ( s / t ) - s ) )
214 210 213 eqtrd 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( ( s / t ) x. ( 1 - t ) ) = ( ( s / t ) - s ) )
215 214 oveq2d 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( ( 1 - ( s / t ) ) + ( ( s / t ) x. ( 1 - t ) ) ) = ( ( 1 - ( s / t ) ) + ( ( s / t ) - s ) ) )
216 simp1 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> s e. CC )
217 npncan 
 |-  ( ( 1 e. CC /\ ( s / t ) e. CC /\ s e. CC ) -> ( ( 1 - ( s / t ) ) + ( ( s / t ) - s ) ) = ( 1 - s ) )
218 122 190 216 217 mp3an2i 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( ( 1 - ( s / t ) ) + ( ( s / t ) - s ) ) = ( 1 - s ) )
219 215 218 eqtr2d 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( 1 - s ) = ( ( 1 - ( s / t ) ) + ( ( s / t ) x. ( 1 - t ) ) ) )
220 219 oveq1d 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( ( 1 - s ) x. ( Z ` i ) ) = ( ( ( 1 - ( s / t ) ) + ( ( s / t ) x. ( 1 - t ) ) ) x. ( Z ` i ) ) )
221 220 adantl 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( 1 - s ) x. ( Z ` i ) ) = ( ( ( 1 - ( s / t ) ) + ( ( s / t ) x. ( 1 - t ) ) ) x. ( Z ` i ) ) )
222 191 194 mulcld 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( s / t ) x. ( 1 - t ) ) e. CC )
223 202 222 195 adddird 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( ( 1 - ( s / t ) ) + ( ( s / t ) x. ( 1 - t ) ) ) x. ( Z ` i ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( ( s / t ) x. ( 1 - t ) ) x. ( Z ` i ) ) ) )
224 191 194 195 mulassd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( ( s / t ) x. ( 1 - t ) ) x. ( Z ` i ) ) = ( ( s / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) )
225 224 oveq2d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( ( s / t ) x. ( 1 - t ) ) x. ( Z ` i ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) )
226 221 223 225 3eqtrrd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) = ( ( 1 - s ) x. ( Z ` i ) ) )
227 191 192 197 mulassd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( ( s / t ) x. t ) x. ( b ` i ) ) = ( ( s / t ) x. ( t x. ( b ` i ) ) ) )
228 212 oveq1d 
 |-  ( ( s e. CC /\ t e. CC /\ t =/= 0 ) -> ( ( ( s / t ) x. t ) x. ( b ` i ) ) = ( s x. ( b ` i ) ) )
229 228 adantl 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( ( s / t ) x. t ) x. ( b ` i ) ) = ( s x. ( b ` i ) ) )
230 227 229 eqtr3d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( s / t ) x. ( t x. ( b ` i ) ) ) = ( s x. ( b ` i ) ) )
231 226 230 oveq12d 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( 1 - t ) x. ( Z ` i ) ) ) ) + ( ( s / t ) x. ( t x. ( b ` i ) ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) )
232 200 206 231 3eqtr2rd 
 |-  ( ( ( ( Z ` i ) e. CC /\ ( b ` i ) e. CC ) /\ ( s e. CC /\ t e. CC /\ t =/= 0 ) ) -> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) )
233 182 184 186 188 189 232 syl23anc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) )
234 233 3expa 
 |-  ( ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) )
235 234 ralrimiva 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t ) -> A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) )
236 oveq2 
 |-  ( r = ( s / t ) -> ( 1 - r ) = ( 1 - ( s / t ) ) )
237 236 oveq1d 
 |-  ( r = ( s / t ) -> ( ( 1 - r ) x. ( Z ` i ) ) = ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) )
238 oveq1 
 |-  ( r = ( s / t ) -> ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) = ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) )
239 237 238 oveq12d 
 |-  ( r = ( s / t ) -> ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) )
240 239 eqeq2d 
 |-  ( r = ( s / t ) -> ( ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) <-> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) )
241 240 ralbidv 
 |-  ( r = ( s / t ) -> ( A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) <-> A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) )
242 241 rspcev 
 |-  ( ( ( s / t ) e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - ( s / t ) ) x. ( Z ` i ) ) + ( ( s / t ) x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) -> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) )
243 179 235 242 syl2anc 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) /\ s <_ t ) -> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) )
244 243 ex 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> ( s <_ t -> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) )
245 174 244 orim12d 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> ( ( t <_ s \/ s <_ t ) -> ( E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) \/ E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) ) )
246 r19.43 
 |-  ( E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) \/ A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) <-> ( E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) \/ E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) )
247 245 246 imbitrrdi 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> ( ( t <_ s \/ s <_ t ) -> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) \/ A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) ) )
248 84 247 mpd 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) \/ A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) )
249 id 
 |-  ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) -> ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) )
250 oveq2 
 |-  ( ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) -> ( r x. ( p ` i ) ) = ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) )
251 250 oveq2d 
 |-  ( ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) -> ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) )
252 249 251 eqeqan12d 
 |-  ( ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> ( ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) <-> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) ) )
253 252 ralimi 
 |-  ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) <-> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) ) )
254 ralbi 
 |-  ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) <-> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) ) -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) ) )
255 253 254 syl 
 |-  ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) ) )
256 id 
 |-  ( ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) -> ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) )
257 oveq2 
 |-  ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) -> ( r x. ( U ` i ) ) = ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) )
258 257 oveq2d 
 |-  ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) -> ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) )
259 256 258 eqeqan12rd 
 |-  ( ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> ( ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) <-> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) )
260 259 ralimi 
 |-  ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) <-> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) )
261 ralbi 
 |-  ( A. i e. ( 1 ... N ) ( ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) <-> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) )
262 260 261 syl 
 |-  ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) )
263 255 262 orbi12d 
 |-  ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> ( ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) <-> ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) \/ A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) ) )
264 263 rexbidv 
 |-  ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> ( E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) <-> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) \/ A. i e. ( 1 ... N ) ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) ) ) ) )
265 248 264 syl5ibrcom 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ t =/= 0 ) -> ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) ) )
266 265 3expia 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( t =/= 0 -> ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) ) ) )
267 266 com23 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> ( t =/= 0 -> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) ) ) )
268 75 267 sylan 
 |-  ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> ( t =/= 0 -> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) ) ) )
269 268 imp 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) -> ( t =/= 0 -> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) ) )
270 72 269 mpd 
 |-  ( ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) /\ A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) -> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) )
271 270 ex 
 |-  ( ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) ) -> ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) ) )
272 271 rexlimdvva 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) -> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) ) )
273 simp3l 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> U e. ( EE ` N ) )
274 brbtwn 
 |-  ( ( U e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) -> ( U Btwn <. Z , b >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) )
275 273 74 54 274 syl3anc 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( U Btwn <. Z , b >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) ) )
276 simp3r 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> p e. ( EE ` N ) )
277 brbtwn 
 |-  ( ( p e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ b e. ( EE ` N ) ) -> ( p Btwn <. Z , b >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) )
278 276 74 54 277 syl3anc 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( p Btwn <. Z , b >. <-> E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) )
279 275 278 anbi12d 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( ( U Btwn <. Z , b >. /\ p Btwn <. Z , b >. ) <-> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) )
280 r19.26 
 |-  ( A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) <-> ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) )
281 280 2rexbii 
 |-  ( E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) <-> E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) )
282 reeanv 
 |-  ( E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) <-> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) )
283 281 282 bitri 
 |-  ( E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) <-> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) )
284 279 283 bitr4di 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( ( U Btwn <. Z , b >. /\ p Btwn <. Z , b >. ) <-> E. t e. ( 0 [,] 1 ) E. s e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( ( U ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( b ` i ) ) ) /\ ( p ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( b ` i ) ) ) ) ) )
285 brbtwn 
 |-  ( ( U e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ p e. ( EE ` N ) ) -> ( U Btwn <. Z , p >. <-> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) ) )
286 273 74 276 285 syl3anc 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( U Btwn <. Z , p >. <-> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) ) )
287 brbtwn 
 |-  ( ( p e. ( EE ` N ) /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) -> ( p Btwn <. Z , U >. <-> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) )
288 276 74 273 287 syl3anc 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( p Btwn <. Z , U >. <-> E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) )
289 286 288 orbi12d 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) <-> ( E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) ) )
290 r19.43 
 |-  ( E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) <-> ( E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ E. r e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) )
291 289 290 bitr4di 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) <-> E. r e. ( 0 [,] 1 ) ( A. i e. ( 1 ... N ) ( U ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( p ` i ) ) ) \/ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - r ) x. ( Z ` i ) ) + ( r x. ( U ` i ) ) ) ) ) )
292 272 284 291 3imtr4d 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) /\ ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> ( ( U Btwn <. Z , b >. /\ p Btwn <. Z , b >. ) -> ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) )
293 292 3expia 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) ) -> ( ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) -> ( ( U Btwn <. Z , b >. /\ p Btwn <. Z , b >. ) -> ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) ) )
294 293 impd 
 |-  ( ( ( N e. NN /\ b e. ( EE ` N ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) ) -> ( ( ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) /\ ( U Btwn <. Z , b >. /\ p Btwn <. Z , b >. ) ) -> ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) )
295 32 294 sylanl2 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ Z =/= U ) ) -> ( ( ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) /\ ( U Btwn <. Z , b >. /\ p Btwn <. Z , b >. ) ) -> ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) )
296 295 3adantr2 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> ( ( ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) /\ ( U Btwn <. Z , b >. /\ p Btwn <. Z , b >. ) ) -> ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) )
297 296 adantr 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> ( ( ( U e. ( EE ` N ) /\ p e. ( EE ` N ) ) /\ ( U Btwn <. Z , b >. /\ p Btwn <. Z , b >. ) ) -> ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) )
298 31 297 mpd 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. A ) -> ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) )
299 298 ralrimiva 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> A. p e. A ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) )
300 299 3exp2 
 |-  ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ b e. ( EE ` N ) /\ A. x e. A x Btwn <. Z , b >. ) ) -> ( Z e. ( EE ` N ) -> ( U e. A -> ( Z =/= U -> A. p e. A ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) ) ) )
301 12 300 syl6 
 |-  ( b e. B -> ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) -> ( Z e. ( EE ` N ) -> ( U e. A -> ( Z =/= U -> A. p e. A ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) ) ) ) )
302 301 exlimiv 
 |-  ( E. b b e. B -> ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) -> ( Z e. ( EE ` N ) -> ( U e. A -> ( Z =/= U -> A. p e. A ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) ) ) ) )
303 3 302 sylbi 
 |-  ( B =/= (/) -> ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) -> ( Z e. ( EE ` N ) -> ( U e. A -> ( Z =/= U -> A. p e. A ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) ) ) ) )
304 303 com4l 
 |-  ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) -> ( Z e. ( EE ` N ) -> ( U e. A -> ( B =/= (/) -> ( Z =/= U -> A. p e. A ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) ) ) ) )
305 304 3impd 
 |-  ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) -> ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) -> ( Z =/= U -> A. p e. A ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) ) )
306 305 imp32 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> A. p e. A ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) )
307 1 sseq2i 
 |-  ( A C_ D <-> A C_ { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) } )
308 ssrab 
 |-  ( A C_ { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) } <-> ( A C_ ( EE ` N ) /\ A. p e. A ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) )
309 307 308 bitri 
 |-  ( A C_ D <-> ( A C_ ( EE ` N ) /\ A. p e. A ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) )
310 2 306 309 sylanbrc 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> A C_ D )