Step |
Hyp |
Ref |
Expression |
1 |
|
stoweidlem34.1 |
|- F/_ t F |
2 |
|
stoweidlem34.2 |
|- F/ j ph |
3 |
|
stoweidlem34.3 |
|- F/ t ph |
4 |
|
stoweidlem34.4 |
|- D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) |
5 |
|
stoweidlem34.5 |
|- B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } ) |
6 |
|
stoweidlem34.6 |
|- J = ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } ) |
7 |
|
stoweidlem34.7 |
|- ( ph -> N e. NN ) |
8 |
|
stoweidlem34.8 |
|- ( ph -> T e. _V ) |
9 |
|
stoweidlem34.9 |
|- ( ph -> F : T --> RR ) |
10 |
|
stoweidlem34.10 |
|- ( ( ph /\ t e. T ) -> 0 <_ ( F ` t ) ) |
11 |
|
stoweidlem34.11 |
|- ( ( ph /\ t e. T ) -> ( F ` t ) < ( ( N - 1 ) x. E ) ) |
12 |
|
stoweidlem34.12 |
|- ( ph -> E e. RR+ ) |
13 |
|
stoweidlem34.13 |
|- ( ph -> E < ( 1 / 3 ) ) |
14 |
|
stoweidlem34.14 |
|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( X ` j ) : T --> RR ) |
15 |
|
stoweidlem34.15 |
|- ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` j ) ` t ) ) |
16 |
|
stoweidlem34.16 |
|- ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` j ) ` t ) <_ 1 ) |
17 |
|
stoweidlem34.17 |
|- ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( D ` j ) ) -> ( ( X ` j ) ` t ) < ( E / N ) ) |
18 |
|
stoweidlem34.18 |
|- ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( B ` j ) ) -> ( 1 - ( E / N ) ) < ( ( X ` j ) ` t ) ) |
19 |
|
simpr |
|- ( ( ph /\ t e. T ) -> t e. T ) |
20 |
|
ovex |
|- ( 1 ... N ) e. _V |
21 |
20
|
rabex |
|- { j e. ( 1 ... N ) | t e. ( D ` j ) } e. _V |
22 |
6
|
fvmpt2 |
|- ( ( t e. T /\ { j e. ( 1 ... N ) | t e. ( D ` j ) } e. _V ) -> ( J ` t ) = { j e. ( 1 ... N ) | t e. ( D ` j ) } ) |
23 |
19 21 22
|
sylancl |
|- ( ( ph /\ t e. T ) -> ( J ` t ) = { j e. ( 1 ... N ) | t e. ( D ` j ) } ) |
24 |
|
ssrab2 |
|- { j e. ( 1 ... N ) | t e. ( D ` j ) } C_ ( 1 ... N ) |
25 |
23 24
|
eqsstrdi |
|- ( ( ph /\ t e. T ) -> ( J ` t ) C_ ( 1 ... N ) ) |
26 |
|
elfznn |
|- ( x e. ( 1 ... N ) -> x e. NN ) |
27 |
26
|
ssriv |
|- ( 1 ... N ) C_ NN |
28 |
25 27
|
sstrdi |
|- ( ( ph /\ t e. T ) -> ( J ` t ) C_ NN ) |
29 |
|
nnssre |
|- NN C_ RR |
30 |
28 29
|
sstrdi |
|- ( ( ph /\ t e. T ) -> ( J ` t ) C_ RR ) |
31 |
7
|
adantr |
|- ( ( ph /\ t e. T ) -> N e. NN ) |
32 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
33 |
31 32
|
eleqtrdi |
|- ( ( ph /\ t e. T ) -> N e. ( ZZ>= ` 1 ) ) |
34 |
|
eluzfz2 |
|- ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) ) |
35 |
33 34
|
syl |
|- ( ( ph /\ t e. T ) -> N e. ( 1 ... N ) ) |
36 |
|
3re |
|- 3 e. RR |
37 |
|
3ne0 |
|- 3 =/= 0 |
38 |
36 37
|
rereccli |
|- ( 1 / 3 ) e. RR |
39 |
38
|
a1i |
|- ( ( ph /\ t e. T ) -> ( 1 / 3 ) e. RR ) |
40 |
|
1red |
|- ( ( ph /\ t e. T ) -> 1 e. RR ) |
41 |
31
|
nnred |
|- ( ( ph /\ t e. T ) -> N e. RR ) |
42 |
|
1lt3 |
|- 1 < 3 |
43 |
36 42
|
pm3.2i |
|- ( 3 e. RR /\ 1 < 3 ) |
44 |
|
recgt1i |
|- ( ( 3 e. RR /\ 1 < 3 ) -> ( 0 < ( 1 / 3 ) /\ ( 1 / 3 ) < 1 ) ) |
45 |
44
|
simprd |
|- ( ( 3 e. RR /\ 1 < 3 ) -> ( 1 / 3 ) < 1 ) |
46 |
43 45
|
mp1i |
|- ( ( ph /\ t e. T ) -> ( 1 / 3 ) < 1 ) |
47 |
39 40 41 46
|
ltsub2dd |
|- ( ( ph /\ t e. T ) -> ( N - 1 ) < ( N - ( 1 / 3 ) ) ) |
48 |
41 40
|
resubcld |
|- ( ( ph /\ t e. T ) -> ( N - 1 ) e. RR ) |
49 |
41 39
|
resubcld |
|- ( ( ph /\ t e. T ) -> ( N - ( 1 / 3 ) ) e. RR ) |
50 |
12
|
rpred |
|- ( ph -> E e. RR ) |
51 |
50
|
adantr |
|- ( ( ph /\ t e. T ) -> E e. RR ) |
52 |
12
|
rpgt0d |
|- ( ph -> 0 < E ) |
53 |
52
|
adantr |
|- ( ( ph /\ t e. T ) -> 0 < E ) |
54 |
|
ltmul1 |
|- ( ( ( N - 1 ) e. RR /\ ( N - ( 1 / 3 ) ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( N - 1 ) < ( N - ( 1 / 3 ) ) <-> ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) ) |
55 |
48 49 51 53 54
|
syl112anc |
|- ( ( ph /\ t e. T ) -> ( ( N - 1 ) < ( N - ( 1 / 3 ) ) <-> ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) ) |
56 |
47 55
|
mpbid |
|- ( ( ph /\ t e. T ) -> ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) |
57 |
11 56
|
jca |
|- ( ( ph /\ t e. T ) -> ( ( F ` t ) < ( ( N - 1 ) x. E ) /\ ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) ) |
58 |
9
|
ffvelrnda |
|- ( ( ph /\ t e. T ) -> ( F ` t ) e. RR ) |
59 |
48 51
|
remulcld |
|- ( ( ph /\ t e. T ) -> ( ( N - 1 ) x. E ) e. RR ) |
60 |
49 51
|
remulcld |
|- ( ( ph /\ t e. T ) -> ( ( N - ( 1 / 3 ) ) x. E ) e. RR ) |
61 |
|
lttr |
|- ( ( ( F ` t ) e. RR /\ ( ( N - 1 ) x. E ) e. RR /\ ( ( N - ( 1 / 3 ) ) x. E ) e. RR ) -> ( ( ( F ` t ) < ( ( N - 1 ) x. E ) /\ ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) -> ( F ` t ) < ( ( N - ( 1 / 3 ) ) x. E ) ) ) |
62 |
|
ltle |
|- ( ( ( F ` t ) e. RR /\ ( ( N - ( 1 / 3 ) ) x. E ) e. RR ) -> ( ( F ` t ) < ( ( N - ( 1 / 3 ) ) x. E ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) ) |
63 |
62
|
3adant2 |
|- ( ( ( F ` t ) e. RR /\ ( ( N - 1 ) x. E ) e. RR /\ ( ( N - ( 1 / 3 ) ) x. E ) e. RR ) -> ( ( F ` t ) < ( ( N - ( 1 / 3 ) ) x. E ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) ) |
64 |
61 63
|
syld |
|- ( ( ( F ` t ) e. RR /\ ( ( N - 1 ) x. E ) e. RR /\ ( ( N - ( 1 / 3 ) ) x. E ) e. RR ) -> ( ( ( F ` t ) < ( ( N - 1 ) x. E ) /\ ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) ) |
65 |
58 59 60 64
|
syl3anc |
|- ( ( ph /\ t e. T ) -> ( ( ( F ` t ) < ( ( N - 1 ) x. E ) /\ ( ( N - 1 ) x. E ) < ( ( N - ( 1 / 3 ) ) x. E ) ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) ) |
66 |
57 65
|
mpd |
|- ( ( ph /\ t e. T ) -> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) |
67 |
|
rabid |
|- ( t e. { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) ) |
68 |
19 66 67
|
sylanbrc |
|- ( ( ph /\ t e. T ) -> t e. { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } ) |
69 |
|
oveq1 |
|- ( j = N -> ( j - ( 1 / 3 ) ) = ( N - ( 1 / 3 ) ) ) |
70 |
69
|
oveq1d |
|- ( j = N -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( N - ( 1 / 3 ) ) x. E ) ) |
71 |
70
|
breq2d |
|- ( j = N -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) ) ) |
72 |
71
|
rabbidv |
|- ( j = N -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } ) |
73 |
|
nnnn0 |
|- ( N e. NN -> N e. NN0 ) |
74 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
75 |
73 74
|
eleqtrdi |
|- ( N e. NN -> N e. ( ZZ>= ` 0 ) ) |
76 |
|
eluzfz2 |
|- ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) ) |
77 |
7 75 76
|
3syl |
|- ( ph -> N e. ( 0 ... N ) ) |
78 |
|
rabexg |
|- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } e. _V ) |
79 |
8 78
|
syl |
|- ( ph -> { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } e. _V ) |
80 |
4 72 77 79
|
fvmptd3 |
|- ( ph -> ( D ` N ) = { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } ) |
81 |
80
|
adantr |
|- ( ( ph /\ t e. T ) -> ( D ` N ) = { t e. T | ( F ` t ) <_ ( ( N - ( 1 / 3 ) ) x. E ) } ) |
82 |
68 81
|
eleqtrrd |
|- ( ( ph /\ t e. T ) -> t e. ( D ` N ) ) |
83 |
|
nfcv |
|- F/_ j N |
84 |
|
nfcv |
|- F/_ j ( 1 ... N ) |
85 |
|
nfmpt1 |
|- F/_ j ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) |
86 |
4 85
|
nfcxfr |
|- F/_ j D |
87 |
86 83
|
nffv |
|- F/_ j ( D ` N ) |
88 |
87
|
nfcri |
|- F/ j t e. ( D ` N ) |
89 |
|
fveq2 |
|- ( j = N -> ( D ` j ) = ( D ` N ) ) |
90 |
89
|
eleq2d |
|- ( j = N -> ( t e. ( D ` j ) <-> t e. ( D ` N ) ) ) |
91 |
83 84 88 90
|
elrabf |
|- ( N e. { j e. ( 1 ... N ) | t e. ( D ` j ) } <-> ( N e. ( 1 ... N ) /\ t e. ( D ` N ) ) ) |
92 |
35 82 91
|
sylanbrc |
|- ( ( ph /\ t e. T ) -> N e. { j e. ( 1 ... N ) | t e. ( D ` j ) } ) |
93 |
92 23
|
eleqtrrd |
|- ( ( ph /\ t e. T ) -> N e. ( J ` t ) ) |
94 |
|
ne0i |
|- ( N e. ( J ` t ) -> ( J ` t ) =/= (/) ) |
95 |
93 94
|
syl |
|- ( ( ph /\ t e. T ) -> ( J ` t ) =/= (/) ) |
96 |
|
nnwo |
|- ( ( ( J ` t ) C_ NN /\ ( J ` t ) =/= (/) ) -> E. i e. ( J ` t ) A. k e. ( J ` t ) i <_ k ) |
97 |
|
nfcv |
|- F/_ i ( J ` t ) |
98 |
|
nfcv |
|- F/_ j T |
99 |
|
nfrab1 |
|- F/_ j { j e. ( 1 ... N ) | t e. ( D ` j ) } |
100 |
98 99
|
nfmpt |
|- F/_ j ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } ) |
101 |
6 100
|
nfcxfr |
|- F/_ j J |
102 |
|
nfcv |
|- F/_ j t |
103 |
101 102
|
nffv |
|- F/_ j ( J ` t ) |
104 |
|
nfv |
|- F/ j i <_ k |
105 |
103 104
|
nfralw |
|- F/ j A. k e. ( J ` t ) i <_ k |
106 |
|
nfv |
|- F/ i A. k e. ( J ` t ) j <_ k |
107 |
|
breq1 |
|- ( i = j -> ( i <_ k <-> j <_ k ) ) |
108 |
107
|
ralbidv |
|- ( i = j -> ( A. k e. ( J ` t ) i <_ k <-> A. k e. ( J ` t ) j <_ k ) ) |
109 |
97 103 105 106 108
|
cbvrexfw |
|- ( E. i e. ( J ` t ) A. k e. ( J ` t ) i <_ k <-> E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k ) |
110 |
96 109
|
sylib |
|- ( ( ( J ` t ) C_ NN /\ ( J ` t ) =/= (/) ) -> E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k ) |
111 |
28 95 110
|
syl2anc |
|- ( ( ph /\ t e. T ) -> E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k ) |
112 |
|
nfv |
|- F/ j t e. T |
113 |
2 112
|
nfan |
|- F/ j ( ph /\ t e. T ) |
114 |
23
|
eleq2d |
|- ( ( ph /\ t e. T ) -> ( j e. ( J ` t ) <-> j e. { j e. ( 1 ... N ) | t e. ( D ` j ) } ) ) |
115 |
114
|
biimpa |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> j e. { j e. ( 1 ... N ) | t e. ( D ` j ) } ) |
116 |
|
rabid |
|- ( j e. { j e. ( 1 ... N ) | t e. ( D ` j ) } <-> ( j e. ( 1 ... N ) /\ t e. ( D ` j ) ) ) |
117 |
115 116
|
sylib |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( j e. ( 1 ... N ) /\ t e. ( D ` j ) ) ) |
118 |
117
|
simprd |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> t e. ( D ` j ) ) |
119 |
118
|
adantr |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ A. k e. ( J ` t ) j <_ k ) -> t e. ( D ` j ) ) |
120 |
|
simp3 |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> t e. ( D ` ( j - 1 ) ) ) |
121 |
|
simp1l |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ph ) |
122 |
|
noel |
|- -. t e. (/) |
123 |
|
oveq1 |
|- ( j = 1 -> ( j - 1 ) = ( 1 - 1 ) ) |
124 |
|
1m1e0 |
|- ( 1 - 1 ) = 0 |
125 |
123 124
|
eqtrdi |
|- ( j = 1 -> ( j - 1 ) = 0 ) |
126 |
125
|
fveq2d |
|- ( j = 1 -> ( D ` ( j - 1 ) ) = ( D ` 0 ) ) |
127 |
36
|
a1i |
|- ( ( ph /\ t e. T ) -> 3 e. RR ) |
128 |
37
|
a1i |
|- ( ( ph /\ t e. T ) -> 3 =/= 0 ) |
129 |
40 127 128
|
redivcld |
|- ( ( ph /\ t e. T ) -> ( 1 / 3 ) e. RR ) |
130 |
129
|
renegcld |
|- ( ( ph /\ t e. T ) -> -u ( 1 / 3 ) e. RR ) |
131 |
130 51
|
remulcld |
|- ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) e. RR ) |
132 |
|
0red |
|- ( ( ph /\ t e. T ) -> 0 e. RR ) |
133 |
|
3pos |
|- 0 < 3 |
134 |
36 133
|
recgt0ii |
|- 0 < ( 1 / 3 ) |
135 |
|
lt0neg2 |
|- ( ( 1 / 3 ) e. RR -> ( 0 < ( 1 / 3 ) <-> -u ( 1 / 3 ) < 0 ) ) |
136 |
38 135
|
ax-mp |
|- ( 0 < ( 1 / 3 ) <-> -u ( 1 / 3 ) < 0 ) |
137 |
134 136
|
mpbi |
|- -u ( 1 / 3 ) < 0 |
138 |
|
ltmul1 |
|- ( ( -u ( 1 / 3 ) e. RR /\ 0 e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( -u ( 1 / 3 ) < 0 <-> ( -u ( 1 / 3 ) x. E ) < ( 0 x. E ) ) ) |
139 |
130 132 51 53 138
|
syl112anc |
|- ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) < 0 <-> ( -u ( 1 / 3 ) x. E ) < ( 0 x. E ) ) ) |
140 |
137 139
|
mpbii |
|- ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) < ( 0 x. E ) ) |
141 |
|
mul02lem2 |
|- ( E e. RR -> ( 0 x. E ) = 0 ) |
142 |
51 141
|
syl |
|- ( ( ph /\ t e. T ) -> ( 0 x. E ) = 0 ) |
143 |
140 142
|
breqtrd |
|- ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) < 0 ) |
144 |
131 132 58 143 10
|
ltletrd |
|- ( ( ph /\ t e. T ) -> ( -u ( 1 / 3 ) x. E ) < ( F ` t ) ) |
145 |
131 58
|
ltnled |
|- ( ( ph /\ t e. T ) -> ( ( -u ( 1 / 3 ) x. E ) < ( F ` t ) <-> -. ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) ) |
146 |
144 145
|
mpbid |
|- ( ( ph /\ t e. T ) -> -. ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) |
147 |
|
nan |
|- ( ( ph -> -. ( t e. T /\ ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) ) <-> ( ( ph /\ t e. T ) -> -. ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) ) |
148 |
146 147
|
mpbir |
|- ( ph -> -. ( t e. T /\ ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) ) |
149 |
|
rabid |
|- ( t e. { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) ) |
150 |
148 149
|
sylnibr |
|- ( ph -> -. t e. { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } ) |
151 |
|
oveq1 |
|- ( j = 0 -> ( j - ( 1 / 3 ) ) = ( 0 - ( 1 / 3 ) ) ) |
152 |
|
df-neg |
|- -u ( 1 / 3 ) = ( 0 - ( 1 / 3 ) ) |
153 |
151 152
|
eqtr4di |
|- ( j = 0 -> ( j - ( 1 / 3 ) ) = -u ( 1 / 3 ) ) |
154 |
153
|
oveq1d |
|- ( j = 0 -> ( ( j - ( 1 / 3 ) ) x. E ) = ( -u ( 1 / 3 ) x. E ) ) |
155 |
154
|
breq2d |
|- ( j = 0 -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) ) ) |
156 |
155
|
rabbidv |
|- ( j = 0 -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } ) |
157 |
7
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
158 |
|
elnn0uz |
|- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) ) |
159 |
157 158
|
sylib |
|- ( ph -> N e. ( ZZ>= ` 0 ) ) |
160 |
|
eluzfz1 |
|- ( N e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... N ) ) |
161 |
159 160
|
syl |
|- ( ph -> 0 e. ( 0 ... N ) ) |
162 |
|
rabexg |
|- ( T e. _V -> { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } e. _V ) |
163 |
8 162
|
syl |
|- ( ph -> { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } e. _V ) |
164 |
4 156 161 163
|
fvmptd3 |
|- ( ph -> ( D ` 0 ) = { t e. T | ( F ` t ) <_ ( -u ( 1 / 3 ) x. E ) } ) |
165 |
150 164
|
neleqtrrd |
|- ( ph -> -. t e. ( D ` 0 ) ) |
166 |
3 165
|
alrimi |
|- ( ph -> A. t -. t e. ( D ` 0 ) ) |
167 |
|
nfcv |
|- F/_ t ( 0 ... N ) |
168 |
|
nfrab1 |
|- F/_ t { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } |
169 |
167 168
|
nfmpt |
|- F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) |
170 |
4 169
|
nfcxfr |
|- F/_ t D |
171 |
|
nfcv |
|- F/_ t 0 |
172 |
170 171
|
nffv |
|- F/_ t ( D ` 0 ) |
173 |
172
|
eq0f |
|- ( ( D ` 0 ) = (/) <-> A. t -. t e. ( D ` 0 ) ) |
174 |
166 173
|
sylibr |
|- ( ph -> ( D ` 0 ) = (/) ) |
175 |
126 174
|
sylan9eqr |
|- ( ( ph /\ j = 1 ) -> ( D ` ( j - 1 ) ) = (/) ) |
176 |
175
|
eleq2d |
|- ( ( ph /\ j = 1 ) -> ( t e. ( D ` ( j - 1 ) ) <-> t e. (/) ) ) |
177 |
122 176
|
mtbiri |
|- ( ( ph /\ j = 1 ) -> -. t e. ( D ` ( j - 1 ) ) ) |
178 |
177
|
ex |
|- ( ph -> ( j = 1 -> -. t e. ( D ` ( j - 1 ) ) ) ) |
179 |
178
|
con2d |
|- ( ph -> ( t e. ( D ` ( j - 1 ) ) -> -. j = 1 ) ) |
180 |
121 120 179
|
sylc |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> -. j = 1 ) |
181 |
|
simplll |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ -. j = 1 ) -> ph ) |
182 |
114 116
|
bitrdi |
|- ( ( ph /\ t e. T ) -> ( j e. ( J ` t ) <-> ( j e. ( 1 ... N ) /\ t e. ( D ` j ) ) ) ) |
183 |
182
|
simprbda |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> j e. ( 1 ... N ) ) |
184 |
7 32
|
eleqtrdi |
|- ( ph -> N e. ( ZZ>= ` 1 ) ) |
185 |
184
|
adantr |
|- ( ( ph /\ j e. ( J ` t ) ) -> N e. ( ZZ>= ` 1 ) ) |
186 |
|
elfzp12 |
|- ( N e. ( ZZ>= ` 1 ) -> ( j e. ( 1 ... N ) <-> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) ) ) |
187 |
185 186
|
syl |
|- ( ( ph /\ j e. ( J ` t ) ) -> ( j e. ( 1 ... N ) <-> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) ) ) |
188 |
187
|
adantlr |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( j e. ( 1 ... N ) <-> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) ) ) |
189 |
183 188
|
mpbid |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( j = 1 \/ j e. ( ( 1 + 1 ) ... N ) ) ) |
190 |
189
|
orcanai |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ -. j = 1 ) -> j e. ( ( 1 + 1 ) ... N ) ) |
191 |
|
fzssp1 |
|- ( 1 ... ( N - 1 ) ) C_ ( 1 ... ( ( N - 1 ) + 1 ) ) |
192 |
7
|
nncnd |
|- ( ph -> N e. CC ) |
193 |
|
1cnd |
|- ( ph -> 1 e. CC ) |
194 |
192 193
|
npcand |
|- ( ph -> ( ( N - 1 ) + 1 ) = N ) |
195 |
194
|
oveq2d |
|- ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) ) |
196 |
191 195
|
sseqtrid |
|- ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) ) |
197 |
196
|
adantr |
|- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) ) |
198 |
|
simpr |
|- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> j e. ( ( 1 + 1 ) ... N ) ) |
199 |
|
1z |
|- 1 e. ZZ |
200 |
|
zaddcl |
|- ( ( 1 e. ZZ /\ 1 e. ZZ ) -> ( 1 + 1 ) e. ZZ ) |
201 |
199 199 200
|
mp2an |
|- ( 1 + 1 ) e. ZZ |
202 |
201
|
a1i |
|- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( 1 + 1 ) e. ZZ ) |
203 |
7
|
nnzd |
|- ( ph -> N e. ZZ ) |
204 |
203
|
adantr |
|- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> N e. ZZ ) |
205 |
|
elfzelz |
|- ( j e. ( ( 1 + 1 ) ... N ) -> j e. ZZ ) |
206 |
205
|
adantl |
|- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> j e. ZZ ) |
207 |
|
1zzd |
|- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> 1 e. ZZ ) |
208 |
|
fzsubel |
|- ( ( ( ( 1 + 1 ) e. ZZ /\ N e. ZZ ) /\ ( j e. ZZ /\ 1 e. ZZ ) ) -> ( j e. ( ( 1 + 1 ) ... N ) <-> ( j - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) ) |
209 |
202 204 206 207 208
|
syl22anc |
|- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j e. ( ( 1 + 1 ) ... N ) <-> ( j - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) ) |
210 |
198 209
|
mpbid |
|- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) |
211 |
|
ax-1cn |
|- 1 e. CC |
212 |
211 211
|
pncan3oi |
|- ( ( 1 + 1 ) - 1 ) = 1 |
213 |
212
|
oveq1i |
|- ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) = ( 1 ... ( N - 1 ) ) |
214 |
210 213
|
eleqtrdi |
|- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j - 1 ) e. ( 1 ... ( N - 1 ) ) ) |
215 |
197 214
|
sseldd |
|- ( ( ph /\ j e. ( ( 1 + 1 ) ... N ) ) -> ( j - 1 ) e. ( 1 ... N ) ) |
216 |
181 190 215
|
syl2anc |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ -. j = 1 ) -> ( j - 1 ) e. ( 1 ... N ) ) |
217 |
216
|
ex |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( -. j = 1 -> ( j - 1 ) e. ( 1 ... N ) ) ) |
218 |
217
|
3adant3 |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( -. j = 1 -> ( j - 1 ) e. ( 1 ... N ) ) ) |
219 |
180 218
|
mpd |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. ( 1 ... N ) ) |
220 |
|
fveq2 |
|- ( i = ( j - 1 ) -> ( D ` i ) = ( D ` ( j - 1 ) ) ) |
221 |
220
|
eleq2d |
|- ( i = ( j - 1 ) -> ( t e. ( D ` i ) <-> t e. ( D ` ( j - 1 ) ) ) ) |
222 |
221
|
elrab3 |
|- ( ( j - 1 ) e. ( 1 ... N ) -> ( ( j - 1 ) e. { i e. ( 1 ... N ) | t e. ( D ` i ) } <-> t e. ( D ` ( j - 1 ) ) ) ) |
223 |
219 222
|
syl |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( ( j - 1 ) e. { i e. ( 1 ... N ) | t e. ( D ` i ) } <-> t e. ( D ` ( j - 1 ) ) ) ) |
224 |
120 223
|
mpbird |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. { i e. ( 1 ... N ) | t e. ( D ` i ) } ) |
225 |
|
nfcv |
|- F/_ i ( 1 ... N ) |
226 |
|
nfv |
|- F/ i t e. ( D ` j ) |
227 |
|
nfcv |
|- F/_ j i |
228 |
86 227
|
nffv |
|- F/_ j ( D ` i ) |
229 |
228
|
nfcri |
|- F/ j t e. ( D ` i ) |
230 |
|
fveq2 |
|- ( j = i -> ( D ` j ) = ( D ` i ) ) |
231 |
230
|
eleq2d |
|- ( j = i -> ( t e. ( D ` j ) <-> t e. ( D ` i ) ) ) |
232 |
84 225 226 229 231
|
cbvrabw |
|- { j e. ( 1 ... N ) | t e. ( D ` j ) } = { i e. ( 1 ... N ) | t e. ( D ` i ) } |
233 |
224 232
|
eleqtrrdi |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. { j e. ( 1 ... N ) | t e. ( D ` j ) } ) |
234 |
23
|
3ad2ant1 |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( J ` t ) = { j e. ( 1 ... N ) | t e. ( D ` j ) } ) |
235 |
233 234
|
eleqtrrd |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> ( j - 1 ) e. ( J ` t ) ) |
236 |
|
elfzelz |
|- ( j e. ( 1 ... N ) -> j e. ZZ ) |
237 |
|
zre |
|- ( j e. ZZ -> j e. RR ) |
238 |
183 236 237
|
3syl |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> j e. RR ) |
239 |
238
|
3adant3 |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> j e. RR ) |
240 |
|
peano2rem |
|- ( j e. RR -> ( j - 1 ) e. RR ) |
241 |
|
ltm1 |
|- ( j e. RR -> ( j - 1 ) < j ) |
242 |
241
|
adantr |
|- ( ( j e. RR /\ ( j - 1 ) e. RR ) -> ( j - 1 ) < j ) |
243 |
|
ltnle |
|- ( ( ( j - 1 ) e. RR /\ j e. RR ) -> ( ( j - 1 ) < j <-> -. j <_ ( j - 1 ) ) ) |
244 |
243
|
ancoms |
|- ( ( j e. RR /\ ( j - 1 ) e. RR ) -> ( ( j - 1 ) < j <-> -. j <_ ( j - 1 ) ) ) |
245 |
242 244
|
mpbid |
|- ( ( j e. RR /\ ( j - 1 ) e. RR ) -> -. j <_ ( j - 1 ) ) |
246 |
239 240 245
|
syl2anc2 |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> -. j <_ ( j - 1 ) ) |
247 |
|
breq2 |
|- ( k = ( j - 1 ) -> ( j <_ k <-> j <_ ( j - 1 ) ) ) |
248 |
247
|
notbid |
|- ( k = ( j - 1 ) -> ( -. j <_ k <-> -. j <_ ( j - 1 ) ) ) |
249 |
248
|
rspcev |
|- ( ( ( j - 1 ) e. ( J ` t ) /\ -. j <_ ( j - 1 ) ) -> E. k e. ( J ` t ) -. j <_ k ) |
250 |
235 246 249
|
syl2anc |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> E. k e. ( J ` t ) -. j <_ k ) |
251 |
|
rexnal |
|- ( E. k e. ( J ` t ) -. j <_ k <-> -. A. k e. ( J ` t ) j <_ k ) |
252 |
250 251
|
sylib |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` ( j - 1 ) ) ) -> -. A. k e. ( J ` t ) j <_ k ) |
253 |
252
|
3expia |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( t e. ( D ` ( j - 1 ) ) -> -. A. k e. ( J ` t ) j <_ k ) ) |
254 |
253
|
con2d |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> ( A. k e. ( J ` t ) j <_ k -> -. t e. ( D ` ( j - 1 ) ) ) ) |
255 |
254
|
imp |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ A. k e. ( J ` t ) j <_ k ) -> -. t e. ( D ` ( j - 1 ) ) ) |
256 |
119 255
|
eldifd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ A. k e. ( J ` t ) j <_ k ) -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) |
257 |
256
|
exp31 |
|- ( ( ph /\ t e. T ) -> ( j e. ( J ` t ) -> ( A. k e. ( J ` t ) j <_ k -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) ) |
258 |
113 257
|
reximdai |
|- ( ( ph /\ t e. T ) -> ( E. j e. ( J ` t ) A. k e. ( J ` t ) j <_ k -> E. j e. ( J ` t ) t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) |
259 |
111 258
|
mpd |
|- ( ( ph /\ t e. T ) -> E. j e. ( J ` t ) t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) |
260 |
|
df-rex |
|- ( E. j e. ( J ` t ) t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) <-> E. j ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) |
261 |
259 260
|
sylib |
|- ( ( ph /\ t e. T ) -> E. j ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) |
262 |
|
simprl |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> j e. ( J ` t ) ) |
263 |
|
eldifn |
|- ( t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) -> -. t e. ( D ` ( j - 1 ) ) ) |
264 |
|
simplr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> t e. T ) |
265 |
|
simpll |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ph ) |
266 |
183
|
adantrr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> j e. ( 1 ... N ) ) |
267 |
|
simprr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. t e. ( D ` ( j - 1 ) ) ) |
268 |
|
oveq1 |
|- ( j = k -> ( j - ( 1 / 3 ) ) = ( k - ( 1 / 3 ) ) ) |
269 |
268
|
oveq1d |
|- ( j = k -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( k - ( 1 / 3 ) ) x. E ) ) |
270 |
269
|
breq2d |
|- ( j = k -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) ) ) |
271 |
270
|
rabbidv |
|- ( j = k -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } ) |
272 |
271
|
cbvmptv |
|- ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) = ( k e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } ) |
273 |
4 272
|
eqtri |
|- D = ( k e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } ) |
274 |
|
oveq1 |
|- ( k = ( j - 1 ) -> ( k - ( 1 / 3 ) ) = ( ( j - 1 ) - ( 1 / 3 ) ) ) |
275 |
274
|
oveq1d |
|- ( k = ( j - 1 ) -> ( ( k - ( 1 / 3 ) ) x. E ) = ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) ) |
276 |
275
|
breq2d |
|- ( k = ( j - 1 ) -> ( ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) ) ) |
277 |
276
|
rabbidv |
|- ( k = ( j - 1 ) -> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } ) |
278 |
|
fzssp1 |
|- ( 0 ... ( N - 1 ) ) C_ ( 0 ... ( ( N - 1 ) + 1 ) ) |
279 |
194
|
oveq2d |
|- ( ph -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) ) |
280 |
278 279
|
sseqtrid |
|- ( ph -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) ) |
281 |
280
|
adantr |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) ) |
282 |
|
simpr |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ( 1 ... N ) ) |
283 |
|
1zzd |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> 1 e. ZZ ) |
284 |
203
|
adantr |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> N e. ZZ ) |
285 |
236
|
adantl |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ZZ ) |
286 |
|
fzsubel |
|- ( ( ( 1 e. ZZ /\ N e. ZZ ) /\ ( j e. ZZ /\ 1 e. ZZ ) ) -> ( j e. ( 1 ... N ) <-> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) ) |
287 |
283 284 285 283 286
|
syl22anc |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( j e. ( 1 ... N ) <-> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) ) |
288 |
282 287
|
mpbid |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( ( 1 - 1 ) ... ( N - 1 ) ) ) |
289 |
124
|
a1i |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( 1 - 1 ) = 0 ) |
290 |
289
|
oveq1d |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( 1 - 1 ) ... ( N - 1 ) ) = ( 0 ... ( N - 1 ) ) ) |
291 |
288 290
|
eleqtrd |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( 0 ... ( N - 1 ) ) ) |
292 |
281 291
|
sseldd |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( 0 ... N ) ) |
293 |
8
|
adantr |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> T e. _V ) |
294 |
|
rabexg |
|- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V ) |
295 |
293 294
|
syl |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V ) |
296 |
273 277 292 295
|
fvmptd3 |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( D ` ( j - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } ) |
297 |
296
|
eleq2d |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( t e. ( D ` ( j - 1 ) ) <-> t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } ) ) |
298 |
297
|
notbid |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( -. t e. ( D ` ( j - 1 ) ) <-> -. t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } ) ) |
299 |
298
|
biimpa |
|- ( ( ( ph /\ j e. ( 1 ... N ) ) /\ -. t e. ( D ` ( j - 1 ) ) ) -> -. t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } ) |
300 |
265 266 267 299
|
syl21anc |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } ) |
301 |
|
rabid |
|- ( t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) ) ) |
302 |
238
|
adantrr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> j e. RR ) |
303 |
|
recn |
|- ( j e. RR -> j e. CC ) |
304 |
|
1cnd |
|- ( j e. RR -> 1 e. CC ) |
305 |
|
1re |
|- 1 e. RR |
306 |
305 36 37
|
3pm3.2i |
|- ( 1 e. RR /\ 3 e. RR /\ 3 =/= 0 ) |
307 |
|
redivcl |
|- ( ( 1 e. RR /\ 3 e. RR /\ 3 =/= 0 ) -> ( 1 / 3 ) e. RR ) |
308 |
|
recn |
|- ( ( 1 / 3 ) e. RR -> ( 1 / 3 ) e. CC ) |
309 |
306 307 308
|
mp2b |
|- ( 1 / 3 ) e. CC |
310 |
309
|
a1i |
|- ( j e. RR -> ( 1 / 3 ) e. CC ) |
311 |
303 304 310
|
subsub4d |
|- ( j e. RR -> ( ( j - 1 ) - ( 1 / 3 ) ) = ( j - ( 1 + ( 1 / 3 ) ) ) ) |
312 |
|
3cn |
|- 3 e. CC |
313 |
312 211 312 37
|
divdiri |
|- ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) ) |
314 |
|
3p1e4 |
|- ( 3 + 1 ) = 4 |
315 |
314
|
oveq1i |
|- ( ( 3 + 1 ) / 3 ) = ( 4 / 3 ) |
316 |
312 37
|
dividi |
|- ( 3 / 3 ) = 1 |
317 |
316
|
oveq1i |
|- ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) ) |
318 |
313 315 317
|
3eqtr3i |
|- ( 4 / 3 ) = ( 1 + ( 1 / 3 ) ) |
319 |
318
|
a1i |
|- ( j e. RR -> ( 4 / 3 ) = ( 1 + ( 1 / 3 ) ) ) |
320 |
319
|
oveq2d |
|- ( j e. RR -> ( j - ( 4 / 3 ) ) = ( j - ( 1 + ( 1 / 3 ) ) ) ) |
321 |
311 320
|
eqtr4d |
|- ( j e. RR -> ( ( j - 1 ) - ( 1 / 3 ) ) = ( j - ( 4 / 3 ) ) ) |
322 |
321
|
oveq1d |
|- ( j e. RR -> ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) = ( ( j - ( 4 / 3 ) ) x. E ) ) |
323 |
302 322
|
syl |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) = ( ( j - ( 4 / 3 ) ) x. E ) ) |
324 |
323
|
breq2d |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) ) |
325 |
324
|
anbi2d |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( ( t e. T /\ ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) ) ) |
326 |
301 325
|
syl5bb |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( t e. { t e. T | ( F ` t ) <_ ( ( ( j - 1 ) - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) ) ) |
327 |
300 326
|
mtbid |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. ( t e. T /\ ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) ) |
328 |
|
imnan |
|- ( ( t e. T -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) <-> -. ( t e. T /\ ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) ) |
329 |
327 328
|
sylibr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> ( t e. T -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) ) |
330 |
264 329
|
mpd |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ -. t e. ( D ` ( j - 1 ) ) ) ) -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) |
331 |
263 330
|
sylanr2 |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) |
332 |
238
|
adantrr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> j e. RR ) |
333 |
|
4re |
|- 4 e. RR |
334 |
333
|
a1i |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> 4 e. RR ) |
335 |
36
|
a1i |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> 3 e. RR ) |
336 |
37
|
a1i |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> 3 =/= 0 ) |
337 |
334 335 336
|
redivcld |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( 4 / 3 ) e. RR ) |
338 |
332 337
|
resubcld |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( j - ( 4 / 3 ) ) e. RR ) |
339 |
50
|
ad2antrr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> E e. RR ) |
340 |
|
remulcl |
|- ( ( ( j - ( 4 / 3 ) ) e. RR /\ E e. RR ) -> ( ( j - ( 4 / 3 ) ) x. E ) e. RR ) |
341 |
340
|
rexrd |
|- ( ( ( j - ( 4 / 3 ) ) e. RR /\ E e. RR ) -> ( ( j - ( 4 / 3 ) ) x. E ) e. RR* ) |
342 |
338 339 341
|
syl2anc |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) e. RR* ) |
343 |
58
|
rexrd |
|- ( ( ph /\ t e. T ) -> ( F ` t ) e. RR* ) |
344 |
343
|
adantr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( F ` t ) e. RR* ) |
345 |
|
xrltnle |
|- ( ( ( ( j - ( 4 / 3 ) ) x. E ) e. RR* /\ ( F ` t ) e. RR* ) -> ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) <-> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) ) |
346 |
342 344 345
|
syl2anc |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) <-> -. ( F ` t ) <_ ( ( j - ( 4 / 3 ) ) x. E ) ) ) |
347 |
331 346
|
mpbird |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) ) |
348 |
|
simpl |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ph /\ t e. T ) ) |
349 |
|
simprr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) |
350 |
349
|
eldifad |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> t e. ( D ` j ) ) |
351 |
|
simplll |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> ph ) |
352 |
183
|
adantr |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> j e. ( 1 ... N ) ) |
353 |
|
simpr |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> t e. ( D ` j ) ) |
354 |
|
oveq1 |
|- ( k = j -> ( k - ( 1 / 3 ) ) = ( j - ( 1 / 3 ) ) ) |
355 |
354
|
oveq1d |
|- ( k = j -> ( ( k - ( 1 / 3 ) ) x. E ) = ( ( j - ( 1 / 3 ) ) x. E ) ) |
356 |
355
|
breq2d |
|- ( k = j -> ( ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) ) |
357 |
356
|
rabbidv |
|- ( k = j -> { t e. T | ( F ` t ) <_ ( ( k - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) |
358 |
|
fz1ssfz0 |
|- ( 1 ... N ) C_ ( 0 ... N ) |
359 |
358
|
sseli |
|- ( j e. ( 1 ... N ) -> j e. ( 0 ... N ) ) |
360 |
359
|
adantl |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ( 0 ... N ) ) |
361 |
|
rabexg |
|- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } e. _V ) |
362 |
293 361
|
syl |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } e. _V ) |
363 |
273 357 360 362
|
fvmptd3 |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( D ` j ) = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) |
364 |
363
|
eleq2d |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( t e. ( D ` j ) <-> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) ) |
365 |
364
|
biimpa |
|- ( ( ( ph /\ j e. ( 1 ... N ) ) /\ t e. ( D ` j ) ) -> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) |
366 |
351 352 353 365
|
syl21anc |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) |
367 |
|
rabid |
|- ( t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) ) |
368 |
366 367
|
sylib |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) ) |
369 |
368
|
simprd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ t e. ( D ` j ) ) -> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) |
370 |
348 262 350 369
|
syl21anc |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) |
371 |
347 370
|
jca |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) ) |
372 |
7
|
ad2antrr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> N e. NN ) |
373 |
|
simplr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> t e. T ) |
374 |
183
|
adantrr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> j e. ( 1 ... N ) ) |
375 |
|
nfv |
|- F/ j i e. ( 0 ... N ) |
376 |
2 375
|
nfan |
|- F/ j ( ph /\ i e. ( 0 ... N ) ) |
377 |
|
nfv |
|- F/ j ( X ` i ) : T --> RR |
378 |
376 377
|
nfim |
|- F/ j ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR ) |
379 |
|
eleq1w |
|- ( j = i -> ( j e. ( 0 ... N ) <-> i e. ( 0 ... N ) ) ) |
380 |
379
|
anbi2d |
|- ( j = i -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ i e. ( 0 ... N ) ) ) ) |
381 |
|
fveq2 |
|- ( j = i -> ( X ` j ) = ( X ` i ) ) |
382 |
381
|
feq1d |
|- ( j = i -> ( ( X ` j ) : T --> RR <-> ( X ` i ) : T --> RR ) ) |
383 |
380 382
|
imbi12d |
|- ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( X ` j ) : T --> RR ) <-> ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR ) ) ) |
384 |
378 383 14
|
chvarfv |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR ) |
385 |
384
|
ad4ant14 |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR ) |
386 |
|
simplll |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ph ) |
387 |
|
simpr |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> i e. ( 0 ... N ) ) |
388 |
|
simpllr |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> t e. T ) |
389 |
2 375 112
|
nf3an |
|- F/ j ( ph /\ i e. ( 0 ... N ) /\ t e. T ) |
390 |
|
nfv |
|- F/ j ( ( X ` i ) ` t ) <_ 1 |
391 |
389 390
|
nfim |
|- F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` i ) ` t ) <_ 1 ) |
392 |
379
|
3anbi2d |
|- ( j = i -> ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) <-> ( ph /\ i e. ( 0 ... N ) /\ t e. T ) ) ) |
393 |
381
|
fveq1d |
|- ( j = i -> ( ( X ` j ) ` t ) = ( ( X ` i ) ` t ) ) |
394 |
393
|
breq1d |
|- ( j = i -> ( ( ( X ` j ) ` t ) <_ 1 <-> ( ( X ` i ) ` t ) <_ 1 ) ) |
395 |
392 394
|
imbi12d |
|- ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` j ) ` t ) <_ 1 ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` i ) ` t ) <_ 1 ) ) ) |
396 |
391 395 16
|
chvarfv |
|- ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` i ) ` t ) <_ 1 ) |
397 |
386 387 388 396
|
syl3anc |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` t ) <_ 1 ) |
398 |
|
simplll |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> ph ) |
399 |
|
0zd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 e. ZZ ) |
400 |
|
elfzel2 |
|- ( i e. ( j ... N ) -> N e. ZZ ) |
401 |
400
|
adantl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> N e. ZZ ) |
402 |
|
elfzelz |
|- ( i e. ( j ... N ) -> i e. ZZ ) |
403 |
402
|
adantl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i e. ZZ ) |
404 |
|
0red |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 e. RR ) |
405 |
|
elfzel1 |
|- ( i e. ( j ... N ) -> j e. ZZ ) |
406 |
405
|
zred |
|- ( i e. ( j ... N ) -> j e. RR ) |
407 |
406
|
adantl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> j e. RR ) |
408 |
402
|
zred |
|- ( i e. ( j ... N ) -> i e. RR ) |
409 |
408
|
adantl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i e. RR ) |
410 |
|
0red |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 0 e. RR ) |
411 |
|
1red |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 1 e. RR ) |
412 |
|
0le1 |
|- 0 <_ 1 |
413 |
412
|
a1i |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 0 <_ 1 ) |
414 |
|
elfzle1 |
|- ( j e. ( 1 ... N ) -> 1 <_ j ) |
415 |
183 414
|
syl |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 1 <_ j ) |
416 |
410 411 238 413 415
|
letrd |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) -> 0 <_ j ) |
417 |
416
|
adantr |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 <_ j ) |
418 |
|
elfzle1 |
|- ( i e. ( j ... N ) -> j <_ i ) |
419 |
418
|
adantl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> j <_ i ) |
420 |
404 407 409 417 419
|
letrd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> 0 <_ i ) |
421 |
|
elfzle2 |
|- ( i e. ( j ... N ) -> i <_ N ) |
422 |
421
|
adantl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i <_ N ) |
423 |
399 401 403 420 422
|
elfzd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) ) |
424 |
423
|
adantlrr |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) ) |
425 |
|
simpll |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> ( ph /\ t e. T ) ) |
426 |
|
simplrl |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> j e. ( J ` t ) ) |
427 |
|
simplrr |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) |
428 |
427
|
eldifad |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` j ) ) |
429 |
|
simpr |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> i e. ( j ... N ) ) |
430 |
|
simpl1 |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ph /\ t e. T ) ) |
431 |
430
|
simprd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. T ) |
432 |
430 58
|
syl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( F ` t ) e. RR ) |
433 |
406
|
adantl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j e. RR ) |
434 |
38
|
a1i |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( 1 / 3 ) e. RR ) |
435 |
433 434
|
resubcld |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( j - ( 1 / 3 ) ) e. RR ) |
436 |
|
simpl1l |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ph ) |
437 |
436 50
|
syl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> E e. RR ) |
438 |
435 437
|
remulcld |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ( j - ( 1 / 3 ) ) x. E ) e. RR ) |
439 |
408
|
adantl |
|- ( ( ph /\ i e. ( j ... N ) ) -> i e. RR ) |
440 |
38
|
a1i |
|- ( ( ph /\ i e. ( j ... N ) ) -> ( 1 / 3 ) e. RR ) |
441 |
439 440
|
resubcld |
|- ( ( ph /\ i e. ( j ... N ) ) -> ( i - ( 1 / 3 ) ) e. RR ) |
442 |
50
|
adantr |
|- ( ( ph /\ i e. ( j ... N ) ) -> E e. RR ) |
443 |
441 442
|
remulcld |
|- ( ( ph /\ i e. ( j ... N ) ) -> ( ( i - ( 1 / 3 ) ) x. E ) e. RR ) |
444 |
436 443
|
sylancom |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ( i - ( 1 / 3 ) ) x. E ) e. RR ) |
445 |
|
simpl3 |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` j ) ) |
446 |
|
simpl2 |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j e. ( J ` t ) ) |
447 |
430 446 183
|
syl2anc |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j e. ( 1 ... N ) ) |
448 |
436 447 363
|
syl2anc |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( D ` j ) = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) |
449 |
445 448
|
eleqtrd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) |
450 |
449 367
|
sylib |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) ) |
451 |
450
|
simprd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) |
452 |
408
|
adantl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> i e. RR ) |
453 |
418
|
adantl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> j <_ i ) |
454 |
433 452 434 453
|
lesub1dd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( j - ( 1 / 3 ) ) <_ ( i - ( 1 / 3 ) ) ) |
455 |
436 441
|
sylancom |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( i - ( 1 / 3 ) ) e. RR ) |
456 |
12
|
rpregt0d |
|- ( ph -> ( E e. RR /\ 0 < E ) ) |
457 |
436 456
|
syl |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( E e. RR /\ 0 < E ) ) |
458 |
|
lemul1 |
|- ( ( ( j - ( 1 / 3 ) ) e. RR /\ ( i - ( 1 / 3 ) ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( j - ( 1 / 3 ) ) <_ ( i - ( 1 / 3 ) ) <-> ( ( j - ( 1 / 3 ) ) x. E ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) ) |
459 |
435 455 457 458
|
syl3anc |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ( j - ( 1 / 3 ) ) <_ ( i - ( 1 / 3 ) ) <-> ( ( j - ( 1 / 3 ) ) x. E ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) ) |
460 |
454 459
|
mpbid |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( ( j - ( 1 / 3 ) ) x. E ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) |
461 |
432 438 444 451 460
|
letrd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) |
462 |
|
rabid |
|- ( t e. { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) ) |
463 |
431 461 462
|
sylanbrc |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } ) |
464 |
|
simpr |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> i e. ( j ... N ) ) |
465 |
|
0zd |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> 0 e. ZZ ) |
466 |
400
|
3ad2ant3 |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> N e. ZZ ) |
467 |
402
|
3ad2ant3 |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> i e. ZZ ) |
468 |
465 466 467
|
3jca |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ i e. ZZ ) ) |
469 |
420 422
|
jca |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) ) /\ i e. ( j ... N ) ) -> ( 0 <_ i /\ i <_ N ) ) |
470 |
469
|
3impa |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> ( 0 <_ i /\ i <_ N ) ) |
471 |
|
elfz2 |
|- ( i e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ i e. ZZ ) /\ ( 0 <_ i /\ i <_ N ) ) ) |
472 |
468 470 471
|
sylanbrc |
|- ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) ) |
473 |
430 446 464 472
|
syl3anc |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> i e. ( 0 ... N ) ) |
474 |
|
oveq1 |
|- ( j = i -> ( j - ( 1 / 3 ) ) = ( i - ( 1 / 3 ) ) ) |
475 |
474
|
oveq1d |
|- ( j = i -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( i - ( 1 / 3 ) ) x. E ) ) |
476 |
475
|
breq2d |
|- ( j = i -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) ) ) |
477 |
476
|
rabbidv |
|- ( j = i -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } ) |
478 |
|
simpr |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> i e. ( 0 ... N ) ) |
479 |
|
rabexg |
|- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } e. _V ) |
480 |
8 479
|
syl |
|- ( ph -> { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } e. _V ) |
481 |
480
|
adantr |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } e. _V ) |
482 |
4 477 478 481
|
fvmptd3 |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> ( D ` i ) = { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } ) |
483 |
436 473 482
|
syl2anc |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> ( D ` i ) = { t e. T | ( F ` t ) <_ ( ( i - ( 1 / 3 ) ) x. E ) } ) |
484 |
463 483
|
eleqtrrd |
|- ( ( ( ( ph /\ t e. T ) /\ j e. ( J ` t ) /\ t e. ( D ` j ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` i ) ) |
485 |
425 426 428 429 484
|
syl31anc |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> t e. ( D ` i ) ) |
486 |
2 375 229
|
nf3an |
|- F/ j ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) |
487 |
|
nfv |
|- F/ j ( ( X ` i ) ` t ) < ( E / N ) |
488 |
486 487
|
nfim |
|- F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) -> ( ( X ` i ) ` t ) < ( E / N ) ) |
489 |
379 231
|
3anbi23d |
|- ( j = i -> ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( D ` j ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) ) ) |
490 |
393
|
breq1d |
|- ( j = i -> ( ( ( X ` j ) ` t ) < ( E / N ) <-> ( ( X ` i ) ` t ) < ( E / N ) ) ) |
491 |
489 490
|
imbi12d |
|- ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( D ` j ) ) -> ( ( X ` j ) ` t ) < ( E / N ) ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) -> ( ( X ` i ) ` t ) < ( E / N ) ) ) ) |
492 |
488 491 17
|
chvarfv |
|- ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( D ` i ) ) -> ( ( X ` i ) ` t ) < ( E / N ) ) |
493 |
398 424 485 492
|
syl3anc |
|- ( ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) /\ i e. ( j ... N ) ) -> ( ( X ` i ) ` t ) < ( E / N ) ) |
494 |
12
|
ad2antrr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> E e. RR+ ) |
495 |
13
|
ad2antrr |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> E < ( 1 / 3 ) ) |
496 |
372 373 374 385 397 493 494 495
|
stoweidlem11 |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) ) |
497 |
|
eleq1w |
|- ( l = j -> ( l e. ( J ` t ) <-> j e. ( J ` t ) ) ) |
498 |
|
fveq2 |
|- ( l = j -> ( D ` l ) = ( D ` j ) ) |
499 |
|
oveq1 |
|- ( l = j -> ( l - 1 ) = ( j - 1 ) ) |
500 |
499
|
fveq2d |
|- ( l = j -> ( D ` ( l - 1 ) ) = ( D ` ( j - 1 ) ) ) |
501 |
498 500
|
difeq12d |
|- ( l = j -> ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) = ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) |
502 |
501
|
eleq2d |
|- ( l = j -> ( t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) <-> t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) |
503 |
497 502
|
anbi12d |
|- ( l = j -> ( ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) <-> ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) ) |
504 |
503
|
anbi2d |
|- ( l = j -> ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) <-> ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) ) ) |
505 |
|
oveq1 |
|- ( l = j -> ( l - ( 4 / 3 ) ) = ( j - ( 4 / 3 ) ) ) |
506 |
505
|
oveq1d |
|- ( l = j -> ( ( l - ( 4 / 3 ) ) x. E ) = ( ( j - ( 4 / 3 ) ) x. E ) ) |
507 |
506
|
breq1d |
|- ( l = j -> ( ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) <-> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) |
508 |
504 507
|
imbi12d |
|- ( l = j -> ( ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) <-> ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) |
509 |
|
eleq1w |
|- ( s = t -> ( s e. T <-> t e. T ) ) |
510 |
509
|
anbi2d |
|- ( s = t -> ( ( ph /\ s e. T ) <-> ( ph /\ t e. T ) ) ) |
511 |
|
fveq2 |
|- ( s = t -> ( J ` s ) = ( J ` t ) ) |
512 |
511
|
eleq2d |
|- ( s = t -> ( l e. ( J ` s ) <-> l e. ( J ` t ) ) ) |
513 |
|
eleq1w |
|- ( s = t -> ( s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) <-> t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) |
514 |
512 513
|
anbi12d |
|- ( s = t -> ( ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) <-> ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) ) |
515 |
510 514
|
anbi12d |
|- ( s = t -> ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) <-> ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) ) ) |
516 |
|
fveq2 |
|- ( s = t -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` s ) = ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) |
517 |
516
|
breq2d |
|- ( s = t -> ( ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` s ) <-> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) |
518 |
515 517
|
imbi12d |
|- ( s = t -> ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` s ) ) <-> ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) |
519 |
|
nfv |
|- F/ j s e. T |
520 |
2 519
|
nfan |
|- F/ j ( ph /\ s e. T ) |
521 |
|
nfcv |
|- F/_ j s |
522 |
101 521
|
nffv |
|- F/_ j ( J ` s ) |
523 |
522
|
nfcri |
|- F/ j l e. ( J ` s ) |
524 |
|
nfcv |
|- F/_ j l |
525 |
86 524
|
nffv |
|- F/_ j ( D ` l ) |
526 |
|
nfcv |
|- F/_ j ( l - 1 ) |
527 |
86 526
|
nffv |
|- F/_ j ( D ` ( l - 1 ) ) |
528 |
525 527
|
nfdif |
|- F/_ j ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) |
529 |
528
|
nfcri |
|- F/ j s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) |
530 |
523 529
|
nfan |
|- F/ j ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) |
531 |
520 530
|
nfan |
|- F/ j ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) |
532 |
|
nfv |
|- F/ t s e. T |
533 |
3 532
|
nfan |
|- F/ t ( ph /\ s e. T ) |
534 |
|
nfmpt1 |
|- F/_ t ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } ) |
535 |
6 534
|
nfcxfr |
|- F/_ t J |
536 |
|
nfcv |
|- F/_ t s |
537 |
535 536
|
nffv |
|- F/_ t ( J ` s ) |
538 |
537
|
nfcri |
|- F/ t l e. ( J ` s ) |
539 |
|
nfcv |
|- F/_ t l |
540 |
170 539
|
nffv |
|- F/_ t ( D ` l ) |
541 |
|
nfcv |
|- F/_ t ( l - 1 ) |
542 |
170 541
|
nffv |
|- F/_ t ( D ` ( l - 1 ) ) |
543 |
540 542
|
nfdif |
|- F/_ t ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) |
544 |
543
|
nfcri |
|- F/ t s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) |
545 |
538 544
|
nfan |
|- F/ t ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) |
546 |
533 545
|
nfan |
|- F/ t ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) |
547 |
7
|
ad2antrr |
|- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> N e. NN ) |
548 |
8
|
ad2antrr |
|- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> T e. _V ) |
549 |
20
|
rabex |
|- { j e. ( 1 ... N ) | s e. ( D ` j ) } e. _V |
550 |
|
nfcv |
|- F/_ t j |
551 |
170 550
|
nffv |
|- F/_ t ( D ` j ) |
552 |
551
|
nfcri |
|- F/ t s e. ( D ` j ) |
553 |
|
nfcv |
|- F/_ t ( 1 ... N ) |
554 |
552 553
|
nfrabw |
|- F/_ t { j e. ( 1 ... N ) | s e. ( D ` j ) } |
555 |
|
eleq1w |
|- ( t = s -> ( t e. ( D ` j ) <-> s e. ( D ` j ) ) ) |
556 |
555
|
rabbidv |
|- ( t = s -> { j e. ( 1 ... N ) | t e. ( D ` j ) } = { j e. ( 1 ... N ) | s e. ( D ` j ) } ) |
557 |
536 554 556 6
|
fvmptf |
|- ( ( s e. T /\ { j e. ( 1 ... N ) | s e. ( D ` j ) } e. _V ) -> ( J ` s ) = { j e. ( 1 ... N ) | s e. ( D ` j ) } ) |
558 |
549 557
|
mpan2 |
|- ( s e. T -> ( J ` s ) = { j e. ( 1 ... N ) | s e. ( D ` j ) } ) |
559 |
558
|
eleq2d |
|- ( s e. T -> ( l e. ( J ` s ) <-> l e. { j e. ( 1 ... N ) | s e. ( D ` j ) } ) ) |
560 |
559
|
biimpa |
|- ( ( s e. T /\ l e. ( J ` s ) ) -> l e. { j e. ( 1 ... N ) | s e. ( D ` j ) } ) |
561 |
525
|
nfcri |
|- F/ j s e. ( D ` l ) |
562 |
|
fveq2 |
|- ( j = l -> ( D ` j ) = ( D ` l ) ) |
563 |
562
|
eleq2d |
|- ( j = l -> ( s e. ( D ` j ) <-> s e. ( D ` l ) ) ) |
564 |
524 84 561 563
|
elrabf |
|- ( l e. { j e. ( 1 ... N ) | s e. ( D ` j ) } <-> ( l e. ( 1 ... N ) /\ s e. ( D ` l ) ) ) |
565 |
560 564
|
sylib |
|- ( ( s e. T /\ l e. ( J ` s ) ) -> ( l e. ( 1 ... N ) /\ s e. ( D ` l ) ) ) |
566 |
565
|
simpld |
|- ( ( s e. T /\ l e. ( J ` s ) ) -> l e. ( 1 ... N ) ) |
567 |
566
|
ad2ant2lr |
|- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> l e. ( 1 ... N ) ) |
568 |
|
simprr |
|- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) |
569 |
9
|
ad2antrr |
|- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> F : T --> RR ) |
570 |
12
|
ad2antrr |
|- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> E e. RR+ ) |
571 |
13
|
ad2antrr |
|- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> E < ( 1 / 3 ) ) |
572 |
384
|
ad4ant14 |
|- ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR ) |
573 |
|
simp1ll |
|- ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) /\ t e. T ) -> ph ) |
574 |
|
nfv |
|- F/ j 0 <_ ( ( X ` i ) ` t ) |
575 |
389 574
|
nfim |
|- F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) ) |
576 |
393
|
breq2d |
|- ( j = i -> ( 0 <_ ( ( X ` j ) ` t ) <-> 0 <_ ( ( X ` i ) ` t ) ) ) |
577 |
392 576
|
imbi12d |
|- ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` j ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) ) ) ) |
578 |
575 577 15
|
chvarfv |
|- ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) ) |
579 |
573 578
|
syld3an1 |
|- ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) ) |
580 |
|
simp1ll |
|- ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ph ) |
581 |
|
nfmpt1 |
|- F/_ j ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } ) |
582 |
5 581
|
nfcxfr |
|- F/_ j B |
583 |
582 227
|
nffv |
|- F/_ j ( B ` i ) |
584 |
583
|
nfcri |
|- F/ j t e. ( B ` i ) |
585 |
2 375 584
|
nf3an |
|- F/ j ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) |
586 |
|
nfv |
|- F/ j ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) |
587 |
585 586
|
nfim |
|- F/ j ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) |
588 |
|
fveq2 |
|- ( j = i -> ( B ` j ) = ( B ` i ) ) |
589 |
588
|
eleq2d |
|- ( j = i -> ( t e. ( B ` j ) <-> t e. ( B ` i ) ) ) |
590 |
379 589
|
3anbi23d |
|- ( j = i -> ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( B ` j ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) ) ) |
591 |
393
|
breq2d |
|- ( j = i -> ( ( 1 - ( E / N ) ) < ( ( X ` j ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) ) |
592 |
590 591
|
imbi12d |
|- ( j = i -> ( ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( B ` j ) ) -> ( 1 - ( E / N ) ) < ( ( X ` j ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) ) ) |
593 |
587 592 18
|
chvarfv |
|- ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) |
594 |
580 593
|
syld3an1 |
|- ( ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) |
595 |
1 531 546 4 5 547 548 567 568 569 570 571 572 579 594
|
stoweidlem26 |
|- ( ( ( ph /\ s e. T ) /\ ( l e. ( J ` s ) /\ s e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` s ) ) |
596 |
518 595
|
vtoclg |
|- ( t e. T -> ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) |
597 |
596
|
ad2antlr |
|- ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) |
598 |
597
|
pm2.43i |
|- ( ( ( ph /\ t e. T ) /\ ( l e. ( J ` t ) /\ t e. ( ( D ` l ) \ ( D ` ( l - 1 ) ) ) ) ) -> ( ( l - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) |
599 |
508 598
|
vtoclg |
|- ( j e. ( J ` t ) -> ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) |
600 |
599
|
ad2antrl |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) |
601 |
600
|
pm2.43i |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) |
602 |
496 601
|
jca |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) |
603 |
262 371 602
|
3jca |
|- ( ( ( ph /\ t e. T ) /\ ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) ) -> ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) |
604 |
603
|
ex |
|- ( ( ph /\ t e. T ) -> ( ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) -> ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) ) |
605 |
113 604
|
eximd |
|- ( ( ph /\ t e. T ) -> ( E. j ( j e. ( J ` t ) /\ t e. ( ( D ` j ) \ ( D ` ( j - 1 ) ) ) ) -> E. j ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) ) |
606 |
261 605
|
mpd |
|- ( ( ph /\ t e. T ) -> E. j ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) |
607 |
|
3anass |
|- ( ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) <-> ( j e. ( J ` t ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) ) |
608 |
607
|
exbii |
|- ( E. j ( j e. ( J ` t ) /\ ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) <-> E. j ( j e. ( J ` t ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) ) |
609 |
606 608
|
sylib |
|- ( ( ph /\ t e. T ) -> E. j ( j e. ( J ` t ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) ) |
610 |
|
df-rex |
|- ( E. j e. ( J ` t ) ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) <-> E. j ( j e. ( J ` t ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) ) |
611 |
609 610
|
sylibr |
|- ( ( ph /\ t e. T ) -> E. j e. ( J ` t ) ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) |
612 |
|
nfcv |
|- F/_ j RR |
613 |
103 612
|
ssrexf |
|- ( ( J ` t ) C_ RR -> ( E. j e. ( J ` t ) ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) -> E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) ) |
614 |
30 611 613
|
sylc |
|- ( ( ph /\ t e. T ) -> E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) |
615 |
614
|
ex |
|- ( ph -> ( t e. T -> E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) ) |
616 |
3 615
|
ralrimi |
|- ( ph -> A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) ) |