Metamath Proof Explorer

Theorem eenglngeehlnmlem2

Description: Lemma 2 for eenglngeehlnm . (Contributed by AV, 15-Feb-2023)

Ref Expression
Assertion eenglngeehlnmlem2 
|- ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> 0 e. RR )
2 1red 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> 1 e. RR )
3 simpr 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> t e. RR )
4 reorelicc 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ t e. RR ) -> ( t < 0 \/ t e. ( 0 [,] 1 ) \/ 1 < t ) )
5 1 2 3 4 syl3anc 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> ( t < 0 \/ t e. ( 0 [,] 1 ) \/ 1 < t ) )
6 0xr 
 |-  0 e. RR*
7 6 a1i 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> 0 e. RR* )
8 1xr 
 |-  1 e. RR*
9 8 a1i 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> 1 e. RR* )
10 simpl 
 |-  ( ( t e. RR /\ t < 0 ) -> t e. RR )
11 10 recnd 
 |-  ( ( t e. RR /\ t < 0 ) -> t e. CC )
12 0red 
 |-  ( ( t e. RR /\ t < 0 ) -> 0 e. RR )
13 1red 
 |-  ( ( t e. RR /\ t < 0 ) -> 1 e. RR )
14 simpr 
 |-  ( ( t e. RR /\ t < 0 ) -> t < 0 )
15 0lt1 
 |-  0 < 1
16 15 a1i 
 |-  ( ( t e. RR /\ t < 0 ) -> 0 < 1 )
17 10 12 13 14 16 lttrd 
 |-  ( ( t e. RR /\ t < 0 ) -> t < 1 )
18 10 17 ltned 
 |-  ( ( t e. RR /\ t < 0 ) -> t =/= 1 )
19 1subrec1sub 
 |-  ( ( t e. CC /\ t =/= 1 ) -> ( 1 - ( 1 / ( 1 - t ) ) ) = ( t / ( t - 1 ) ) )
20 11 18 19 syl2anc 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - ( 1 / ( 1 - t ) ) ) = ( t / ( t - 1 ) ) )
21 10 13 resubcld 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t - 1 ) e. RR )
22 1cnd 
 |-  ( ( t e. RR /\ t < 0 ) -> 1 e. CC )
23 11 22 18 subne0d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t - 1 ) =/= 0 )
24 10 21 23 redivcld 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t / ( t - 1 ) ) e. RR )
25 24 rexrd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t / ( t - 1 ) ) e. RR* )
26 20 25 eqeltrd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - ( 1 / ( 1 - t ) ) ) e. RR* )
27 26 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( 1 - ( 1 / ( 1 - t ) ) ) e. RR* )
28 10 renegcld 
 |-  ( ( t e. RR /\ t < 0 ) -> -u t e. RR )
29 10 13 sublt0d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t - 1 ) < 0 <-> t < 1 ) )
30 17 29 mpbird 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t - 1 ) < 0 )
31 21 30 negelrpd 
 |-  ( ( t e. RR /\ t < 0 ) -> -u ( t - 1 ) e. RR+ )
32 10 12 14 ltled 
 |-  ( ( t e. RR /\ t < 0 ) -> t <_ 0 )
33 10 le0neg1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t <_ 0 <-> 0 <_ -u t ) )
34 32 33 mpbid 
 |-  ( ( t e. RR /\ t < 0 ) -> 0 <_ -u t )
35 28 31 34 divge0d 
 |-  ( ( t e. RR /\ t < 0 ) -> 0 <_ ( -u t / -u ( t - 1 ) ) )
36 21 recnd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t - 1 ) e. CC )
37 11 36 23 div2negd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( -u t / -u ( t - 1 ) ) = ( t / ( t - 1 ) ) )
38 20 37 eqtr4d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - ( 1 / ( 1 - t ) ) ) = ( -u t / -u ( t - 1 ) ) )
39 35 38 breqtrrd 
 |-  ( ( t e. RR /\ t < 0 ) -> 0 <_ ( 1 - ( 1 / ( 1 - t ) ) ) )
