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
|
addid1d |
|- ( ( 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
|
syl5bb |
|- ( ( t e. RR /\ t < 0 ) -> ( 1 = ( t / ( t - 1 ) ) <-> ( ( t - 1 ) x. 1 ) = t ) ) |
84 |
36
|
mulid1d |
|- ( ( 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
|
ffvelrnda |
|- ( ( ( ( ( ( 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
|
ffvelrnda |
|- ( ( ( ( ( ( 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
|
ffvelrnda |
|- ( ( ( ( ( ( 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
|
syl5bb |
|- ( ( ( ( ( ( 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
|
syl5bb |
|- ( ( ( ( ( ( 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
|
ffvelrnda |
|- ( ( ( ( ( ( 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
|
ffvelrnda |
|- ( ( ( ( ( ( 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
|
ffvelrnda |
|- ( ( ( ( ( ( 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
|
syl5bb |
|- ( ( ( ( ( ( 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 ) ) ) ) ) ) |