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

Theorem fourierdlem50 38132
 Description: Continuity of and its limits with respect to the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem50.xre
fourierdlem50.p ..^
fourierdlem50.m
fourierdlem50.v
fourierdlem50.a
fourierdlem50.b
fourierdlem50.altb
fourierdlem50.ab
fourierdlem50.q
fourierdlem50.t
fourierdlem50.n
fourierdlem50.s
fourierdlem50.j ..^
fourierdlem50.u ..^
fourierdlem50.ch ..^ ..^
Assertion
Ref Expression
fourierdlem50 ..^
Distinct variable groups:   ,,   ,,   ,,,   ,   ,,   ,   ,,   ,   ,   ,,   ,   ,,   ,,   ,   ,,
Allowed substitution hints:   (,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,)   (,)   (,,,)   (,,,)   (,,)   ()   (,,,)   (,)   ()

Proof of Theorem fourierdlem50
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem50.u . . 3 ..^
2 fourierdlem50.m . . . . . . . 8
3 fourierdlem50.a . . . . . . . 8
4 fourierdlem50.b . . . . . . . 8
5 fourierdlem50.altb . . . . . . . . 9
63, 4, 5ltled 9800 . . . . . . . 8
7 fourierdlem50.p . . . . . . . . . . . . 13 ..^
8 fourierdlem50.v . . . . . . . . . . . . 13
97, 2, 8fourierdlem15 38096 . . . . . . . . . . . 12
10 pire 23492 . . . . . . . . . . . . . . . 16
1110renegcli 9955 . . . . . . . . . . . . . . 15
1211a1i 11 . . . . . . . . . . . . . 14
13 fourierdlem50.xre . . . . . . . . . . . . . 14
1412, 13readdcld 9688 . . . . . . . . . . . . 13
1510a1i 11 . . . . . . . . . . . . . 14
1615, 13readdcld 9688 . . . . . . . . . . . . 13
1714, 16iccssred 37698 . . . . . . . . . . . 12
189, 17fssd 5750 . . . . . . . . . . 11
1918ffvelrnda 6037 . . . . . . . . . 10
2013adantr 472 . . . . . . . . . 10
2119, 20resubcld 10068 . . . . . . . . 9
22 fourierdlem50.q . . . . . . . . 9
2321, 22fmptd 6061 . . . . . . . 8
2422a1i 11 . . . . . . . . . . 11
25 fveq2 5879 . . . . . . . . . . . . 13
2625oveq1d 6323 . . . . . . . . . . . 12
2726adantl 473 . . . . . . . . . . 11
28 nnssnn0 10896 . . . . . . . . . . . . . . 15
2928a1i 11 . . . . . . . . . . . . . 14
30 nn0uz 11217 . . . . . . . . . . . . . 14
3129, 30syl6sseq 3464 . . . . . . . . . . . . 13
3231, 2sseldd 3419 . . . . . . . . . . . 12
33 eluzfz1 11832 . . . . . . . . . . . 12
3432, 33syl 17 . . . . . . . . . . 11
3518, 34ffvelrnd 6038 . . . . . . . . . . . 12
3635, 13resubcld 10068 . . . . . . . . . . 11
3724, 27, 34, 36fvmptd 5969 . . . . . . . . . 10
387fourierdlem2 38083 . . . . . . . . . . . . . . . 16 ..^
392, 38syl 17 . . . . . . . . . . . . . . 15 ..^
408, 39mpbid 215 . . . . . . . . . . . . . 14 ..^
4140simprd 470 . . . . . . . . . . . . 13 ..^
4241simpld 466 . . . . . . . . . . . 12
4342simpld 466 . . . . . . . . . . 11
4443oveq1d 6323 . . . . . . . . . 10
4512recnd 9687 . . . . . . . . . . 11
4613recnd 9687 . . . . . . . . . . 11
4745, 46pncand 10006 . . . . . . . . . 10
4837, 44, 473eqtrd 2509 . . . . . . . . 9
4912rexrd 9708 . . . . . . . . . 10
5015rexrd 9708 . . . . . . . . . 10
51 fourierdlem50.ab . . . . . . . . . . 11
523leidd 10201 . . . . . . . . . . . 12
533, 4, 3, 52, 6eliccd 37697 . . . . . . . . . . 11
5451, 53sseldd 3419 . . . . . . . . . 10
55 iccgelb 11716 . . . . . . . . . 10
5649, 50, 54, 55syl3anc 1292 . . . . . . . . 9
5748, 56eqbrtrd 4416 . . . . . . . 8
584leidd 10201 . . . . . . . . . . . 12
593, 4, 4, 6, 58eliccd 37697 . . . . . . . . . . 11
6051, 59sseldd 3419 . . . . . . . . . 10
61 iccleub 11715 . . . . . . . . . 10
6249, 50, 60, 61syl3anc 1292 . . . . . . . . 9
63 fveq2 5879 . . . . . . . . . . . . 13
6463oveq1d 6323 . . . . . . . . . . . 12
6564adantl 473 . . . . . . . . . . 11
66 eluzfz2 11833 . . . . . . . . . . . 12
6732, 66syl 17 . . . . . . . . . . 11
6818, 67ffvelrnd 6038 . . . . . . . . . . . 12
6968, 13resubcld 10068 . . . . . . . . . . 11
7024, 65, 67, 69fvmptd 5969 . . . . . . . . . 10
7142simprd 470 . . . . . . . . . . 11
7271oveq1d 6323 . . . . . . . . . 10
7315recnd 9687 . . . . . . . . . . 11
7473, 46pncand 10006 . . . . . . . . . 10
7570, 72, 743eqtrrd 2510 . . . . . . . . 9
7662, 75breqtrd 4420 . . . . . . . 8
77 fourierdlem50.j . . . . . . . 8 ..^
78 fourierdlem50.t . . . . . . . 8
79 prfi 7864 . . . . . . . . . . . 12
8079a1i 11 . . . . . . . . . . 11
81 fzfid 12224 . . . . . . . . . . . . 13
8222rnmptfi 37508 . . . . . . . . . . . . 13
8381, 82syl 17 . . . . . . . . . . . 12
84 infi 7813 . . . . . . . . . . . 12
8583, 84syl 17 . . . . . . . . . . 11
86 unfi 7856 . . . . . . . . . . 11
8780, 85, 86syl2anc 673 . . . . . . . . . 10
8878, 87syl5eqel 2553 . . . . . . . . 9
893, 4jca 541 . . . . . . . . . . . 12
90 prssg 4118 . . . . . . . . . . . . 13
913, 4, 90syl2anc 673 . . . . . . . . . . . 12
9289, 91mpbid 215 . . . . . . . . . . 11
93 inss2 3644 . . . . . . . . . . . . 13
94 ioossre 11721 . . . . . . . . . . . . 13
9593, 94sstri 3427 . . . . . . . . . . . 12
9695a1i 11 . . . . . . . . . . 11
9792, 96unssd 3601 . . . . . . . . . 10
9878, 97syl5eqss 3462 . . . . . . . . 9
99 fourierdlem50.s . . . . . . . . 9
100 fourierdlem50.n . . . . . . . . 9
10188, 98, 99, 100fourierdlem36 38118 . . . . . . . 8
102 eqid 2471 . . . . . . . 8 ..^ ..^
1032, 3, 4, 6, 23, 57, 76, 77, 78, 101, 102fourierdlem20 38101 . . . . . . 7 ..^
104 fourierdlem50.ch . . . . . . . . . . . . 13 ..^ ..^
105104biimpi 199 . . . . . . . . . . . . . . . . . 18 ..^ ..^
106 simp-4l 784 . . . . . . . . . . . . . . . . . 18 ..^ ..^
107105, 106syl 17 . . . . . . . . . . . . . . . . 17
108 simplr 770 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^
109105, 108syl 17 . . . . . . . . . . . . . . . . 17 ..^
110107, 109jca 541 . . . . . . . . . . . . . . . 16 ..^
111 simp-4r 785 . . . . . . . . . . . . . . . . 17 ..^ ..^ ..^
112105, 111syl 17 . . . . . . . . . . . . . . . 16 ..^
113 elfzofz 11962 . . . . . . . . . . . . . . . . . . . . . 22 ..^
114113ad2antlr 741 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
115105, 114syl 17 . . . . . . . . . . . . . . . . . . . 20
116107, 18syl 17 . . . . . . . . . . . . . . . . . . . . . 22
117116, 115ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . 21
118107, 13syl 17 . . . . . . . . . . . . . . . . . . . . 21
119117, 118resubcld 10068 . . . . . . . . . . . . . . . . . . . 20
120 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22
121120oveq1d 6323 . . . . . . . . . . . . . . . . . . . . 21
122121, 22fvmptg 5961 . . . . . . . . . . . . . . . . . . . 20
123115, 119, 122syl2anc 673 . . . . . . . . . . . . . . . . . . 19
124123, 119eqeltrd 2549 . . . . . . . . . . . . . . . . . 18
12523adantr 472 . . . . . . . . . . . . . . . . . . . 20 ..^
126 fzofzp1 12037 . . . . . . . . . . . . . . . . . . . . 21 ..^
127126adantl 473 . . . . . . . . . . . . . . . . . . . 20 ..^
128125, 127ffvelrnd 6038 . . . . . . . . . . . . . . . . . . 19 ..^
129107, 112, 128syl2anc 673 . . . . . . . . . . . . . . . . . 18
130 isof1o 6234 . . . . . . . . . . . . . . . . . . . . . . . 24
131101, 130syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
132 f1of 5828 . . . . . . . . . . . . . . . . . . . . . . 23
133131, 132syl 17 . . . . . . . . . . . . . . . . . . . . . 22
134 fzofzp1 12037 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
13577, 134syl 17 . . . . . . . . . . . . . . . . . . . . . 22
136133, 135ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . 21
13798, 136sseldd 3419 . . . . . . . . . . . . . . . . . . . 20
138107, 137syl 17 . . . . . . . . . . . . . . . . . . 19
139 elfzofz 11962 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
14077, 139syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
141133, 140ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . 22
14298, 141sseldd 3419 . . . . . . . . . . . . . . . . . . . . 21
143107, 142syl 17 . . . . . . . . . . . . . . . . . . . 20
144105simprd 470 . . . . . . . . . . . . . . . . . . . . . 22
145124rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . 23
14623adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
147 fzofzp1 12037 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
148147adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
149146, 148ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
150149rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
151110, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
152143rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . 23
153138rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . 23
154 elfzoelz 11947 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
155154zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
156155ltp1d 10559 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
15777, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25
158 isoeq5 6232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
15978, 158ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
160101, 159sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . 26
161 isorel 6235 . . . . . . . . . . . . . . . . . . . . . . . . . 26
162160, 140, 135, 161syl12anc 1290 . . . . . . . . . . . . . . . . . . . . . . . . 25
163157, 162mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . 24
164107, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
165145, 151, 152, 153, 164ioossioobi 37714 . . . . . . . . . . . . . . . . . . . . . 22
166144, 165mpbid 215 . . . . . . . . . . . . . . . . . . . . 21
167166simpld 466 . . . . . . . . . . . . . . . . . . . 20
168124, 143, 138, 167, 164lelttrd 9810 . . . . . . . . . . . . . . . . . . 19
169 elfzofz 11962 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
170169ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
171170ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
172105, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
173107, 172, 21syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . 23
17422fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . 23
175172, 173, 174syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
176175, 173eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . 21
177 simpllr 777 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
178105, 177syl 17 . . . . . . . . . . . . . . . . . . . . 21
179176, 129, 143, 138, 164, 178fourierdlem10 38091 . . . . . . . . . . . . . . . . . . . 20
180179simprd 470 . . . . . . . . . . . . . . . . . . 19
181124, 138, 129, 168, 180ltletrd 9812 . . . . . . . . . . . . . . . . . 18
182124, 129, 118, 181ltadd2dd 9811 . . . . . . . . . . . . . . . . 17
183123oveq2d 6324 . . . . . . . . . . . . . . . . . 18
184107, 46syl 17 . . . . . . . . . . . . . . . . . . 19
185117recnd 9687 . . . . . . . . . . . . . . . . . . 19
186184, 185pncan3d 10008 . . . . . . . . . . . . . . . . . 18
187183, 186eqtr2d 2506 . . . . . . . . . . . . . . . . 17
188112, 126syl 17 . . . . . . . . . . . . . . . . . . . 20
18918adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
190189, 127ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
191107, 112, 190syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
192191, 118resubcld 10068 . . . . . . . . . . . . . . . . . . . . 21
193188, 192jca 541 . . . . . . . . . . . . . . . . . . . 20
194 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . 23
195 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25
196195oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . . 24
197196eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . 23
198194, 197anbi12d 725 . . . . . . . . . . . . . . . . . . . . . 22
199 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23
200199, 196eqeq12d 2486 . . . . . . . . . . . . . . . . . . . . . 22
201198, 200imbi12d 327 . . . . . . . . . . . . . . . . . . . . 21
202201, 122vtoclg 3093 . . . . . . . . . . . . . . . . . . . 20
203188, 193, 202sylc 61 . . . . . . . . . . . . . . . . . . 19
204203oveq2d 6324 . . . . . . . . . . . . . . . . . 18
205191recnd 9687 . . . . . . . . . . . . . . . . . . 19
206184, 205pncan3d 10008 . . . . . . . . . . . . . . . . . 18
207204, 206eqtr2d 2506 . . . . . . . . . . . . . . . . 17
208182, 187, 2073brtr4d 4426 . . . . . . . . . . . . . . . 16
209 eleq1 2537 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
210209anbi2d 718 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^ ..^
211 oveq1 6315 . . . . . . . . . . . . . . . . . . . . 21
212211fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20
213212breq2d 4407 . . . . . . . . . . . . . . . . . . 19
214210, 213anbi12d 725 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
215 fveq2 5879 . . . . . . . . . . . . . . . . . . 19
216215breq2d 4407 . . . . . . . . . . . . . . . . . 18
217214, 216imbi12d 327 . . . . . . . . . . . . . . . . 17 ..^ ..^ ..^ ..^
218 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
219218anbi2d 718 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
220219anbi1d 719 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^ ..^ ..^
221 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21
222221breq1d 4405 . . . . . . . . . . . . . . . . . . . 20
223220, 222anbi12d 725 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^ ..^
224221breq1d 4405 . . . . . . . . . . . . . . . . . . 19
225223, 224imbi12d 327 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
226 elfzoelz 11947 . . . . . . . . . . . . . . . . . . . . 21 ..^
227226ad3antlr 745 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
228 elfzoelz 11947 . . . . . . . . . . . . . . . . . . . . 21 ..^
229228ad2antlr 741 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
230 simplr 770 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
23118adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
232 fzofzp1 12037 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
233232adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
234231, 233ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
235234adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
236235adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
23718adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
238 elfzofz 11962 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
239238adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
240237, 239ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
241240ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
242228zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
243 peano2re 9824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
244242, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
245244ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
246226zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
247246ad3antlr 745 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
248 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
249245, 247, 248nltled 9802 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
250228peano2zd 11066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
251250ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
252226ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
253 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
254 eluz2 11188 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
255251, 252, 253, 254syl3anbrc 1214 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
256255adantlll 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
257 simplll 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
258 0zd 10973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ ..^
259 elfzoel2 11946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
260259ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ ..^
261 elfzelz 11826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
262261adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ ..^
263258, 260, 2623jca 1210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^
264 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
265261zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
266265adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
267242adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
268 elfzole1 11955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
269268adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
270267, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
271267ltp1d 10559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
272 elfzle1 11828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
273272adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
274267, 270, 266, 271, 273ltletrd 9812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
275264, 267, 266, 269, 274lelttrd 9810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
276264, 266, 275ltled 9800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
277276adantll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^
278265adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
279259zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
280279adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
281246adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
282 elfzle2 11829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
283282adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
284 elfzolt2 11956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
285284adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
286278, 281, 280, 283, 285lelttrd 9810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
287278, 280, 286ltled 9800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
288287adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^
289263, 277, 288jca32 544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^
290 elfz2 11817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
291289, 290sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
292291adantlll 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
293257, 292, 19syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
294293adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
295 simplll 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
296 0zd 10973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
297 elfzelz 11826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
298297adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
299 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
300298zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
301242adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
302268adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
303301, 243syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
304301ltp1d 10559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
305 elfzle1 11828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
306305adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
307301, 303, 300, 304, 306ltletrd 9812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
308299, 301, 300, 302, 307lelttrd 9810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
309299, 300, 308ltled 9800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
310 eluz2 11188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
311296, 298, 309, 310syl3anbrc 1214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
312311adantll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
313 elfzoel2 11946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
314313ad2antlr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
315297zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
316315adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
317 peano2rem 9961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
318246, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
319318adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
320279adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
321 elfzle2 11829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
322321adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
323246ltm1d 10561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
324318, 246, 279, 323, 284lttrd 9813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
325324adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
326316, 319, 320, 322, 325lelttrd 9810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
327326adantll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
328327adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
329 elfzo2 11950 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
330312, 314, 328, 329syl3anbrc 1214 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^ ..^
331169, 19sylan2 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
33241simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
333332r19.21bi 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
334331, 190, 333ltled 9800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
335295, 330, 334syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
336335adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
337256, 294, 336monoord 12281 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
338249, 337syldan 478 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
339236, 241, 338lensymd 9803 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
340339adantlr 729 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
341230, 340condan 811 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
342 zleltp1 11011 . . . . . . . . . . . . . . . . . . . . . 22
343227, 229, 342syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
344341, 343mpbird 240 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
345 eluz2 11188 . . . . . . . . . . . . . . . . . . . 20
346227, 229, 344, 345syl3anbrc 1214 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
34718ad3antrrr 744 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
348 0zd 10973 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
349259ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
350 elfzelz 11826 . . . . . . . . . . . . . . . . . . . . . . . . . 26
351350adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
352348, 349, 3513jca 1210 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
353 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
354246adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
355350zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
356355adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
357 elfzole1 11955 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
358357adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
359 elfzle1 11828 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
360359adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
361353, 354, 356, 358, 360letrd 9809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
362361adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
363355adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
364313zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
365364adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
366242adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
367 elfzle2 11829 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
368367adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
369 elfzolt2 11956 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
370369adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
371363, 366, 365, 368, 370lelttrd 9810 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^
372363, 365, 371ltled 9800 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
373372adantll 728 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
374352, 362, 373jca32 544 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
375374, 290sylibr 217 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
376375adantlll 732 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
377347, 376ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
378377adantlr 729 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
379 simp-4l 784 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
380 0zd 10973 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
381 elfzelz 11826 . . . . . . . . . . . . . . . . . . . . . . . . 25
382381adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
383 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
384246adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
385382zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
386357adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
387 elfzle1 11828 . . . . . . . . . . . . . . . . . . . . . . . . . 26
388387adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
389383, 384, 385, 386, 388letrd 9809 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
390380, 382, 389, 310syl3anbrc 1214 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
391390adantll 728 . . . . . . . . . . . . . . . . . . . . . 22 ..^
392391adant423 37430 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
393313ad3antlr 745 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
394381zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . 25
395394adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
396242adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
397364adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
398 elfzle2 11829 . . . . . . . . . . . . . . . . . . . . . . . . . 26
399398adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
400 zltlem1 11013 . . . . . . . . . . . . . . . . . . . . . . . . . 26
401381, 228, 400syl2anr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
402399, 401mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
403369adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ..^
404395, 396, 397, 402, 403lttrd 9813 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
405404adantll 728 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
406405adantlr 729 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
407392, 393, 406, 329syl3anbrc 1214 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^ ..^
408379, 407, 334syl2anc 673 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
409346, 378, 408monoord 12281 . . . . . . . . . . . . . . . . . 18 ..^ ..^
410225, 409chvarv 2120 . . . . . . . . . . . . . . . . 17 ..^ ..^
411217, 410chvarv 2120 . . . . . . . . . . . . . . . 16 ..^ ..^
412110, 112, 208, 411syl21anc 1291 . . . . . . . . . . . . . . 15
413107, 112jca 541 . . . . . . . . . . . . . . . 16 ..^
414110, 149syl 17 . . . . . . . . . . . . . . . . . 18
415179simpld 466 . . . . . . . . . . . . . . . . . . . 20
416176, 143, 138, 415, 164lelttrd 9810 . . . . . . . . . . . . . . . . . . 19
417166simprd 470 . . . . . . . . . . . . . . . . . . 19
418176, 138, 414, 416, 417ltletrd 9812 . . . . . . . . . . . . . . . . . 18
419176, 414, 118, 418ltadd2dd 9811 . . . . . . . . . . . . . . . . 17
420175oveq2d 6324 . . . . . . . . . . . . . . . . . 18
421107, 172, 19syl2anc 673 . . . . . . . . . . . . . . . . . . . 20
422421recnd 9687 . . . . . . . . . . . . . . . . . . 19
423184, 422pncan3d 10008 . . . . . . . . . . . . . . . . . 18
424420, 423eqtr2d 2506 . . . . . . . . . . . . . . . . 17
42522a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ..^
426 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23
427426oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . 22
428427adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ..^
42918adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
430429, 148ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . 22 ..^
43113adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ..^
432430, 431resubcld 10068 . . . . . . . . . . . . . . . . . . . . 21 ..^
433425, 428, 148, 432fvmptd 5969 . . . . . . . . . . . . . . . . . . . 20 ..^
434107, 109, 433syl2anc 673 . . . . . . . . . . . . . . . . . . 19
435434oveq2d 6324 . . . . . . . . . . . . . . . . . 18
436110, 430syl 17 . . . . . . . . . . . . . . . . . . . 20
437436recnd 9687 . . . . . . . . . . . . . . . . . . 19
438184, 437pncan3d 10008 . . . . . . . . . . . . . . . . . 18
439435, 438eqtr2d 2506 . . . . . . . . . . . . . . . . 17
440419, 424, 4393brtr4d 4426 . . . . . . . . . . . . . . . 16
441 eleq1 2537 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
442441anbi2d 718 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^ ..^
443 oveq1 6315 . . . . . . . . . . . . . . . . . . . . 21
444443fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20
445444breq2d 4407 . . . . . . . . . . . . . . . . . . 19
446442, 445anbi12d 725 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
447 fveq2 5879 . . . . . . . . . . . . . . . . . . 19
448447breq2d 4407 . . . . . . . . . . . . . . . . . 18
449446, 448imbi12d 327 . . . . . . . . . . . . . . . . 17 ..^ ..^ ..^ ..^
450 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
451450anbi2d 718 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
452451anbi1d 719 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^ ..^ ..^
453 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21
454453breq1d 4405 . . . . . . . . . . . . . . . . . . . 20
455452, 454anbi12d 725 . . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^ ..^
456453breq1d 4405 . . . . . . . . . . . . . . . . . . 19
457455, 456imbi12d 327 . . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
458457, 409chvarv 2120 . . . . . . . . . . . . . . . . 17 ..^ ..^
459449, 458chvarv 2120 . . . . . . . . . . . . . . . 16 ..^ ..^
460413, 109, 440, 459syl21anc 1291 . . . . . . . . . . . . . . 15
461117, 421letri3d 9794 . . . . . . . . . . . . . . 15
462412, 460, 461mpbir2and 936 . . . . . . . . . . . . . 14
4637, 2, 8fourierdlem34 38116 . . . . . . . . . . . . . . . 16
464107, 463syl 17 . . . . . . . . . . . . . . 15
465 f1fveq 6181 . . . . . . . . . . . . . . 15
466464, 115, 172, 465syl12anc 1290 . . . . . . . . . . . . . 14
467462, 466mpbid 215 . . . . . . . . . . . . 13
468104, 467sylbir 218 . . . . . . . . . . . 12 ..^ ..^
469468ex 441 . . . . . . . . . . 11 ..^ ..^
470 simpl 464 . . . . . . . . . . . . . 14
471 fveq2 5879 . . . . . . . . . . . . . . . . 17
472 oveq1 6315 . . . . . . . . . . . . . . . . . 18
473472fveq2d 5883 . . . . . . . . . . . . . . . . 17
474471, 473oveq12d 6326 . . . . . . . . . . . . . . . 16
475474eqcomd 2477 . . . . . . . . . . . . . . 15
476475adantl 473 . . . . . . . . . . . . . 14
477470, 476sseqtrd 3454 . . . . . . . . . . . . 13
478477ex 441 . . . . . . . . . . . 12
479478ad2antlr 741 . . . . . . . . . . 11 ..^ ..^
480469, 479impbid 195 . . . . . . . . . 10 ..^ ..^
481480ralrimiva 2809 . . . . . . . . 9 ..^