40 39 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> 0 <_ ( 1 - ( 1 / ( 1 - t ) ) ) )
41 1red 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> 1 e. RR )
42 13 10 resubcld 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - t ) e. RR )
43 10 13 posdifd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t < 1 <-> 0 < ( 1 - t ) ) )
44 17 43 mpbid 
 |-  ( ( t e. RR /\ t < 0 ) -> 0 < ( 1 - t ) )
45 42 44 elrpd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - t ) e. RR+ )
46 45 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( 1 - t ) e. RR+ )
47 46 rpreccld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( 1 / ( 1 - t ) ) e. RR+ )
48 41 47 ltsubrpd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( 1 - ( 1 / ( 1 - t ) ) ) < 1 )
49 7 9 27 40 48 elicod 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( 1 - ( 1 / ( 1 - t ) ) ) e. ( 0 [,) 1 ) )
50 oveq2 
 |-  ( l = ( 1 - ( 1 / ( 1 - t ) ) ) -> ( 1 - l ) = ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) )
51 50 oveq1d 
 |-  ( l = ( 1 - ( 1 / ( 1 - t ) ) ) -> ( ( 1 - l ) x. ( p ` i ) ) = ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) )
52 oveq1 
 |-  ( l = ( 1 - ( 1 / ( 1 - t ) ) ) -> ( l x. ( y ` i ) ) = ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) )
53 51 52 oveq12d 
 |-  ( l = ( 1 - ( 1 / ( 1 - t ) ) ) -> ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) = ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) )
54 53 eqeq2d 
 |-  ( l = ( 1 - ( 1 / ( 1 - t ) ) ) -> ( ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) <-> ( x ` i ) = ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) ) )
55 54 ralbidv 
 |-  ( l = ( 1 - ( 1 / ( 1 - t ) ) ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) <-> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) ) )
56 55 adantl 
 |-  ( ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) /\ l = ( 1 - ( 1 / ( 1 - t ) ) ) ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) <-> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) ) )
57 22 11 subcld 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - t ) e. CC )
58 10 17 gtned 
 |-  ( ( t e. RR /\ t < 0 ) -> 1 =/= t )
59 22 11 58 subne0d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - t ) =/= 0 )
60 57 59 reccld 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 / ( 1 - t ) ) e. CC )
61 22 60 nncand 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) = ( 1 / ( 1 - t ) ) )
62 61 60 eqeltrd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) e. CC )
63 22 60 subcld 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - ( 1 / ( 1 - t ) ) ) e. CC )
64 16 gt0ne0d 
 |-  ( ( t e. RR /\ t < 0 ) -> 1 =/= 0 )
65 36 11 subeq0ad 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( ( t - 1 ) - t ) = 0 <-> ( t - 1 ) = t ) )
66 11 22 11 sub32d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t - 1 ) - t ) = ( ( t - t ) - 1 ) )
67 66 eqeq1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( ( t - 1 ) - t ) = 0 <-> ( ( t - t ) - 1 ) = 0 ) )
68 11 subidd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t - t ) = 0 )
69 68 oveq1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t - t ) - 1 ) = ( 0 - 1 ) )
70 69 eqeq1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( ( t - t ) - 1 ) = 0 <-> ( 0 - 1 ) = 0 ) )
71 0cnd 
 |-  ( ( t e. RR /\ t < 0 ) -> 0 e. CC )
72 71 22 71 subaddd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( 0 - 1 ) = 0 <-> ( 1 + 0 ) = 0 ) )
73 22 addridd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 + 0 ) = 1 )
74 73 eqeq1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( 1 + 0 ) = 0 <-> 1 = 0 ) )
75 72 74 bitrd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( 0 - 1 ) = 0 <-> 1 = 0 ) )
76 67 70 75 3bitrd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( ( t - 1 ) - t ) = 0 <-> 1 = 0 ) )
77 65 76 bitr3d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t - 1 ) = t <-> 1 = 0 ) )
78 77 necon3bid 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t - 1 ) =/= t <-> 1 =/= 0 ) )
79 64 78 mpbird 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t - 1 ) =/= t )
80 20 eqeq2d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 = ( 1 - ( 1 / ( 1 - t ) ) ) <-> 1 = ( t / ( t - 1 ) ) ) )
81 eqcom 
 |-  ( 1 = ( t / ( t - 1 ) ) <-> ( t / ( t - 1 ) ) = 1 )
82 11 36 22 23 divmuld 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t / ( t - 1 ) ) = 1 <-> ( ( t - 1 ) x. 1 ) = t ) )
83 81 82 bitrid 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 = ( t / ( t - 1 ) ) <-> ( ( t - 1 ) x. 1 ) = t ) )
84 36 mulridd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t - 1 ) x. 1 ) = ( t - 1 ) )
85 84 eqeq1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( ( t - 1 ) x. 1 ) = t <-> ( t - 1 ) = t ) )
86 80 83 85 3bitrd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 = ( 1 - ( 1 / ( 1 - t ) ) ) <-> ( t - 1 ) = t ) )
87 86 necon3bid 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 =/= ( 1 - ( 1 / ( 1 - t ) ) ) <-> ( t - 1 ) =/= t ) )
88 79 87 mpbird 
 |-  ( ( t e. RR /\ t < 0 ) -> 1 =/= ( 1 - ( 1 / ( 1 - t ) ) ) )
89 22 63 88 subne0d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) =/= 0 )
90 61 oveq1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( 1 - t ) ) = ( ( 1 / ( 1 - t ) ) x. ( 1 - t ) ) )
91 57 59 recid2d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( 1 / ( 1 - t ) ) x. ( 1 - t ) ) = 1 )
92 90 91 eqtrd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( 1 - t ) ) = 1 )
93 62 57 89 92 mvllmuld 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - t ) = ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) )
94 93 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( 1 - t ) = ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) )
95 94 oveq1d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - t ) x. ( x ` i ) ) = ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) )
96 20 oveq1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) = ( ( t / ( t - 1 ) ) - 1 ) )
97 20 96 oveq12d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) = ( ( t / ( t - 1 ) ) / ( ( t / ( t - 1 ) ) - 1 ) ) )
98 subdivcomb2 
 |-  ( ( t e. CC /\ 1 e. CC /\ ( ( t - 1 ) e. CC /\ ( t - 1 ) =/= 0 ) ) -> ( ( t - ( ( t - 1 ) x. 1 ) ) / ( t - 1 ) ) = ( ( t / ( t - 1 ) ) - 1 ) )
