Step |
Hyp |
Ref |
Expression |
1 |
|
stoweidlem26.1 |
|- F/_ t F |
2 |
|
stoweidlem26.2 |
|- F/ j ph |
3 |
|
stoweidlem26.3 |
|- F/ t ph |
4 |
|
stoweidlem26.4 |
|- D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) |
5 |
|
stoweidlem26.5 |
|- B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } ) |
6 |
|
stoweidlem26.6 |
|- ( ph -> N e. NN ) |
7 |
|
stoweidlem26.7 |
|- ( ph -> T e. _V ) |
8 |
|
stoweidlem26.8 |
|- ( ph -> L e. ( 1 ... N ) ) |
9 |
|
stoweidlem26.9 |
|- ( ph -> S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) ) |
10 |
|
stoweidlem26.10 |
|- ( ph -> F : T --> RR ) |
11 |
|
stoweidlem26.11 |
|- ( ph -> E e. RR+ ) |
12 |
|
stoweidlem26.12 |
|- ( ph -> E < ( 1 / 3 ) ) |
13 |
|
stoweidlem26.13 |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR ) |
14 |
|
stoweidlem26.14 |
|- ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) ) |
15 |
|
stoweidlem26.15 |
|- ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) |
16 |
|
1re |
|- 1 e. RR |
17 |
|
eleq1 |
|- ( L = 1 -> ( L e. RR <-> 1 e. RR ) ) |
18 |
16 17
|
mpbiri |
|- ( L = 1 -> L e. RR ) |
19 |
18
|
adantl |
|- ( ( ph /\ L = 1 ) -> L e. RR ) |
20 |
|
4re |
|- 4 e. RR |
21 |
20
|
a1i |
|- ( ( ph /\ L = 1 ) -> 4 e. RR ) |
22 |
|
3re |
|- 3 e. RR |
23 |
22
|
a1i |
|- ( ( ph /\ L = 1 ) -> 3 e. RR ) |
24 |
|
3ne0 |
|- 3 =/= 0 |
25 |
24
|
a1i |
|- ( ( ph /\ L = 1 ) -> 3 =/= 0 ) |
26 |
21 23 25
|
redivcld |
|- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR ) |
27 |
19 26
|
resubcld |
|- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR ) |
28 |
11
|
rpred |
|- ( ph -> E e. RR ) |
29 |
28
|
adantr |
|- ( ( ph /\ L = 1 ) -> E e. RR ) |
30 |
27 29
|
remulcld |
|- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR ) |
31 |
|
0red |
|- ( ( ph /\ L = 1 ) -> 0 e. RR ) |
32 |
|
fzfid |
|- ( ph -> ( 0 ... N ) e. Fin ) |
33 |
28
|
adantr |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> E e. RR ) |
34 |
|
eldif |
|- ( S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) <-> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) ) |
35 |
9 34
|
sylib |
|- ( ph -> ( S e. ( D ` L ) /\ -. S e. ( D ` ( L - 1 ) ) ) ) |
36 |
35
|
simpld |
|- ( ph -> S e. ( D ` L ) ) |
37 |
|
oveq1 |
|- ( j = L -> ( j - ( 1 / 3 ) ) = ( L - ( 1 / 3 ) ) ) |
38 |
37
|
oveq1d |
|- ( j = L -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( L - ( 1 / 3 ) ) x. E ) ) |
39 |
38
|
breq2d |
|- ( j = L -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) ) |
40 |
39
|
rabbidv |
|- ( j = L -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } ) |
41 |
|
fz1ssfz0 |
|- ( 1 ... N ) C_ ( 0 ... N ) |
42 |
41 8
|
sseldi |
|- ( ph -> L e. ( 0 ... N ) ) |
43 |
|
rabexg |
|- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V ) |
44 |
7 43
|
syl |
|- ( ph -> { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } e. _V ) |
45 |
4 40 42 44
|
fvmptd3 |
|- ( ph -> ( D ` L ) = { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } ) |
46 |
36 45
|
eleqtrd |
|- ( ph -> S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } ) |
47 |
|
nfcv |
|- F/_ t S |
48 |
|
nfcv |
|- F/_ t T |
49 |
1 47
|
nffv |
|- F/_ t ( F ` S ) |
50 |
|
nfcv |
|- F/_ t <_ |
51 |
|
nfcv |
|- F/_ t ( ( L - ( 1 / 3 ) ) x. E ) |
52 |
49 50 51
|
nfbr |
|- F/ t ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) |
53 |
|
fveq2 |
|- ( t = S -> ( F ` t ) = ( F ` S ) ) |
54 |
53
|
breq1d |
|- ( t = S -> ( ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) ) |
55 |
47 48 52 54
|
elrabf |
|- ( S e. { t e. T | ( F ` t ) <_ ( ( L - ( 1 / 3 ) ) x. E ) } <-> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) ) |
56 |
46 55
|
sylib |
|- ( ph -> ( S e. T /\ ( F ` S ) <_ ( ( L - ( 1 / 3 ) ) x. E ) ) ) |
57 |
56
|
simpld |
|- ( ph -> S e. T ) |
58 |
57
|
adantr |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> S e. T ) |
59 |
13 58
|
ffvelrnd |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. RR ) |
60 |
33 59
|
remulcld |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR ) |
61 |
32 60
|
fsumrecl |
|- ( ph -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) |
62 |
61
|
adantr |
|- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) |
63 |
20 22 24
|
redivcli |
|- ( 4 / 3 ) e. RR |
64 |
63
|
a1i |
|- ( ( ph /\ L = 1 ) -> ( 4 / 3 ) e. RR ) |
65 |
19 64
|
resubcld |
|- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) e. RR ) |
66 |
19
|
recnd |
|- ( ( ph /\ L = 1 ) -> L e. CC ) |
67 |
66
|
subid1d |
|- ( ( ph /\ L = 1 ) -> ( L - 0 ) = L ) |
68 |
|
3cn |
|- 3 e. CC |
69 |
68 24
|
dividi |
|- ( 3 / 3 ) = 1 |
70 |
|
3lt4 |
|- 3 < 4 |
71 |
|
3pos |
|- 0 < 3 |
72 |
22 20 22 71
|
ltdiv1ii |
|- ( 3 < 4 <-> ( 3 / 3 ) < ( 4 / 3 ) ) |
73 |
70 72
|
mpbi |
|- ( 3 / 3 ) < ( 4 / 3 ) |
74 |
69 73
|
eqbrtrri |
|- 1 < ( 4 / 3 ) |
75 |
|
breq1 |
|- ( L = 1 -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) ) |
76 |
75
|
adantl |
|- ( ( ph /\ L = 1 ) -> ( L < ( 4 / 3 ) <-> 1 < ( 4 / 3 ) ) ) |
77 |
74 76
|
mpbiri |
|- ( ( ph /\ L = 1 ) -> L < ( 4 / 3 ) ) |
78 |
67 77
|
eqbrtrd |
|- ( ( ph /\ L = 1 ) -> ( L - 0 ) < ( 4 / 3 ) ) |
79 |
19 31 64 78
|
ltsub23d |
|- ( ( ph /\ L = 1 ) -> ( L - ( 4 / 3 ) ) < 0 ) |
80 |
11
|
rpgt0d |
|- ( ph -> 0 < E ) |
81 |
80
|
adantr |
|- ( ( ph /\ L = 1 ) -> 0 < E ) |
82 |
|
mulltgt0 |
|- ( ( ( ( L - ( 4 / 3 ) ) e. RR /\ ( L - ( 4 / 3 ) ) < 0 ) /\ ( E e. RR /\ 0 < E ) ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 ) |
83 |
65 79 29 81 82
|
syl22anc |
|- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < 0 ) |
84 |
|
0cn |
|- 0 e. CC |
85 |
|
fsumconst |
|- ( ( ( 0 ... N ) e. Fin /\ 0 e. CC ) -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) ) |
86 |
32 84 85
|
sylancl |
|- ( ph -> sum_ i e. ( 0 ... N ) 0 = ( ( # ` ( 0 ... N ) ) x. 0 ) ) |
87 |
|
hashcl |
|- ( ( 0 ... N ) e. Fin -> ( # ` ( 0 ... N ) ) e. NN0 ) |
88 |
|
nn0cn |
|- ( ( # ` ( 0 ... N ) ) e. NN0 -> ( # ` ( 0 ... N ) ) e. CC ) |
89 |
32 87 88
|
3syl |
|- ( ph -> ( # ` ( 0 ... N ) ) e. CC ) |
90 |
89
|
mul01d |
|- ( ph -> ( ( # ` ( 0 ... N ) ) x. 0 ) = 0 ) |
91 |
86 90
|
eqtrd |
|- ( ph -> sum_ i e. ( 0 ... N ) 0 = 0 ) |
92 |
91
|
adantr |
|- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 = 0 ) |
93 |
|
0red |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 e. RR ) |
94 |
11
|
rpge0d |
|- ( ph -> 0 <_ E ) |
95 |
94
|
adantr |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ E ) |
96 |
|
nfv |
|- F/ t i e. ( 0 ... N ) |
97 |
3 96
|
nfan |
|- F/ t ( ph /\ i e. ( 0 ... N ) ) |
98 |
|
nfv |
|- F/ t 0 <_ ( ( X ` i ) ` S ) |
99 |
97 98
|
nfim |
|- F/ t ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) |
100 |
|
fveq2 |
|- ( t = S -> ( ( X ` i ) ` t ) = ( ( X ` i ) ` S ) ) |
101 |
100
|
breq2d |
|- ( t = S -> ( 0 <_ ( ( X ` i ) ` t ) <-> 0 <_ ( ( X ` i ) ` S ) ) ) |
102 |
101
|
imbi2d |
|- ( t = S -> ( ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) ) ) |
103 |
14
|
3expia |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> ( t e. T -> 0 <_ ( ( X ` i ) ` t ) ) ) |
104 |
103
|
com12 |
|- ( t e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` t ) ) ) |
105 |
47 99 102 104
|
vtoclgaf |
|- ( S e. T -> ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) ) |
106 |
58 105
|
mpcom |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) |
107 |
33 59 95 106
|
mulge0d |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) ) |
108 |
32 93 60 107
|
fsumle |
|- ( ph -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
109 |
108
|
adantr |
|- ( ( ph /\ L = 1 ) -> sum_ i e. ( 0 ... N ) 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
110 |
92 109
|
eqbrtrrd |
|- ( ( ph /\ L = 1 ) -> 0 <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
111 |
30 31 62 83 110
|
ltletrd |
|- ( ( ph /\ L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
112 |
|
elfzelz |
|- ( L e. ( 1 ... N ) -> L e. ZZ ) |
113 |
|
zre |
|- ( L e. ZZ -> L e. RR ) |
114 |
8 112 113
|
3syl |
|- ( ph -> L e. RR ) |
115 |
20
|
a1i |
|- ( ph -> 4 e. RR ) |
116 |
22
|
a1i |
|- ( ph -> 3 e. RR ) |
117 |
24
|
a1i |
|- ( ph -> 3 =/= 0 ) |
118 |
115 116 117
|
redivcld |
|- ( ph -> ( 4 / 3 ) e. RR ) |
119 |
114 118
|
resubcld |
|- ( ph -> ( L - ( 4 / 3 ) ) e. RR ) |
120 |
119 28
|
remulcld |
|- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR ) |
121 |
120
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) e. RR ) |
122 |
16
|
a1i |
|- ( ph -> 1 e. RR ) |
123 |
28 6
|
nndivred |
|- ( ph -> ( E / N ) e. RR ) |
124 |
122 123
|
resubcld |
|- ( ph -> ( 1 - ( E / N ) ) e. RR ) |
125 |
114 122
|
resubcld |
|- ( ph -> ( L - 1 ) e. RR ) |
126 |
124 125
|
remulcld |
|- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR ) |
127 |
28 126
|
remulcld |
|- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR ) |
128 |
127
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) e. RR ) |
129 |
|
fzfid |
|- ( ph -> ( 0 ... ( L - 2 ) ) e. Fin ) |
130 |
8
|
elfzelzd |
|- ( ph -> L e. ZZ ) |
131 |
|
2z |
|- 2 e. ZZ |
132 |
131
|
a1i |
|- ( ph -> 2 e. ZZ ) |
133 |
130 132
|
zsubcld |
|- ( ph -> ( L - 2 ) e. ZZ ) |
134 |
6
|
nnzd |
|- ( ph -> N e. ZZ ) |
135 |
130
|
zred |
|- ( ph -> L e. RR ) |
136 |
|
2re |
|- 2 e. RR |
137 |
136
|
a1i |
|- ( ph -> 2 e. RR ) |
138 |
135 137
|
resubcld |
|- ( ph -> ( L - 2 ) e. RR ) |
139 |
6
|
nnred |
|- ( ph -> N e. RR ) |
140 |
|
0le2 |
|- 0 <_ 2 |
141 |
|
0red |
|- ( ph -> 0 e. RR ) |
142 |
141 137 135
|
lesub2d |
|- ( ph -> ( 0 <_ 2 <-> ( L - 2 ) <_ ( L - 0 ) ) ) |
143 |
140 142
|
mpbii |
|- ( ph -> ( L - 2 ) <_ ( L - 0 ) ) |
144 |
130
|
zcnd |
|- ( ph -> L e. CC ) |
145 |
144
|
subid1d |
|- ( ph -> ( L - 0 ) = L ) |
146 |
143 145
|
breqtrd |
|- ( ph -> ( L - 2 ) <_ L ) |
147 |
|
elfzle2 |
|- ( L e. ( 1 ... N ) -> L <_ N ) |
148 |
8 147
|
syl |
|- ( ph -> L <_ N ) |
149 |
138 135 139 146 148
|
letrd |
|- ( ph -> ( L - 2 ) <_ N ) |
150 |
133 134 149
|
3jca |
|- ( ph -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) ) |
151 |
|
eluz2 |
|- ( N e. ( ZZ>= ` ( L - 2 ) ) <-> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) ) |
152 |
150 151
|
sylibr |
|- ( ph -> N e. ( ZZ>= ` ( L - 2 ) ) ) |
153 |
|
fzss2 |
|- ( N e. ( ZZ>= ` ( L - 2 ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) ) |
154 |
152 153
|
syl |
|- ( ph -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) ) |
155 |
154
|
sselda |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) ) |
156 |
155 59
|
syldan |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR ) |
157 |
129 156
|
fsumrecl |
|- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR ) |
158 |
28 157
|
remulcld |
|- ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR ) |
159 |
158
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR ) |
160 |
28 125
|
remulcld |
|- ( ph -> ( E x. ( L - 1 ) ) e. RR ) |
161 |
28 28
|
remulcld |
|- ( ph -> ( E x. E ) e. RR ) |
162 |
160 161
|
resubcld |
|- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) e. RR ) |
163 |
125 6
|
nndivred |
|- ( ph -> ( ( L - 1 ) / N ) e. RR ) |
164 |
161 163
|
remulcld |
|- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) e. RR ) |
165 |
160 164
|
resubcld |
|- ( ph -> ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) e. RR ) |
166 |
125 28
|
resubcld |
|- ( ph -> ( ( L - 1 ) - E ) e. RR ) |
167 |
122 28
|
readdcld |
|- ( ph -> ( 1 + E ) e. RR ) |
168 |
16 22 24
|
redivcli |
|- ( 1 / 3 ) e. RR |
169 |
168
|
a1i |
|- ( ph -> ( 1 / 3 ) e. RR ) |
170 |
28 169 122 12
|
ltadd2dd |
|- ( ph -> ( 1 + E ) < ( 1 + ( 1 / 3 ) ) ) |
171 |
|
ax-1cn |
|- 1 e. CC |
172 |
68 171 68 24
|
divdiri |
|- ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) ) |
173 |
|
3p1e4 |
|- ( 3 + 1 ) = 4 |
174 |
173
|
oveq1i |
|- ( ( 3 + 1 ) / 3 ) = ( 4 / 3 ) |
175 |
69
|
oveq1i |
|- ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) ) |
176 |
172 174 175
|
3eqtr3ri |
|- ( 1 + ( 1 / 3 ) ) = ( 4 / 3 ) |
177 |
170 176
|
breqtrdi |
|- ( ph -> ( 1 + E ) < ( 4 / 3 ) ) |
178 |
167 118 114 177
|
ltsub2dd |
|- ( ph -> ( L - ( 4 / 3 ) ) < ( L - ( 1 + E ) ) ) |
179 |
171
|
a1i |
|- ( ph -> 1 e. CC ) |
180 |
11
|
rpcnd |
|- ( ph -> E e. CC ) |
181 |
144 179 180
|
subsub4d |
|- ( ph -> ( ( L - 1 ) - E ) = ( L - ( 1 + E ) ) ) |
182 |
178 181
|
breqtrrd |
|- ( ph -> ( L - ( 4 / 3 ) ) < ( ( L - 1 ) - E ) ) |
183 |
119 166 11 182
|
ltmul1dd |
|- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( ( L - 1 ) - E ) x. E ) ) |
184 |
144 179
|
subcld |
|- ( ph -> ( L - 1 ) e. CC ) |
185 |
184 180
|
subcld |
|- ( ph -> ( ( L - 1 ) - E ) e. CC ) |
186 |
180 185
|
mulcomd |
|- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( ( L - 1 ) - E ) x. E ) ) |
187 |
180 184 180
|
subdid |
|- ( ph -> ( E x. ( ( L - 1 ) - E ) ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) ) |
188 |
186 187
|
eqtr3d |
|- ( ph -> ( ( ( L - 1 ) - E ) x. E ) = ( ( E x. ( L - 1 ) ) - ( E x. E ) ) ) |
189 |
183 188
|
breqtrd |
|- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( E x. E ) ) ) |
190 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
191 |
|
elfz |
|- ( ( L e. ZZ /\ 1 e. ZZ /\ N e. ZZ ) -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) ) |
192 |
130 190 134 191
|
syl3anc |
|- ( ph -> ( L e. ( 1 ... N ) <-> ( 1 <_ L /\ L <_ N ) ) ) |
193 |
8 192
|
mpbid |
|- ( ph -> ( 1 <_ L /\ L <_ N ) ) |
194 |
193
|
simprd |
|- ( ph -> L <_ N ) |
195 |
|
zlem1lt |
|- ( ( L e. ZZ /\ N e. ZZ ) -> ( L <_ N <-> ( L - 1 ) < N ) ) |
196 |
130 134 195
|
syl2anc |
|- ( ph -> ( L <_ N <-> ( L - 1 ) < N ) ) |
197 |
194 196
|
mpbid |
|- ( ph -> ( L - 1 ) < N ) |
198 |
6
|
nngt0d |
|- ( ph -> 0 < N ) |
199 |
|
ltdiv1 |
|- ( ( ( L - 1 ) e. RR /\ N e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) ) |
200 |
125 139 139 198 199
|
syl112anc |
|- ( ph -> ( ( L - 1 ) < N <-> ( ( L - 1 ) / N ) < ( N / N ) ) ) |
201 |
197 200
|
mpbid |
|- ( ph -> ( ( L - 1 ) / N ) < ( N / N ) ) |
202 |
6
|
nncnd |
|- ( ph -> N e. CC ) |
203 |
6
|
nnne0d |
|- ( ph -> N =/= 0 ) |
204 |
202 203
|
dividd |
|- ( ph -> ( N / N ) = 1 ) |
205 |
201 204
|
breqtrd |
|- ( ph -> ( ( L - 1 ) / N ) < 1 ) |
206 |
28 28 80 80
|
mulgt0d |
|- ( ph -> 0 < ( E x. E ) ) |
207 |
|
ltmul2 |
|- ( ( ( ( L - 1 ) / N ) e. RR /\ 1 e. RR /\ ( ( E x. E ) e. RR /\ 0 < ( E x. E ) ) ) -> ( ( ( L - 1 ) / N ) < 1 <-> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) ) ) |
208 |
163 122 161 206 207
|
syl112anc |
|- ( ph -> ( ( ( L - 1 ) / N ) < 1 <-> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) ) ) |
209 |
205 208
|
mpbid |
|- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( ( E x. E ) x. 1 ) ) |
210 |
180 180
|
mulcld |
|- ( ph -> ( E x. E ) e. CC ) |
211 |
210
|
mulid1d |
|- ( ph -> ( ( E x. E ) x. 1 ) = ( E x. E ) ) |
212 |
209 211
|
breqtrd |
|- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) < ( E x. E ) ) |
213 |
164 161 160 212
|
ltsub2dd |
|- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. E ) ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) ) |
214 |
120 162 165 189 213
|
lttrd |
|- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) ) |
215 |
180 202 203
|
divcld |
|- ( ph -> ( E / N ) e. CC ) |
216 |
179 215 184
|
subdird |
|- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) ) |
217 |
184
|
mulid2d |
|- ( ph -> ( 1 x. ( L - 1 ) ) = ( L - 1 ) ) |
218 |
217
|
oveq1d |
|- ( ph -> ( ( 1 x. ( L - 1 ) ) - ( ( E / N ) x. ( L - 1 ) ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) |
219 |
216 218
|
eqtrd |
|- ( ph -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) = ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) |
220 |
219
|
oveq2d |
|- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) ) |
221 |
215 184
|
mulcld |
|- ( ph -> ( ( E / N ) x. ( L - 1 ) ) e. CC ) |
222 |
180 184 221
|
subdid |
|- ( ph -> ( E x. ( ( L - 1 ) - ( ( E / N ) x. ( L - 1 ) ) ) ) = ( ( E x. ( L - 1 ) ) - ( E x. ( ( E / N ) x. ( L - 1 ) ) ) ) ) |
223 |
180 202 184 203
|
div32d |
|- ( ph -> ( ( E / N ) x. ( L - 1 ) ) = ( E x. ( ( L - 1 ) / N ) ) ) |
224 |
223
|
oveq2d |
|- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) ) |
225 |
184 202 203
|
divcld |
|- ( ph -> ( ( L - 1 ) / N ) e. CC ) |
226 |
180 180 225
|
mulassd |
|- ( ph -> ( ( E x. E ) x. ( ( L - 1 ) / N ) ) = ( E x. ( E x. ( ( L - 1 ) / N ) ) ) ) |
227 |
224 226
|
eqtr4d |
|- ( ph -> ( E x. ( ( E / N ) x. ( L - 1 ) ) ) = ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) |
228 |
227
|
oveq2d |
|- ( ph -> ( ( E x. ( L - 1 ) ) - ( E x. ( ( E / N ) x. ( L - 1 ) ) ) ) = ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) ) |
229 |
220 222 228
|
3eqtrd |
|- ( ph -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) = ( ( E x. ( L - 1 ) ) - ( ( E x. E ) x. ( ( L - 1 ) / N ) ) ) ) |
230 |
214 229
|
breqtrrd |
|- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) ) |
231 |
230
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) ) |
232 |
179 215
|
subcld |
|- ( ph -> ( 1 - ( E / N ) ) e. CC ) |
233 |
|
fsumconst |
|- ( ( ( 0 ... ( L - 2 ) ) e. Fin /\ ( 1 - ( E / N ) ) e. CC ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) ) |
234 |
129 232 233
|
syl2anc |
|- ( ph -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) ) |
235 |
234
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) ) |
236 |
|
0zd |
|- ( ( ph /\ -. L = 1 ) -> 0 e. ZZ ) |
237 |
8
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> L e. ( 1 ... N ) ) |
238 |
237
|
elfzelzd |
|- ( ( ph /\ -. L = 1 ) -> L e. ZZ ) |
239 |
131
|
a1i |
|- ( ( ph /\ -. L = 1 ) -> 2 e. ZZ ) |
240 |
238 239
|
zsubcld |
|- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ZZ ) |
241 |
|
elnnuz |
|- ( N e. NN <-> N e. ( ZZ>= ` 1 ) ) |
242 |
6 241
|
sylib |
|- ( ph -> N e. ( ZZ>= ` 1 ) ) |
243 |
|
elfzp12 |
|- ( N e. ( ZZ>= ` 1 ) -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) ) |
244 |
242 243
|
syl |
|- ( ph -> ( L e. ( 1 ... N ) <-> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) ) |
245 |
8 244
|
mpbid |
|- ( ph -> ( L = 1 \/ L e. ( ( 1 + 1 ) ... N ) ) ) |
246 |
245
|
orcanai |
|- ( ( ph /\ -. L = 1 ) -> L e. ( ( 1 + 1 ) ... N ) ) |
247 |
|
1p1e2 |
|- ( 1 + 1 ) = 2 |
248 |
247
|
a1i |
|- ( ( ph /\ -. L = 1 ) -> ( 1 + 1 ) = 2 ) |
249 |
248
|
oveq1d |
|- ( ( ph /\ -. L = 1 ) -> ( ( 1 + 1 ) ... N ) = ( 2 ... N ) ) |
250 |
246 249
|
eleqtrd |
|- ( ( ph /\ -. L = 1 ) -> L e. ( 2 ... N ) ) |
251 |
|
elfzle1 |
|- ( L e. ( 2 ... N ) -> 2 <_ L ) |
252 |
250 251
|
syl |
|- ( ( ph /\ -. L = 1 ) -> 2 <_ L ) |
253 |
114
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> L e. RR ) |
254 |
136
|
a1i |
|- ( ( ph /\ -. L = 1 ) -> 2 e. RR ) |
255 |
253 254
|
subge0d |
|- ( ( ph /\ -. L = 1 ) -> ( 0 <_ ( L - 2 ) <-> 2 <_ L ) ) |
256 |
252 255
|
mpbird |
|- ( ( ph /\ -. L = 1 ) -> 0 <_ ( L - 2 ) ) |
257 |
236 240 256
|
3jca |
|- ( ( ph /\ -. L = 1 ) -> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) ) |
258 |
|
eluz2 |
|- ( ( L - 2 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( L - 2 ) e. ZZ /\ 0 <_ ( L - 2 ) ) ) |
259 |
257 258
|
sylibr |
|- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( ZZ>= ` 0 ) ) |
260 |
|
hashfz |
|- ( ( L - 2 ) e. ( ZZ>= ` 0 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) ) |
261 |
259 260
|
syl |
|- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( ( ( L - 2 ) - 0 ) + 1 ) ) |
262 |
|
2cn |
|- 2 e. CC |
263 |
262
|
a1i |
|- ( ph -> 2 e. CC ) |
264 |
144 263
|
subcld |
|- ( ph -> ( L - 2 ) e. CC ) |
265 |
264
|
subid1d |
|- ( ph -> ( ( L - 2 ) - 0 ) = ( L - 2 ) ) |
266 |
265
|
oveq1d |
|- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( ( L - 2 ) + 1 ) ) |
267 |
144 263 179
|
subadd23d |
|- ( ph -> ( ( L - 2 ) + 1 ) = ( L + ( 1 - 2 ) ) ) |
268 |
262 171
|
negsubdi2i |
|- -u ( 2 - 1 ) = ( 1 - 2 ) |
269 |
|
2m1e1 |
|- ( 2 - 1 ) = 1 |
270 |
269
|
negeqi |
|- -u ( 2 - 1 ) = -u 1 |
271 |
268 270
|
eqtr3i |
|- ( 1 - 2 ) = -u 1 |
272 |
271
|
a1i |
|- ( ph -> ( 1 - 2 ) = -u 1 ) |
273 |
272
|
oveq2d |
|- ( ph -> ( L + ( 1 - 2 ) ) = ( L + -u 1 ) ) |
274 |
144 179
|
negsubd |
|- ( ph -> ( L + -u 1 ) = ( L - 1 ) ) |
275 |
273 274
|
eqtrd |
|- ( ph -> ( L + ( 1 - 2 ) ) = ( L - 1 ) ) |
276 |
266 267 275
|
3eqtrd |
|- ( ph -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) ) |
277 |
276
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( ( ( L - 2 ) - 0 ) + 1 ) = ( L - 1 ) ) |
278 |
261 277
|
eqtrd |
|- ( ( ph /\ -. L = 1 ) -> ( # ` ( 0 ... ( L - 2 ) ) ) = ( L - 1 ) ) |
279 |
278
|
oveq1d |
|- ( ( ph /\ -. L = 1 ) -> ( ( # ` ( 0 ... ( L - 2 ) ) ) x. ( 1 - ( E / N ) ) ) = ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) ) |
280 |
184 232
|
mulcomd |
|- ( ph -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) |
281 |
280
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) x. ( 1 - ( E / N ) ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) |
282 |
235 279 281
|
3eqtrd |
|- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) = ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) |
283 |
|
fzfid |
|- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) e. Fin ) |
284 |
|
fzn0 |
|- ( ( 0 ... ( L - 2 ) ) =/= (/) <-> ( L - 2 ) e. ( ZZ>= ` 0 ) ) |
285 |
259 284
|
sylibr |
|- ( ( ph /\ -. L = 1 ) -> ( 0 ... ( L - 2 ) ) =/= (/) ) |
286 |
124
|
ad2antrr |
|- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) e. RR ) |
287 |
|
simpll |
|- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ph ) |
288 |
155
|
adantlr |
|- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. ( 0 ... N ) ) |
289 |
287 288 59
|
syl2anc |
|- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. RR ) |
290 |
57
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. T ) |
291 |
|
elfzelz |
|- ( i e. ( 0 ... ( L - 2 ) ) -> i e. ZZ ) |
292 |
291
|
zred |
|- ( i e. ( 0 ... ( L - 2 ) ) -> i e. RR ) |
293 |
292
|
adantl |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i e. RR ) |
294 |
168
|
a1i |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 / 3 ) e. RR ) |
295 |
293 294
|
readdcld |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) e. RR ) |
296 |
28
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> E e. RR ) |
297 |
295 296
|
remulcld |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) e. RR ) |
298 |
114
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> L e. RR ) |
299 |
136
|
a1i |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> 2 e. RR ) |
300 |
298 299
|
resubcld |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR ) |
301 |
300 294
|
readdcld |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR ) |
302 |
301 296
|
remulcld |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR ) |
303 |
10 57
|
jca |
|- ( ph -> ( F : T --> RR /\ S e. T ) ) |
304 |
303
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F : T --> RR /\ S e. T ) ) |
305 |
|
ffvelrn |
|- ( ( F : T --> RR /\ S e. T ) -> ( F ` S ) e. RR ) |
306 |
304 305
|
syl |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( F ` S ) e. RR ) |
307 |
|
elfzle2 |
|- ( i e. ( 0 ... ( L - 2 ) ) -> i <_ ( L - 2 ) ) |
308 |
307
|
adantl |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> i <_ ( L - 2 ) ) |
309 |
293 300 294 308
|
leadd1dd |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) ) |
310 |
28 80
|
jca |
|- ( ph -> ( E e. RR /\ 0 < E ) ) |
311 |
310
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E e. RR /\ 0 < E ) ) |
312 |
|
lemul1 |
|- ( ( ( i + ( 1 / 3 ) ) e. RR /\ ( ( L - 2 ) + ( 1 / 3 ) ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) ) ) |
313 |
295 301 311 312
|
syl3anc |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) <_ ( ( L - 2 ) + ( 1 / 3 ) ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) ) ) |
314 |
309 313
|
mpbid |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) ) |
315 |
114 137
|
resubcld |
|- ( ph -> ( L - 2 ) e. RR ) |
316 |
315 169
|
readdcld |
|- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) e. RR ) |
317 |
316 28
|
remulcld |
|- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) e. RR ) |
318 |
10 57
|
ffvelrnd |
|- ( ph -> ( F ` S ) e. RR ) |
319 |
125 169
|
resubcld |
|- ( ph -> ( ( L - 1 ) - ( 1 / 3 ) ) e. RR ) |
320 |
319 28
|
remulcld |
|- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) e. RR ) |
321 |
|
addid1 |
|- ( 1 e. CC -> ( 1 + 0 ) = 1 ) |
322 |
321
|
eqcomd |
|- ( 1 e. CC -> 1 = ( 1 + 0 ) ) |
323 |
171 322
|
mp1i |
|- ( ph -> 1 = ( 1 + 0 ) ) |
324 |
179
|
subidd |
|- ( ph -> ( 1 - 1 ) = 0 ) |
325 |
324
|
eqcomd |
|- ( ph -> 0 = ( 1 - 1 ) ) |
326 |
325
|
oveq2d |
|- ( ph -> ( 1 + 0 ) = ( 1 + ( 1 - 1 ) ) ) |
327 |
|
addsubass |
|- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( 1 + 1 ) - 1 ) = ( 1 + ( 1 - 1 ) ) ) |
328 |
327
|
eqcomd |
|- ( ( 1 e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) ) |
329 |
179 179 179 328
|
syl3anc |
|- ( ph -> ( 1 + ( 1 - 1 ) ) = ( ( 1 + 1 ) - 1 ) ) |
330 |
323 326 329
|
3eqtrd |
|- ( ph -> 1 = ( ( 1 + 1 ) - 1 ) ) |
331 |
330
|
oveq2d |
|- ( ph -> ( L - 1 ) = ( L - ( ( 1 + 1 ) - 1 ) ) ) |
332 |
247
|
a1i |
|- ( ph -> ( 1 + 1 ) = 2 ) |
333 |
332
|
oveq1d |
|- ( ph -> ( ( 1 + 1 ) - 1 ) = ( 2 - 1 ) ) |
334 |
333
|
oveq2d |
|- ( ph -> ( L - ( ( 1 + 1 ) - 1 ) ) = ( L - ( 2 - 1 ) ) ) |
335 |
144 263 179
|
subsubd |
|- ( ph -> ( L - ( 2 - 1 ) ) = ( ( L - 2 ) + 1 ) ) |
336 |
331 334 335
|
3eqtrd |
|- ( ph -> ( L - 1 ) = ( ( L - 2 ) + 1 ) ) |
337 |
336
|
oveq1d |
|- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) ) |
338 |
262 68 24
|
divcli |
|- ( 2 / 3 ) e. CC |
339 |
338
|
a1i |
|- ( ph -> ( 2 / 3 ) e. CC ) |
340 |
264 179 339
|
addsubassd |
|- ( ph -> ( ( ( L - 2 ) + 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) ) |
341 |
171 68 24
|
divcli |
|- ( 1 / 3 ) e. CC |
342 |
|
df-3 |
|- 3 = ( 2 + 1 ) |
343 |
342
|
oveq1i |
|- ( 3 / 3 ) = ( ( 2 + 1 ) / 3 ) |
344 |
262 171 68 24
|
divdiri |
|- ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) ) |
345 |
343 69 344
|
3eqtr3ri |
|- ( ( 2 / 3 ) + ( 1 / 3 ) ) = 1 |
346 |
171 338 341 345
|
subaddrii |
|- ( 1 - ( 2 / 3 ) ) = ( 1 / 3 ) |
347 |
346
|
a1i |
|- ( ph -> ( 1 - ( 2 / 3 ) ) = ( 1 / 3 ) ) |
348 |
347
|
oveq2d |
|- ( ph -> ( ( L - 2 ) + ( 1 - ( 2 / 3 ) ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) ) |
349 |
337 340 348
|
3eqtrd |
|- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) = ( ( L - 2 ) + ( 1 / 3 ) ) ) |
350 |
136 22 24
|
redivcli |
|- ( 2 / 3 ) e. RR |
351 |
350
|
a1i |
|- ( ph -> ( 2 / 3 ) e. RR ) |
352 |
|
1lt2 |
|- 1 < 2 |
353 |
22 71
|
pm3.2i |
|- ( 3 e. RR /\ 0 < 3 ) |
354 |
16 136 353
|
3pm3.2i |
|- ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) |
355 |
|
ltdiv1 |
|- ( ( 1 e. RR /\ 2 e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) ) |
356 |
354 355
|
mp1i |
|- ( ph -> ( 1 < 2 <-> ( 1 / 3 ) < ( 2 / 3 ) ) ) |
357 |
352 356
|
mpbii |
|- ( ph -> ( 1 / 3 ) < ( 2 / 3 ) ) |
358 |
169 351 125 357
|
ltsub2dd |
|- ( ph -> ( ( L - 1 ) - ( 2 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) ) |
359 |
349 358
|
eqbrtrrd |
|- ( ph -> ( ( L - 2 ) + ( 1 / 3 ) ) < ( ( L - 1 ) - ( 1 / 3 ) ) ) |
360 |
316 319 11 359
|
ltmul1dd |
|- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) |
361 |
35
|
simprd |
|- ( ph -> -. S e. ( D ` ( L - 1 ) ) ) |
362 |
|
oveq1 |
|- ( j = ( L - 1 ) -> ( j - ( 1 / 3 ) ) = ( ( L - 1 ) - ( 1 / 3 ) ) ) |
363 |
362
|
oveq1d |
|- ( j = ( L - 1 ) -> ( ( j - ( 1 / 3 ) ) x. E ) = ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) |
364 |
363
|
breq2d |
|- ( j = ( L - 1 ) -> ( ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) <-> ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) |
365 |
364
|
rabbidv |
|- ( j = ( L - 1 ) -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } ) |
366 |
134
|
peano2zd |
|- ( ph -> ( N + 1 ) e. ZZ ) |
367 |
193
|
simpld |
|- ( ph -> 1 <_ L ) |
368 |
139 122
|
readdcld |
|- ( ph -> ( N + 1 ) e. RR ) |
369 |
139
|
lep1d |
|- ( ph -> N <_ ( N + 1 ) ) |
370 |
114 139 368 194 369
|
letrd |
|- ( ph -> L <_ ( N + 1 ) ) |
371 |
190 366 130 367 370
|
elfzd |
|- ( ph -> L e. ( 1 ... ( N + 1 ) ) ) |
372 |
144 179
|
npcand |
|- ( ph -> ( ( L - 1 ) + 1 ) = L ) |
373 |
|
0p1e1 |
|- ( 0 + 1 ) = 1 |
374 |
373
|
a1i |
|- ( ph -> ( 0 + 1 ) = 1 ) |
375 |
374
|
oveq1d |
|- ( ph -> ( ( 0 + 1 ) ... ( N + 1 ) ) = ( 1 ... ( N + 1 ) ) ) |
376 |
371 372 375
|
3eltr4d |
|- ( ph -> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) |
377 |
|
0zd |
|- ( ph -> 0 e. ZZ ) |
378 |
130 190
|
zsubcld |
|- ( ph -> ( L - 1 ) e. ZZ ) |
379 |
|
fzaddel |
|- ( ( ( 0 e. ZZ /\ N e. ZZ ) /\ ( ( L - 1 ) e. ZZ /\ 1 e. ZZ ) ) -> ( ( L - 1 ) e. ( 0 ... N ) <-> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) |
380 |
377 134 378 190 379
|
syl22anc |
|- ( ph -> ( ( L - 1 ) e. ( 0 ... N ) <-> ( ( L - 1 ) + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) |
381 |
376 380
|
mpbird |
|- ( ph -> ( L - 1 ) e. ( 0 ... N ) ) |
382 |
|
rabexg |
|- ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V ) |
383 |
7 382
|
syl |
|- ( ph -> { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } e. _V ) |
384 |
4 365 381 383
|
fvmptd3 |
|- ( ph -> ( D ` ( L - 1 ) ) = { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } ) |
385 |
361 384
|
neleqtrd |
|- ( ph -> -. S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } ) |
386 |
|
nfcv |
|- F/_ t ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) |
387 |
49 50 386
|
nfbr |
|- F/ t ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) |
388 |
53
|
breq1d |
|- ( t = S -> ( ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) <-> ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) |
389 |
47 48 387 388
|
elrabf |
|- ( S e. { t e. T | ( F ` t ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) } <-> ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) |
390 |
385 389
|
sylnib |
|- ( ph -> -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) |
391 |
|
ianor |
|- ( -. ( S e. T /\ ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) |
392 |
390 391
|
sylib |
|- ( ph -> ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) |
393 |
|
olc |
|- ( S e. T -> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) ) |
394 |
393
|
anim1i |
|- ( ( S e. T /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) ) |
395 |
57 392 394
|
syl2anc |
|- ( ph -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) ) |
396 |
|
orcom |
|- ( ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) <-> ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) ) |
397 |
396
|
anbi2i |
|- ( ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. S e. T \/ -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) <-> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) ) ) |
398 |
395 397
|
sylib |
|- ( ph -> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) ) ) |
399 |
|
pm4.43 |
|- ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) <-> ( ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ S e. T ) /\ ( -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) \/ -. S e. T ) ) ) |
400 |
398 399
|
sylibr |
|- ( ph -> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) |
401 |
320 318
|
ltnled |
|- ( ph -> ( ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) <-> -. ( F ` S ) <_ ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) ) ) |
402 |
400 401
|
mpbird |
|- ( ph -> ( ( ( L - 1 ) - ( 1 / 3 ) ) x. E ) < ( F ` S ) ) |
403 |
317 320 318 360 402
|
lttrd |
|- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) < ( F ` S ) ) |
404 |
317 318 403
|
ltled |
|- ( ph -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) |
405 |
404
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( ( L - 2 ) + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) |
406 |
297 302 306 314 405
|
letrd |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) |
407 |
|
nfcv |
|- F/_ t ( ( i + ( 1 / 3 ) ) x. E ) |
408 |
407 50 49
|
nfbr |
|- F/ t ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) |
409 |
53
|
breq2d |
|- ( t = S -> ( ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) ) |
410 |
47 48 408 409
|
elrabf |
|- ( S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } <-> ( S e. T /\ ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` S ) ) ) |
411 |
290 406 410
|
sylanbrc |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } ) |
412 |
|
oveq1 |
|- ( j = i -> ( j + ( 1 / 3 ) ) = ( i + ( 1 / 3 ) ) ) |
413 |
412
|
oveq1d |
|- ( j = i -> ( ( j + ( 1 / 3 ) ) x. E ) = ( ( i + ( 1 / 3 ) ) x. E ) ) |
414 |
413
|
breq1d |
|- ( j = i -> ( ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) <-> ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) ) ) |
415 |
414
|
rabbidv |
|- ( j = i -> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } ) |
416 |
|
rabexg |
|- ( T e. _V -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V ) |
417 |
7 416
|
syl |
|- ( ph -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V ) |
418 |
417
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V ) |
419 |
5 415 155 418
|
fvmptd3 |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( B ` i ) = { t e. T | ( ( i + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } ) |
420 |
411 419
|
eleqtrrd |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> S e. ( B ` i ) ) |
421 |
150
|
3ad2ant1 |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( ( L - 2 ) e. ZZ /\ N e. ZZ /\ ( L - 2 ) <_ N ) ) |
422 |
421 151
|
sylibr |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> N e. ( ZZ>= ` ( L - 2 ) ) ) |
423 |
422 153
|
syl |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 0 ... ( L - 2 ) ) C_ ( 0 ... N ) ) |
424 |
|
simp2 |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... ( L - 2 ) ) ) |
425 |
423 424
|
sseldd |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> i e. ( 0 ... N ) ) |
426 |
|
elex |
|- ( S e. ( B ` i ) -> S e. _V ) |
427 |
426
|
3ad2ant3 |
|- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> S e. _V ) |
428 |
|
nfcv |
|- F/_ t ( 0 ... N ) |
429 |
|
nfrab1 |
|- F/_ t { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } |
430 |
428 429
|
nfmpt |
|- F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } ) |
431 |
5 430
|
nfcxfr |
|- F/_ t B |
432 |
|
nfcv |
|- F/_ t i |
433 |
431 432
|
nffv |
|- F/_ t ( B ` i ) |
434 |
433
|
nfel2 |
|- F/ t S e. ( B ` i ) |
435 |
3 96 434
|
nf3an |
|- F/ t ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) |
436 |
|
nfv |
|- F/ t ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) |
437 |
435 436
|
nfim |
|- F/ t ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) |
438 |
|
eleq1 |
|- ( t = S -> ( t e. ( B ` i ) <-> S e. ( B ` i ) ) ) |
439 |
438
|
3anbi3d |
|- ( t = S -> ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) <-> ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) ) ) |
440 |
100
|
breq2d |
|- ( t = S -> ( ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) ) |
441 |
439 440
|
imbi12d |
|- ( t = S -> ( ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) ) <-> ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) ) ) |
442 |
437 441 15
|
vtoclg1f |
|- ( S e. _V -> ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) ) |
443 |
427 442
|
mpcom |
|- ( ( ph /\ i e. ( 0 ... N ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) |
444 |
425 443
|
syld3an2 |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) /\ S e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) |
445 |
420 444
|
mpd3an3 |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) |
446 |
445
|
adantlr |
|- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` S ) ) |
447 |
283 285 286 289 446
|
fsumlt |
|- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( 1 - ( E / N ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) |
448 |
282 447
|
eqbrtrrd |
|- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) |
449 |
126
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR ) |
450 |
157
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR ) |
451 |
310
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( E e. RR /\ 0 < E ) ) |
452 |
|
ltmul2 |
|- ( ( ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) e. RR /\ sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) <-> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) ) ) |
453 |
449 450 451 452
|
syl3anc |
|- ( ( ph /\ -. L = 1 ) -> ( ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) < sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) <-> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) ) ) |
454 |
448 453
|
mpbid |
|- ( ( ph /\ -. L = 1 ) -> ( E x. ( ( 1 - ( E / N ) ) x. ( L - 1 ) ) ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) ) |
455 |
121 128 159 231 454
|
lttrd |
|- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) ) |
456 |
155 60
|
syldan |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR ) |
457 |
456
|
adantlr |
|- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR ) |
458 |
457
|
recnd |
|- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC ) |
459 |
283 458
|
fsumcl |
|- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. CC ) |
460 |
459
|
addid1d |
|- ( ( ph /\ -. L = 1 ) -> ( sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) + 0 ) = sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) ) |
461 |
|
0red |
|- ( ( ph /\ -. L = 1 ) -> 0 e. RR ) |
462 |
|
fzfid |
|- ( ( ph /\ -. L = 1 ) -> ( ( L - 1 ) ... N ) e. Fin ) |
463 |
28
|
adantr |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. RR ) |
464 |
|
0zd |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. ZZ ) |
465 |
134
|
adantr |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> N e. ZZ ) |
466 |
|
elfzelz |
|- ( i e. ( ( L - 1 ) ... N ) -> i e. ZZ ) |
467 |
466
|
adantl |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ZZ ) |
468 |
|
0red |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 e. RR ) |
469 |
125
|
adantr |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. RR ) |
470 |
466
|
zred |
|- ( i e. ( ( L - 1 ) ... N ) -> i e. RR ) |
471 |
470
|
adantl |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. RR ) |
472 |
|
1m1e0 |
|- ( 1 - 1 ) = 0 |
473 |
122 114 122 367
|
lesub1dd |
|- ( ph -> ( 1 - 1 ) <_ ( L - 1 ) ) |
474 |
472 473
|
eqbrtrrid |
|- ( ph -> 0 <_ ( L - 1 ) ) |
475 |
474
|
adantr |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( L - 1 ) ) |
476 |
|
simpr |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( ( L - 1 ) ... N ) ) |
477 |
378
|
adantr |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) e. ZZ ) |
478 |
|
elfz |
|- ( ( i e. ZZ /\ ( L - 1 ) e. ZZ /\ N e. ZZ ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) ) |
479 |
467 477 465 478
|
syl3anc |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( i e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ i /\ i <_ N ) ) ) |
480 |
476 479
|
mpbid |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( L - 1 ) <_ i /\ i <_ N ) ) |
481 |
480
|
simpld |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( L - 1 ) <_ i ) |
482 |
468 469 471 475 481
|
letrd |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ i ) |
483 |
|
elfzle2 |
|- ( i e. ( ( L - 1 ) ... N ) -> i <_ N ) |
484 |
483
|
adantl |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i <_ N ) |
485 |
464 465 467 482 484
|
elfzd |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> i e. ( 0 ... N ) ) |
486 |
485 59
|
syldan |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( ( X ` i ) ` S ) e. RR ) |
487 |
463 486
|
remulcld |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR ) |
488 |
487
|
adantlr |
|- ( ( ( ph /\ -. L = 1 ) /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. RR ) |
489 |
462 488
|
fsumrecl |
|- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) |
490 |
283 457
|
fsumrecl |
|- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) |
491 |
|
fzfid |
|- ( ph -> ( ( L - 1 ) ... N ) e. Fin ) |
492 |
180
|
adantr |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> E e. CC ) |
493 |
492
|
mul01d |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) = 0 ) |
494 |
485 106
|
syldan |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( ( X ` i ) ` S ) ) |
495 |
310
|
adantr |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E e. RR /\ 0 < E ) ) |
496 |
|
lemul2 |
|- ( ( 0 e. RR /\ ( ( X ` i ) ` S ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( 0 <_ ( ( X ` i ) ` S ) <-> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) ) |
497 |
468 486 495 496
|
syl3anc |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( 0 <_ ( ( X ` i ) ` S ) <-> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) ) |
498 |
494 497
|
mpbid |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> ( E x. 0 ) <_ ( E x. ( ( X ` i ) ` S ) ) ) |
499 |
493 498
|
eqbrtrrd |
|- ( ( ph /\ i e. ( ( L - 1 ) ... N ) ) -> 0 <_ ( E x. ( ( X ` i ) ` S ) ) ) |
500 |
491 487 499
|
fsumge0 |
|- ( ph -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
501 |
500
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> 0 <_ sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
502 |
461 489 490 501
|
leadd2dd |
|- ( ( ph /\ -. L = 1 ) -> ( sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) + 0 ) <_ ( sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) + sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) ) ) |
503 |
460 502
|
eqbrtrrd |
|- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) <_ ( sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) + sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) ) ) |
504 |
156
|
recnd |
|- ( ( ph /\ i e. ( 0 ... ( L - 2 ) ) ) -> ( ( X ` i ) ` S ) e. CC ) |
505 |
129 180 504
|
fsummulc2 |
|- ( ph -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) = sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) ) |
506 |
505
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) = sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) ) |
507 |
|
elfzelz |
|- ( j e. ( 0 ... ( L - 2 ) ) -> j e. ZZ ) |
508 |
507
|
adantl |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ZZ ) |
509 |
508
|
zred |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. RR ) |
510 |
315
|
adantr |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. RR ) |
511 |
125
|
adantr |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. RR ) |
512 |
|
simpr |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j e. ( 0 ... ( L - 2 ) ) ) |
513 |
|
0zd |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> 0 e. ZZ ) |
514 |
133
|
adantr |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) e. ZZ ) |
515 |
|
elfz |
|- ( ( j e. ZZ /\ 0 e. ZZ /\ ( L - 2 ) e. ZZ ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) ) |
516 |
508 513 514 515
|
syl3anc |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( 0 ... ( L - 2 ) ) <-> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) ) |
517 |
512 516
|
mpbid |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( 0 <_ j /\ j <_ ( L - 2 ) ) ) |
518 |
517
|
simprd |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j <_ ( L - 2 ) ) |
519 |
122 137 114
|
ltsub2d |
|- ( ph -> ( 1 < 2 <-> ( L - 2 ) < ( L - 1 ) ) ) |
520 |
352 519
|
mpbii |
|- ( ph -> ( L - 2 ) < ( L - 1 ) ) |
521 |
520
|
adantr |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 2 ) < ( L - 1 ) ) |
522 |
509 510 511 518 521
|
lelttrd |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> j < ( L - 1 ) ) |
523 |
509 511
|
ltnled |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j < ( L - 1 ) <-> -. ( L - 1 ) <_ j ) ) |
524 |
522 523
|
mpbid |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. ( L - 1 ) <_ j ) |
525 |
524
|
intnanrd |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. ( ( L - 1 ) <_ j /\ j <_ N ) ) |
526 |
378
|
adantr |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( L - 1 ) e. ZZ ) |
527 |
134
|
adantr |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> N e. ZZ ) |
528 |
|
elfz |
|- ( ( j e. ZZ /\ ( L - 1 ) e. ZZ /\ N e. ZZ ) -> ( j e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ j /\ j <_ N ) ) ) |
529 |
508 526 527 528
|
syl3anc |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> ( j e. ( ( L - 1 ) ... N ) <-> ( ( L - 1 ) <_ j /\ j <_ N ) ) ) |
530 |
525 529
|
mtbird |
|- ( ( ph /\ j e. ( 0 ... ( L - 2 ) ) ) -> -. j e. ( ( L - 1 ) ... N ) ) |
531 |
530
|
ex |
|- ( ph -> ( j e. ( 0 ... ( L - 2 ) ) -> -. j e. ( ( L - 1 ) ... N ) ) ) |
532 |
2 531
|
ralrimi |
|- ( ph -> A. j e. ( 0 ... ( L - 2 ) ) -. j e. ( ( L - 1 ) ... N ) ) |
533 |
|
disj |
|- ( ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) <-> A. j e. ( 0 ... ( L - 2 ) ) -. j e. ( ( L - 1 ) ... N ) ) |
534 |
532 533
|
sylibr |
|- ( ph -> ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) ) |
535 |
534
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( ( 0 ... ( L - 2 ) ) i^i ( ( L - 1 ) ... N ) ) = (/) ) |
536 |
149
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) <_ N ) |
537 |
133 377 134
|
3jca |
|- ( ph -> ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) ) |
538 |
537
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) ) |
539 |
|
elfz |
|- ( ( ( L - 2 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( ( L - 2 ) e. ( 0 ... N ) <-> ( 0 <_ ( L - 2 ) /\ ( L - 2 ) <_ N ) ) ) |
540 |
538 539
|
syl |
|- ( ( ph /\ -. L = 1 ) -> ( ( L - 2 ) e. ( 0 ... N ) <-> ( 0 <_ ( L - 2 ) /\ ( L - 2 ) <_ N ) ) ) |
541 |
256 536 540
|
mpbir2and |
|- ( ( ph /\ -. L = 1 ) -> ( L - 2 ) e. ( 0 ... N ) ) |
542 |
|
fzsplit |
|- ( ( L - 2 ) e. ( 0 ... N ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) ) |
543 |
541 542
|
syl |
|- ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) ) |
544 |
267 273 274
|
3eqtrd |
|- ( ph -> ( ( L - 2 ) + 1 ) = ( L - 1 ) ) |
545 |
544
|
oveq1d |
|- ( ph -> ( ( ( L - 2 ) + 1 ) ... N ) = ( ( L - 1 ) ... N ) ) |
546 |
545
|
uneq2d |
|- ( ph -> ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) ) |
547 |
546
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( ( 0 ... ( L - 2 ) ) u. ( ( ( L - 2 ) + 1 ) ... N ) ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) ) |
548 |
543 547
|
eqtrd |
|- ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) = ( ( 0 ... ( L - 2 ) ) u. ( ( L - 1 ) ... N ) ) ) |
549 |
|
fzfid |
|- ( ( ph /\ -. L = 1 ) -> ( 0 ... N ) e. Fin ) |
550 |
180
|
adantr |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> E e. CC ) |
551 |
59
|
recnd |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` S ) e. CC ) |
552 |
550 551
|
mulcld |
|- ( ( ph /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC ) |
553 |
552
|
adantlr |
|- ( ( ( ph /\ -. L = 1 ) /\ i e. ( 0 ... N ) ) -> ( E x. ( ( X ` i ) ` S ) ) e. CC ) |
554 |
535 548 549 553
|
fsumsplit |
|- ( ( ph /\ -. L = 1 ) -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) = ( sum_ i e. ( 0 ... ( L - 2 ) ) ( E x. ( ( X ` i ) ` S ) ) + sum_ i e. ( ( L - 1 ) ... N ) ( E x. ( ( X ` i ) ` S ) ) ) ) |
555 |
503 506 554
|
3brtr4d |
|- ( ( ph /\ -. L = 1 ) -> ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
556 |
120 158 61
|
3jca |
|- ( ph -> ( ( ( L - ( 4 / 3 ) ) x. E ) e. RR /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) ) |
557 |
556
|
adantr |
|- ( ( ph /\ -. L = 1 ) -> ( ( ( L - ( 4 / 3 ) ) x. E ) e. RR /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) ) |
558 |
|
ltletr |
|- ( ( ( ( L - ( 4 / 3 ) ) x. E ) e. RR /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) e. RR /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. RR ) -> ( ( ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) ) |
559 |
557 558
|
syl |
|- ( ( ph /\ -. L = 1 ) -> ( ( ( ( L - ( 4 / 3 ) ) x. E ) < ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) /\ ( E x. sum_ i e. ( 0 ... ( L - 2 ) ) ( ( X ` i ) ` S ) ) <_ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) ) |
560 |
455 555 559
|
mp2and |
|- ( ( ph /\ -. L = 1 ) -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
561 |
111 560
|
pm2.61dan |
|- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
562 |
|
sumex |
|- sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. _V |
563 |
100
|
oveq2d |
|- ( t = S -> ( E x. ( ( X ` i ) ` t ) ) = ( E x. ( ( X ` i ) ` S ) ) ) |
564 |
563
|
sumeq2sdv |
|- ( t = S -> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
565 |
|
eqid |
|- ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) = ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) |
566 |
564 565
|
fvmptg |
|- ( ( S e. T /\ sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) e. _V ) -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
567 |
57 562 566
|
sylancl |
|- ( ph -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) = sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` S ) ) ) |
568 |
561 567
|
breqtrrd |
|- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) ) |