Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem20 Structured version   Visualization version   Unicode version

Theorem fourierdlem20 38101
 Description: Every interval in the partition is included in an interval of the partition . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem20.m
fourierdlem20.a
fourierdlem20.b
fourierdlem20.aleb
fourierdlem20.q
fourierdlem20.q0
fourierdlem20.qm
fourierdlem20.j ..^
fourierdlem20.t
fourierdlem20.s
fourierdlem20.i ..^
Assertion
Ref Expression
fourierdlem20 ..^
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,)   (,)   (,)   (,)   ()   (,)

Proof of Theorem fourierdlem20
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem20.i . . 3 ..^
2 ssrab2 3500 . . . 4 ..^ ..^
3 fzossfz 11965 . . . . . . . 8 ..^
4 fzssz 11827 . . . . . . . 8
53, 4sstri 3427 . . . . . . 7 ..^
62, 5sstri 3427 . . . . . 6 ..^
76a1i 11 . . . . 5 ..^
8 0z 10972 . . . . . . . . . 10
9 0le0 10721 . . . . . . . . . 10
10 eluz2 11188 . . . . . . . . . 10
118, 8, 9, 10mpbir3an 1212 . . . . . . . . 9
1211a1i 11 . . . . . . . 8
13 fourierdlem20.m . . . . . . . . 9
1413nnzd 11062 . . . . . . . 8
1513nngt0d 10675 . . . . . . . 8
16 elfzo2 11950 . . . . . . . 8 ..^
1712, 14, 15, 16syl3anbrc 1214 . . . . . . 7 ..^
18 fourierdlem20.q . . . . . . . . 9
193, 17sseldi 3416 . . . . . . . . 9
2018, 19ffvelrnd 6038 . . . . . . . 8
21 fourierdlem20.a . . . . . . . 8
22 fourierdlem20.t . . . . . . . . . . 11
2321rexrd 9708 . . . . . . . . . . . . . . 15
24 fourierdlem20.b . . . . . . . . . . . . . . . 16
2524rexrd 9708 . . . . . . . . . . . . . . 15
26 fourierdlem20.aleb . . . . . . . . . . . . . . 15
27 lbicc2 11774 . . . . . . . . . . . . . . 15
2823, 25, 26, 27syl3anc 1292 . . . . . . . . . . . . . 14
29 ubicc2 11775 . . . . . . . . . . . . . . 15
3023, 25, 26, 29syl3anc 1292 . . . . . . . . . . . . . 14
3128, 30jca 541 . . . . . . . . . . . . 13
32 prssg 4118 . . . . . . . . . . . . . 14
3323, 25, 32syl2anc 673 . . . . . . . . . . . . 13
3431, 33mpbid 215 . . . . . . . . . . . 12
35 inss2 3644 . . . . . . . . . . . . . 14
36 ioossicc 11745 . . . . . . . . . . . . . 14
3735, 36sstri 3427 . . . . . . . . . . . . 13
3837a1i 11 . . . . . . . . . . . 12
3934, 38unssd 3601 . . . . . . . . . . 11
4022, 39syl5eqss 3462 . . . . . . . . . 10
4121, 24iccssred 37698 . . . . . . . . . 10
4240, 41sstrd 3428 . . . . . . . . 9
43 fourierdlem20.s . . . . . . . . . . 11
44 isof1o 6234 . . . . . . . . . . 11
45 f1of 5828 . . . . . . . . . . 11
4643, 44, 453syl 18 . . . . . . . . . 10
47 fourierdlem20.j . . . . . . . . . . 11 ..^
48 elfzofz 11962 . . . . . . . . . . 11 ..^
4947, 48syl 17 . . . . . . . . . 10
5046, 49ffvelrnd 6038 . . . . . . . . 9
5142, 50sseldd 3419 . . . . . . . 8
52 fourierdlem20.q0 . . . . . . . 8
5340, 50sseldd 3419 . . . . . . . . 9
54 iccgelb 11716 . . . . . . . . 9
5523, 25, 53, 54syl3anc 1292 . . . . . . . 8
5620, 21, 51, 52, 55letrd 9809 . . . . . . 7
57 fveq2 5879 . . . . . . . . 9
5857breq1d 4405 . . . . . . . 8
5958elrab 3184 . . . . . . 7 ..^ ..^
6017, 56, 59sylanbrc 677 . . . . . 6 ..^
61 ne0i 3728 . . . . . 6 ..^ ..^
6260, 61syl 17 . . . . 5 ..^
6313nnred 10646 . . . . . 6
642sseli 3414 . . . . . . . . 9 ..^ ..^
65 elfzo0le 11987 . . . . . . . . 9 ..^
6664, 65syl 17 . . . . . . . 8 ..^
6766adantl 473 . . . . . . 7 ..^
6867ralrimiva 2809 . . . . . 6 ..^
69 breq2 4399 . . . . . . . 8
7069ralbidv 2829 . . . . . . 7 ..^ ..^
7170rspcev 3136 . . . . . 6 ..^ ..^
7263, 68, 71syl2anc 673 . . . . 5 ..^
73 suprzcl 11038 . . . . 5 ..^ ..^ ..^ ..^ ..^
747, 62, 72, 73syl3anc 1292 . . . 4 ..^ ..^
752, 74sseldi 3416 . . 3 ..^ ..^
761, 75syl5eqel 2553 . 2 ..^
773, 76sseldi 3416 . . . . 5
7818, 77ffvelrnd 6038 . . . 4
7978rexrd 9708 . . 3
80 fzofzp1 12037 . . . . . 6 ..^
8176, 80syl 17 . . . . 5
8218, 81ffvelrnd 6038 . . . 4
8382rexrd 9708 . . 3
841, 74syl5eqel 2553 . . . . 5 ..^
85 nfrab1 2957 . . . . . . . 8 ..^
86 nfcv 2612 . . . . . . . 8
87 nfcv 2612 . . . . . . . 8
8885, 86, 87nfsup 7983 . . . . . . 7 ..^
891, 88nfcxfr 2610 . . . . . 6
90 nfcv 2612 . . . . . 6 ..^
91 nfcv 2612 . . . . . . . 8
9291, 89nffv 5886 . . . . . . 7
93 nfcv 2612 . . . . . . 7
94 nfcv 2612 . . . . . . 7
9592, 93, 94nfbr 4440 . . . . . 6
96 fveq2 5879 . . . . . . 7
9796breq1d 4405 . . . . . 6
9889, 90, 95, 97elrabf 3182 . . . . 5 ..^ ..^
9984, 98sylib 201 . . . 4 ..^
10099simprd 470 . . 3
101 simpr 468 . . . . . 6
10283adantr 472 . . . . . . 7
103 iccssxr 11742 . . . . . . . . . 10
10440, 103syl6ss 3430 . . . . . . . . 9
105 fzofzp1 12037 . . . . . . . . . . 11 ..^
10647, 105syl 17 . . . . . . . . . 10
10746, 106ffvelrnd 6038 . . . . . . . . 9
108104, 107sseldd 3419 . . . . . . . 8
109108adantr 472 . . . . . . 7
110 xrltnle 9719 . . . . . . 7
111102, 109, 110syl2anc 673 . . . . . 6
112101, 111mpbird 240 . . . . 5
113 fzssz 11827 . . . . . 6
114 f1ofo 5835 . . . . . . . . . 10
11543, 44, 1143syl 18 . . . . . . . . 9
116115adantr 472 . . . . . . . 8
117 ffun 5742 . . . . . . . . . . . . . 14
11818, 117syl 17 . . . . . . . . . . . . 13
119 fdm 5745 . . . . . . . . . . . . . . . 16
12018, 119syl 17 . . . . . . . . . . . . . . 15
121120eqcomd 2477 . . . . . . . . . . . . . 14
12281, 121eleqtrd 2551 . . . . . . . . . . . . 13
123 fvelrn 6030 . . . . . . . . . . . . 13
124118, 122, 123syl2anc 673 . . . . . . . . . . . 12
125124adantr 472 . . . . . . . . . . 11
12623adantr 472 . . . . . . . . . . . 12
12725adantr 472 . . . . . . . . . . . 12
12882adantr 472 . . . . . . . . . . . 12
12941, 53sseldd 3419 . . . . . . . . . . . . . 14
1304sseli 3414 . . . . . . . . . . . . . . . . . . . 20
131 zre 10965 . . . . . . . . . . . . . . . . . . . 20
13277, 130, 1313syl 18 . . . . . . . . . . . . . . . . . . 19
133132adantr 472 . . . . . . . . . . . . . . . . . 18
134133ltp1d 10559 . . . . . . . . . . . . . . . . 17
135134adantlr 729 . . . . . . . . . . . . . . . 16
136 simplr 770 . . . . . . . . . . . . . . . . . 18
137129ad2antrr 740 . . . . . . . . . . . . . . . . . 18
138 simpr 468 . . . . . . . . . . . . . . . . . 18
139136, 137, 138nltled 9802 . . . . . . . . . . . . . . . . 17
140132adantr 472 . . . . . . . . . . . . . . . . . . . 20
141 1red 9676 . . . . . . . . . . . . . . . . . . . 20
142140, 141readdcld 9688 . . . . . . . . . . . . . . . . . . 19
143 elfzoelz 11947 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
144143zred 11063 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
145144ssriv 3422 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
1462, 145sstri 3427 . . . . . . . . . . . . . . . . . . . . . 22 ..^
147146a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ..^
14862adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ..^
14972adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ..^
15082adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
151129adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
15224adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
153 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25
15442, 107sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
155154adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
156 elfzoelz 11947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
157 zre 10965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
15847, 156, 1573syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159158ltp1d 10559 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
160 isorel 6235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
16143, 49, 106, 160syl12anc 1290 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
162159, 161mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
163162adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
16440, 107sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
165 iccleub 11715 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
16623, 25, 164, 165syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
167166adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
168151, 155, 152, 163, 167ltletrd 9812 . . . . . . . . . . . . . . . . . . . . . . . . 25
169150, 151, 152, 153, 168lelttrd 9810 . . . . . . . . . . . . . . . . . . . . . . . 24
170169adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
17124adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
17282adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
173 fourierdlem20.qm . . . . . . . . . . . . . . . . . . . . . . . . . . 27
174173adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
17514adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
17681adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
177 fzval3 12012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
17814, 177syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
179178adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
180176, 179eleqtrd 2551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ ..^
181 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ ..^
182180, 181jca 541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^ ..^
183 elfzonelfzo 12042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^ ..^
184175, 182, 183sylc 61 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^
185 fzval3 12012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
18614, 185syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
187186eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
188187adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^
189184, 188eleqtrd 2551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
190 elfz1eq 11836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
191189, 190syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
192191eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
193192fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
194174, 193breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
195171, 172, 194lensymd 9803 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
196195adantlr 729 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
197170, 196condan 811 . . . . . . . . . . . . . . . . . . . . . 22 ..^
198 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . 24
199 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . 24
20089, 198, 199nfov 6334 . . . . . . . . . . . . . . . . . . . . . . 23
20191, 200nffv 5886 . . . . . . . . . . . . . . . . . . . . . . . 24
202201, 93, 94nfbr 4440 . . . . . . . . . . . . . . . . . . . . . . 23
203 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24
204203breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . 23
205200, 90, 202, 204elrabf 3182 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
206197, 153, 205sylanbrc 677 . . . . . . . . . . . . . . . . . . . . 21 ..^
207 suprub 10592 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^ ..^ ..^ ..^
208147, 148, 149, 206, 207syl31anc 1295 . . . . . . . . . . . . . . . . . . . 20 ..^
209208, 1syl6breqr 4436 . . . . . . . . . . . . . . . . . . 19
210142, 140, 209lensymd 9803 . . . . . . . . . . . . . . . . . 18
211210adantlr 729 . . . . . . . . . . . . . . . . 17
212139, 211syldan 478 . . . . . . . . . . . . . . . 16
213135, 212condan 811 . . . . . . . . . . . . . . 15
21482, 213mpdan 681 . . . . . . . . . . . . . 14
21521, 129, 82, 55, 214lelttrd 9810 . . . . . . . . . . . . 13
216215adantr 472 . . . . . . . . . . . 12
217154adantr 472 . . . . . . . . . . . . 13
21824adantr 472 . . . . . . . . . . . . 13
219 simpr 468 . . . . . . . . . . . . 13
220166adantr 472 . . . . . . . . . . . . 13
221128, 217, 218, 219, 220ltletrd 9812 . . . . . . . . . . . 12
222126, 127, 128, 216, 221eliood 37691 . . . . . . . . . . 11
223125, 222elind 3609 . . . . . . . . . 10
224 elun2 3593 . . . . . . . . . 10
225223, 224syl 17 . . . . . . . . 9
226225, 22syl6eleqr 2560 . . . . . . . 8
227 foelrn 6056 . . . . . . . 8
228116, 226, 227syl2anc 673 . . . . . . 7
229214adantr 472 . . . . . . . . . . . . . 14
230 simpr 468 . . . . . . . . . . . . . 14
231229, 230breqtrd 4420 . . . . . . . . . . . . 13
232231adantlr 729 . . . . . . . . . . . 12
23343ad2antrr 740 . . . . . . . . . . . . 13
23449anim1i 578 . . . . . . . . . . . . . 14
235234adantr 472 . . . . . . . . . . . . 13
236 isorel 6235 . . . . . . . . . . . . 13
237233, 235, 236syl2anc 673 . . . . . . . . . . . 12
238232, 237mpbird 240 . . . . . . . . . . 11
239238adantllr 733 . . . . . . . . . 10
240 eqcom 2478 . . . . . . . . . . . . . . . 16
241240biimpi 199 . . . . . . . . . . . . . . 15
242241adantl 473 . . . . . . . . . . . . . 14
243 simpl 464 . . . . . . . . . . . . . 14
244242, 243eqbrtrd 4416 . . . . . . . . . . . . 13
245244adantll 728 . . . . . . . . . . . 12
246245adantlr 729 . . . . . . . . . . 11
24743ad2antrr 740 . . . . . . . . . . . . 13
248 simpr 468 . . . . . . . . . . . . 13
249106ad2antrr 740 . . . . . . . . . . . . 13
250 isorel 6235 . . . . . . . . . . . . 13
251247, 248, 249, 250syl12anc 1290 . . . . . . . . . . . 12
252251adantr 472 . . . . . . . . . . 11
253246, 252mpbird 240 . . . . . . . . . 10
254239, 253jca 541 . . . . . . . . 9
255254ex 441 . . . . . . . 8
256255reximdva 2858 . . . . . . 7
257228, 256mpd 15 . . . . . 6
258 ssrexv 3480 . . . . . 6
259113, 257, 258mpsyl 64 . . . . 5
260112, 259syldan 478 . . . 4
261 simplr 770 . . . . . . 7
26247, 156syl 17 . . . . . . . . 9
263262ad2antrr 740 . . . . . . . 8
264 simprl 772 . . . . . . . 8
265 simprr 774 . . . . . . . 8
266 btwnnz 11035 . . . . . . . 8
267263, 264, 265, 266syl3anc 1292 . . . . . . 7
268261, 267pm2.65da 586 . . . . . 6
269268nrexdv 2842 . . . . 5
270269adantr 472 . . . 4
271260, 270condan 811 . . 3
272 ioossioo 11751 . . 3
27379, 83, 100, 271, 272syl22anc 1293 . 2
274 fveq2 5879 . . . . 5
275 oveq1 6315 . . . . . 6
276275fveq2d 5883 . . . . 5
277274, 276oveq12d 6326 . . . 4
278277sseq2d 3446 . . 3
279278rspcev 3136 . 2 ..^ ..^
28076, 273, 279syl2anc 673 1 ..^
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376   wceq 1452   wcel 1904   wne 2641  wral 2756  wrex 2757  crab 2760   cun 3388   cin 3389   wss 3390  c0 3722  cpr 3961   class class class wbr 4395   cdm 4839   crn 4840   wfun 5583  wf 5585  wfo 5587  wf1o 5588  cfv 5589   wiso 5590  (class class class)co 6308  csup 7972  cr 9556  cc0 9557  c1 9558   caddc 9560  cxr 9692   clt 9693   cle 9694  cn 10631  cz 10961  cuz 11182  cioo 11660  cicc 11663  cfz 11810  ..^cfzo 11942 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-sup 7974  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-n0 10894  df-z 10962  df-uz 11183  df-ioo 11664  df-icc 11667  df-fz 11811  df-fzo 11943 This theorem is referenced by:  fourierdlem50  38132
 Copyright terms: Public domain W3C validator