99 11 22 36 23 98 syl112anc 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t - ( ( t - 1 ) x. 1 ) ) / ( t - 1 ) ) = ( ( t / ( t - 1 ) ) - 1 ) )
100 84 oveq2d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t - ( ( t - 1 ) x. 1 ) ) = ( t - ( t - 1 ) ) )
101 11 22 nncand 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t - ( t - 1 ) ) = 1 )
102 100 101 eqtrd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t - ( ( t - 1 ) x. 1 ) ) = 1 )
103 102 oveq1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t - ( ( t - 1 ) x. 1 ) ) / ( t - 1 ) ) = ( 1 / ( t - 1 ) ) )
104 99 103 eqtr3d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t / ( t - 1 ) ) - 1 ) = ( 1 / ( t - 1 ) ) )
105 104 oveq1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( ( t / ( t - 1 ) ) - 1 ) x. t ) = ( ( 1 / ( t - 1 ) ) x. t ) )
106 11 36 23 divrec2d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t / ( t - 1 ) ) = ( ( 1 / ( t - 1 ) ) x. t ) )
107 105 106 eqtr4d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( ( t / ( t - 1 ) ) - 1 ) x. t ) = ( t / ( t - 1 ) ) )
108 20 63 eqeltrrd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t / ( t - 1 ) ) e. CC )
109 108 22 subcld 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t / ( t - 1 ) ) - 1 ) e. CC )
110 79 necomd 
 |-  ( ( t e. RR /\ t < 0 ) -> t =/= ( t - 1 ) )
111 11 36 23 110 divne1d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( t / ( t - 1 ) ) =/= 1 )
112 108 22 111 subne0d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t / ( t - 1 ) ) - 1 ) =/= 0 )
113 108 109 11 112 divmuld 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( ( t / ( t - 1 ) ) / ( ( t / ( t - 1 ) ) - 1 ) ) = t <-> ( ( ( t / ( t - 1 ) ) - 1 ) x. t ) = ( t / ( t - 1 ) ) ) )
114 107 113 mpbird 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( t / ( t - 1 ) ) / ( ( t / ( t - 1 ) ) - 1 ) ) = t )
115 97 114 eqtr2d 
 |-  ( ( t e. RR /\ t < 0 ) -> t = ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) )
116 115 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> t = ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) )
117 116 oveq1d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( t x. ( y ` i ) ) = ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) )
118 95 117 oveq12d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) = ( ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) + ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) ) )
119 118 eqeq2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) <-> ( p ` i ) = ( ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) + ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) ) ) )
120 119 biimpd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( p ` i ) = ( ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) + ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) ) ) )
121 eqcom 
 |-  ( ( x ` i ) = ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) <-> ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) = ( x ` i ) )
122 elmapi 
 |-  ( x e. ( RR ^m ( 1 ... N ) ) -> x : ( 1 ... N ) --> RR )
123 122 3ad2ant2 
 |-  ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) -> x : ( 1 ... N ) --> RR )
124 123 adantr 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> x : ( 1 ... N ) --> RR )
125 124 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) -> x : ( 1 ... N ) --> RR )
126 125 ffvelcdmda 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. RR )
127 126 recnd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. CC )
128 1cnd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> 1 e. CC )
129 11 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> t e. CC )
130 128 129 subcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( 1 - t ) e. CC )
131 58 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> 1 =/= t )
132 128 129 131 subne0d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( 1 - t ) =/= 0 )
133 130 132 reccld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( 1 / ( 1 - t ) ) e. CC )
134 128 133 subcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( 1 - ( 1 / ( 1 - t ) ) ) e. CC )
135 eldifi 
 |-  ( y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) -> y e. ( RR ^m ( 1 ... N ) ) )
136 elmapi 
 |-  ( y e. ( RR ^m ( 1 ... N ) ) -> y : ( 1 ... N ) --> RR )
137 135 136 syl 
 |-  ( y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) -> y : ( 1 ... N ) --> RR )
138 137 3ad2ant3 
 |-  ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) -> y : ( 1 ... N ) --> RR )
139 138 adantr 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> y : ( 1 ... N ) --> RR )
140 139 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) -> y : ( 1 ... N ) --> RR )
141 140 ffvelcdmda 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) e. RR )
142 141 recnd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) e. CC )
143 134 142 mulcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) e. CC )
144 62 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) e. CC )
145 elmapi 
 |-  ( p e. ( RR ^m ( 1 ... N ) ) -> p : ( 1 ... N ) --> RR )
146 145 adantl 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> p : ( 1 ... N ) --> RR )
147 146 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) -> p : ( 1 ... N ) --> RR )
148 147 ffvelcdmda 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( p ` i ) e. RR )
149 148 recnd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( p ` i ) e. CC )
150 144 149 mulcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) e. CC )
151 127 143 150 subadd2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) = ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) <-> ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) = ( x ` i ) ) )
152 121 151 bitr4id 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) = ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) <-> ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) = ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) ) )
153 eqcom 
 |-  ( ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) = ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) <-> ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) = ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) )
154 127 143 subcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) e. CC )
155 89 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) =/= 0 )
156 154 144 149 155 divmuld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) = ( p ` i ) <-> ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) = ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) ) )
157 eqcom 
 |-  ( ( ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) = ( p ` i ) <-> ( p ` i ) = ( ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) )
158 127 143 144 155 divsubdird 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) = ( ( ( x ` i ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) - ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) ) )
159 127 144 155 divcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) e. CC )
160 143 144 155 divcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) e. CC )
161 159 160 negsubd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) + -u ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) ) = ( ( ( x ` i ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) - ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) ) )
162 127 144 155 divrec2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) = ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) )
163 143 144 155 divneg2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> -u ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) = ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / -u ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) )
164 128 134 negsubdi2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> -u ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) = ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) )
165 164 oveq2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / -u ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) = ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) )
166 134 128 subcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) e. CC )
167 88 necomd 
 |-  ( ( t e. RR /\ t < 0 ) -> ( 1 - ( 1 / ( 1 - t ) ) ) =/= 1 )
168 63 22 167 subne0d 
 |-  ( ( t e. RR /\ t < 0 ) -> ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) =/= 0 )
169 168 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) =/= 0 )
170 134 142 166 169 div23d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) = ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) )
171 163 165 170 3eqtrd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> -u ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) = ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) )
172 162 171 oveq12d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) + -u ( ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) ) = ( ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) + ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) ) )
173 158 161 172 3eqtr2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) = ( ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) + ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) ) )
174 173 eqeq2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) <-> ( p ` i ) = ( ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) + ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) ) ) )
175 157 174 bitrid 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) = ( p ` i ) <-> ( p ` i ) = ( ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) + ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) ) ) )
176 156 175 bitr3d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) = ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) <-> ( p ` i ) = ( ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) + ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) ) ) )
177 153 176 bitrid 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( ( x ` i ) - ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) = ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) <-> ( p ` i ) = ( ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) + ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) ) ) )
178 152 177 bitrd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( x ` i ) = ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) <-> ( p ` i ) = ( ( ( 1 / ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) ) x. ( x ` i ) ) + ( ( ( 1 - ( 1 / ( 1 - t ) ) ) / ( ( 1 - ( 1 / ( 1 - t ) ) ) - 1 ) ) x. ( y ` i ) ) ) ) )
179 120 178 sylibrd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( x ` i ) = ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) ) )
180 179 ralimdva 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) ) )
181 180 imp 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - ( 1 - ( 1 / ( 1 - t ) ) ) ) x. ( p ` i ) ) + ( ( 1 - ( 1 / ( 1 - t ) ) ) x. ( y ` i ) ) ) )
182 49 56 181 rspcedvd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) )
183 182 3mix2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ t < 0 ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) )
184 183 exp31 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> ( t < 0 -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) ) )
185 184 com23 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( t < 0 -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) ) )
186 185 imp 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( t < 0 -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) )
187 simpr 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) /\ t e. ( 0 [,] 1 ) ) -> t e. ( 0 [,] 1 ) )
188 oveq2 
 |-  ( k = t -> ( 1 - k ) = ( 1 - t ) )
189 188 oveq1d 
 |-  ( k = t -> ( ( 1 - k ) x. ( x ` i ) ) = ( ( 1 - t ) x. ( x ` i ) ) )
190 oveq1 
 |-  ( k = t -> ( k x. ( y ` i ) ) = ( t x. ( y ` i ) ) )
191 189 190 oveq12d 
 |-  ( k = t -> ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) )
192 191 eqeq2d 
 |-  ( k = t -> ( ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) <-> ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
193 192 ralbidv 
 |-  ( k = t -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) <-> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
194 193 adantl 
 |-  ( ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) /\ t e. ( 0 [,] 1 ) ) /\ k = t ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) <-> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) )
195 simplr 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) /\ t e. ( 0 [,] 1 ) ) -> A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) )
196 187 194 195 rspcedvd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) /\ t e. ( 0 [,] 1 ) ) -> E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) )
197 196 3mix1d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) /\ t e. ( 0 [,] 1 ) ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) )
198 197 ex 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( t e. ( 0 [,] 1 ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) )
199 1red 
 |-  ( ( t e. RR /\ 1 < t ) -> 1 e. RR )
200 simpl 
 |-  ( ( t e. RR /\ 1 < t ) -> t e. RR )
201 0red 
 |-  ( ( t e. RR /\ 1 < t ) -> 0 e. RR )
202 15 a1i 
 |-  ( ( t e. RR /\ 1 < t ) -> 0 < 1 )
203 simpr 
 |-  ( ( t e. RR /\ 1 < t ) -> 1 < t )
204 201 199 200 202 203 lttrd 
 |-  ( ( t e. RR /\ 1 < t ) -> 0 < t )
205 204 gt0ne0d 
 |-  ( ( t e. RR /\ 1 < t ) -> t =/= 0 )
206 199 200 205 redivcld 
 |-  ( ( t e. RR /\ 1 < t ) -> ( 1 / t ) e. RR )
207 200 204 recgt0d 
 |-  ( ( t e. RR /\ 1 < t ) -> 0 < ( 1 / t ) )
208 recgt1i 
 |-  ( ( t e. RR /\ 1 < t ) -> ( 0 < ( 1 / t ) /\ ( 1 / t ) < 1 ) )
209 206 adantr 
 |-  ( ( ( t e. RR /\ 1 < t ) /\ ( 0 < ( 1 / t ) /\ ( 1 / t ) < 1 ) ) -> ( 1 / t ) e. RR )
210 1red 
 |-  ( ( ( t e. RR /\ 1 < t ) /\ ( 0 < ( 1 / t ) /\ ( 1 / t ) < 1 ) ) -> 1 e. RR )
211 simprr 
 |-  ( ( ( t e. RR /\ 1 < t ) /\ ( 0 < ( 1 / t ) /\ ( 1 / t ) < 1 ) ) -> ( 1 / t ) < 1 )
212 209 210 211 ltled 
 |-  ( ( ( t e. RR /\ 1 < t ) /\ ( 0 < ( 1 / t ) /\ ( 1 / t ) < 1 ) ) -> ( 1 / t ) <_ 1 )
213 208 212 mpdan 
 |-  ( ( t e. RR /\ 1 < t ) -> ( 1 / t ) <_ 1 )
214 206 207 213 3jca 
 |-  ( ( t e. RR /\ 1 < t ) -> ( ( 1 / t ) e. RR /\ 0 < ( 1 / t ) /\ ( 1 / t ) <_ 1 ) )
215 1re 
 |-  1 e. RR
216 6 215 pm3.2i 
 |-  ( 0 e. RR* /\ 1 e. RR )
217 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( ( 1 / t ) e. ( 0 (,] 1 ) <-> ( ( 1 / t ) e. RR /\ 0 < ( 1 / t ) /\ ( 1 / t ) <_ 1 ) ) )
218 216 217 mp1i 
 |-  ( ( t e. RR /\ 1 < t ) -> ( ( 1 / t ) e. ( 0 (,] 1 ) <-> ( ( 1 / t ) e. RR /\ 0 < ( 1 / t ) /\ ( 1 / t ) <_ 1 ) ) )
219 214 218 mpbird 
 |-  ( ( t e. RR /\ 1 < t ) -> ( 1 / t ) e. ( 0 (,] 1 ) )
220 219 ad4ant23 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( 1 / t ) e. ( 0 (,] 1 ) )
221 oveq2 
 |-  ( m = ( 1 / t ) -> ( 1 - m ) = ( 1 - ( 1 / t ) ) )
222 221 oveq1d 
 |-  ( m = ( 1 / t ) -> ( ( 1 - m ) x. ( x ` i ) ) = ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) )
223 oveq1 
 |-  ( m = ( 1 / t ) -> ( m x. ( p ` i ) ) = ( ( 1 / t ) x. ( p ` i ) ) )
224 222 223 oveq12d 
 |-  ( m = ( 1 / t ) -> ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) = ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) )
225 224 eqeq2d 
 |-  ( m = ( 1 / t ) -> ( ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) <-> ( y ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) ) )
226 225 ralbidv 
 |-  ( m = ( 1 / t ) -> ( A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) <-> A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) ) )
227 226 adantl 
 |-  ( ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) /\ m = ( 1 / t ) ) -> ( A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) <-> A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) ) )
228 simplr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) -> t e. RR )
229 228 recnd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) -> t e. CC )
230 229 adantr 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> t e. CC )
231 204 ex 
 |-  ( t e. RR -> ( 1 < t -> 0 < t ) )
232 gt0ne0 
 |-  ( ( t e. RR /\ 0 < t ) -> t =/= 0 )
233 232 ex 
 |-  ( t e. RR -> ( 0 < t -> t =/= 0 ) )
234 231 233 syld 
 |-  ( t e. RR -> ( 1 < t -> t =/= 0 ) )
235 234 adantl 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> ( 1 < t -> t =/= 0 ) )
236 235 imp 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) -> t =/= 0 )
237 236 adantr 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> t =/= 0 )
238 230 237 reccld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( 1 / t ) e. CC )
239 1cnd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> 1 e. CC )
240 230 237 recne0d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( 1 / t ) =/= 0 )
241 238 239 238 240 divsubdird 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) = ( ( ( 1 / t ) / ( 1 / t ) ) - ( 1 / ( 1 / t ) ) ) )
242 238 240 dividd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( 1 / t ) / ( 1 / t ) ) = 1 )
243 230 237 recrecd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( 1 / ( 1 / t ) ) = t )
244 242 243 oveq12d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 / t ) / ( 1 / t ) ) - ( 1 / ( 1 / t ) ) ) = ( 1 - t ) )
245 241 244 eqtr2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( 1 - t ) = ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) )
246 245 oveq1d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - t ) x. ( x ` i ) ) = ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) )
247 229 236 recrecd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) -> ( 1 / ( 1 / t ) ) = t )
248 247 eqcomd 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) -> t = ( 1 / ( 1 / t ) ) )
249 248 adantr 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> t = ( 1 / ( 1 / t ) ) )
250 249 oveq1d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( t x. ( y ` i ) ) = ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) )
251 246 250 oveq12d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) = ( ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) ) )
252 251 eqeq2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) <-> ( p ` i ) = ( ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) ) ) )
253 252 biimpd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( p ` i ) = ( ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) ) ) )
254 eqcom 
 |-  ( ( y ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) <-> ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) = ( y ` i ) )
255 139 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) -> y : ( 1 ... N ) --> RR )
256 255 ffvelcdmda 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) e. RR )
257 256 recnd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( y ` i ) e. CC )
258 239 238 subcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( 1 - ( 1 / t ) ) e. CC )
259 124 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) -> x : ( 1 ... N ) --> RR )
260 259 ffvelcdmda 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. RR )
261 260 recnd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( x ` i ) e. CC )
262 258 261 mulcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) e. CC )
263 146 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) -> p : ( 1 ... N ) --> RR )
264 263 ffvelcdmda 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( p ` i ) e. RR )
265 264 recnd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( p ` i ) e. CC )
266 238 265 mulcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( 1 / t ) x. ( p ` i ) ) e. CC )
267 257 262 266 subaddd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) = ( ( 1 / t ) x. ( p ` i ) ) <-> ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) = ( y ` i ) ) )
268 254 267 bitr4id 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) <-> ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) = ( ( 1 / t ) x. ( p ` i ) ) ) )
269 eqcom 
 |-  ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) = ( ( 1 / t ) x. ( p ` i ) ) <-> ( ( 1 / t ) x. ( p ` i ) ) = ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) )
270 257 262 subcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) e. CC )
271 270 238 265 240 divmuld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) / ( 1 / t ) ) = ( p ` i ) <-> ( ( 1 / t ) x. ( p ` i ) ) = ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) ) )
272 269 271 bitr4id 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) = ( ( 1 / t ) x. ( p ` i ) ) <-> ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) / ( 1 / t ) ) = ( p ` i ) ) )
273 eqcom 
 |-  ( ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) / ( 1 / t ) ) = ( p ` i ) <-> ( p ` i ) = ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) / ( 1 / t ) ) )
274 257 262 238 240 divsubdird 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) / ( 1 / t ) ) = ( ( ( y ` i ) / ( 1 / t ) ) - ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) ) )
275 257 238 240 divcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) / ( 1 / t ) ) e. CC )
276 262 238 240 divcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) e. CC )
277 275 276 negsubd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) / ( 1 / t ) ) + -u ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) ) = ( ( ( y ` i ) / ( 1 / t ) ) - ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) ) )
278 262 238 240 divnegd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> -u ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) = ( -u ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) )
279 258 261 mulneg1d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( -u ( 1 - ( 1 / t ) ) x. ( x ` i ) ) = -u ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) )
280 279 eqcomd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> -u ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) = ( -u ( 1 - ( 1 / t ) ) x. ( x ` i ) ) )
281 280 oveq1d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( -u ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) = ( ( -u ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) )
282 239 238 negsubdi2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> -u ( 1 - ( 1 / t ) ) = ( ( 1 / t ) - 1 ) )
283 282 oveq1d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( -u ( 1 - ( 1 / t ) ) x. ( x ` i ) ) = ( ( ( 1 / t ) - 1 ) x. ( x ` i ) ) )
284 283 oveq1d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( -u ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) = ( ( ( ( 1 / t ) - 1 ) x. ( x ` i ) ) / ( 1 / t ) ) )
285 238 239 subcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( 1 / t ) - 1 ) e. CC )
286 285 261 238 240 div23d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 / t ) - 1 ) x. ( x ` i ) ) / ( 1 / t ) ) = ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) )
287 284 286 eqtrd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( -u ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) = ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) )
288 278 281 287 3eqtrd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> -u ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) = ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) )
289 288 oveq2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) / ( 1 / t ) ) + -u ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) ) = ( ( ( y ` i ) / ( 1 / t ) ) + ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) ) )
290 257 238 240 divrec2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) / ( 1 / t ) ) = ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) )
291 290 oveq1d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) / ( 1 / t ) ) + ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) ) = ( ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) + ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) ) )
292 238 240 reccld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( 1 / ( 1 / t ) ) e. CC )
293 292 257 mulcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) e. CC )
294 285 238 240 divcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) e. CC )
295 294 261 mulcld 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) e. CC )
296 293 295 addcomd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) + ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) ) = ( ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) ) )
297 289 291 296 3eqtrd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) / ( 1 / t ) ) + -u ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) / ( 1 / t ) ) ) = ( ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) ) )
298 274 277 297 3eqtr2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) / ( 1 / t ) ) = ( ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) ) )
299 298 eqeq2d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) / ( 1 / t ) ) <-> ( p ` i ) = ( ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) ) ) )
300 273 299 bitrid 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( ( ( y ` i ) - ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) ) / ( 1 / t ) ) = ( p ` i ) <-> ( p ` i ) = ( ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) ) ) )
301 268 272 300 3bitrd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( y ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) <-> ( p ` i ) = ( ( ( ( ( 1 / t ) - 1 ) / ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / ( 1 / t ) ) x. ( y ` i ) ) ) ) )
302 253 301 sylibrd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ i e. ( 1 ... N ) ) -> ( ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( y ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) ) )
303 302 ralimdva 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) ) )
304 303 imp 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - ( 1 / t ) ) x. ( x ` i ) ) + ( ( 1 / t ) x. ( p ` i ) ) ) )
305 220 227 304 rspcedvd 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) )
306 305 3mix3d 
 |-  ( ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ 1 < t ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) )
307 306 exp31 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> ( 1 < t -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) ) )
308 307 com23 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( 1 < t -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) ) )
309 308 imp 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( 1 < t -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) )
310 186 198 309 3jaod 
 |-  ( ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) /\ A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) ) -> ( ( t < 0 \/ t e. ( 0 [,] 1 ) \/ 1 < t ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) )
311 310 ex 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( ( t < 0 \/ t e. ( 0 [,] 1 ) \/ 1 < t ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) ) )
312 5 311 mpid 
 |-  ( ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) /\ t e. RR ) -> ( A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) )
313 312 rexlimdva 
 |-  ( ( ( N e. NN /\ x e. ( RR ^m ( 1 ... N ) ) /\ y e. ( ( RR ^m ( 1 ... N ) ) \ { x } ) ) /\ p e. ( RR ^m ( 1 ... N ) ) ) -> ( E. t e. RR A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - t ) x. ( x ` i ) ) + ( t x. ( y ` i ) ) ) -> ( E. k e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( p ` i ) = ( ( ( 1 - k ) x. ( x ` i ) ) + ( k x. ( y ` i ) ) ) \/ E. l e. ( 0 [,) 1 ) A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - l ) x. ( p ` i ) ) + ( l x. ( y ` i ) ) ) \/ E. m e. ( 0 (,] 1 ) A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - m ) x. ( x ` i ) ) + ( m x. ( p ` i ) ) ) ) ) )