Metamath Proof Explorer


Theorem fourierdlem46

Description: The function F has a limit at the bounds of every interval induced by the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem46.cn φ F : dom F cn
fourierdlem46.rlim φ x π π dom F F x +∞ lim x
fourierdlem46.llim φ x π π dom F F −∞ x lim x
fourierdlem46.qiso φ Q Isom < , < 0 M H
fourierdlem46.qf φ Q : 0 M H
fourierdlem46.i φ I 0 ..^ M
fourierdlem46.10 φ Q I < Q I + 1
fourierdlem46.qiss φ Q I Q I + 1 π π
fourierdlem46.c φ C
fourierdlem46.h H = π π C π π dom F
fourierdlem46.ranq φ ran Q = H
Assertion fourierdlem46 φ F Q I Q I + 1 lim Q I F Q I Q I + 1 lim Q I + 1

Proof

Step Hyp Ref Expression
1 fourierdlem46.cn φ F : dom F cn
2 fourierdlem46.rlim φ x π π dom F F x +∞ lim x
3 fourierdlem46.llim φ x π π dom F F −∞ x lim x
4 fourierdlem46.qiso φ Q Isom < , < 0 M H
5 fourierdlem46.qf φ Q : 0 M H
6 fourierdlem46.i φ I 0 ..^ M
7 fourierdlem46.10 φ Q I < Q I + 1
8 fourierdlem46.qiss φ Q I Q I + 1 π π
9 fourierdlem46.c φ C
10 fourierdlem46.h H = π π C π π dom F
11 fourierdlem46.ranq φ ran Q = H
12 pire π
13 12 a1i φ π
14 13 renegcld φ π
15 tpssi π π C π π C
16 14 13 9 15 syl3anc φ π π C
17 14 13 iccssred φ π π
18 17 ssdifssd φ π π dom F
19 16 18 unssd φ π π C π π dom F
20 10 19 eqsstrid φ H
21 elfzofz I 0 ..^ M I 0 M
22 6 21 syl φ I 0 M
23 5 22 ffvelrnd φ Q I H
24 20 23 sseldd φ Q I
25 24 adantr φ Q I dom F Q I
26 fzofzp1 I 0 ..^ M I + 1 0 M
27 6 26 syl φ I + 1 0 M
28 5 27 ffvelrnd φ Q I + 1 H
29 20 28 sseldd φ Q I + 1
30 29 rexrd φ Q I + 1 *
31 30 adantr φ Q I dom F Q I + 1 *
32 7 adantr φ Q I dom F Q I < Q I + 1
33 simpr Q I dom F x = Q I x = Q I
34 simpl Q I dom F x = Q I Q I dom F
35 33 34 eqeltrd Q I dom F x = Q I x dom F
36 35 adantll φ Q I dom F x = Q I x dom F
37 36 adantlr φ Q I dom F x Q I Q I + 1 x = Q I x dom F
38 ssun2 π π dom F π π C π π dom F
39 38 10 sseqtrri π π dom F H
40 ioossicc π π π π
41 8 40 sstrdi φ Q I Q I + 1 π π
42 41 sselda φ x Q I Q I + 1 x π π
43 42 adantr φ x Q I Q I + 1 ¬ x dom F x π π
44 simpr φ x Q I Q I + 1 ¬ x dom F ¬ x dom F
45 43 44 eldifd φ x Q I Q I + 1 ¬ x dom F x π π dom F
46 39 45 sseldi φ x Q I Q I + 1 ¬ x dom F x H
47 11 eqcomd φ H = ran Q
48 47 ad2antrr φ x Q I Q I + 1 ¬ x dom F H = ran Q
49 46 48 eleqtrd φ x Q I Q I + 1 ¬ x dom F x ran Q
50 simpr φ x ran Q x ran Q
51 ffn Q : 0 M H Q Fn 0 M
52 5 51 syl φ Q Fn 0 M
53 52 adantr φ x ran Q Q Fn 0 M
54 fvelrnb Q Fn 0 M x ran Q j 0 M Q j = x
55 53 54 syl φ x ran Q x ran Q j 0 M Q j = x
56 50 55 mpbid φ x ran Q j 0 M Q j = x
57 56 adantlr φ x Q I Q I + 1 x ran Q j 0 M Q j = x
58 elfzelz j 0 M j
59 58 ad2antlr φ x Q I Q I + 1 x ran Q j 0 M Q j = x j
60 simplll φ x Q I Q I + 1 j 0 M Q j = x φ
61 simplr φ x Q I Q I + 1 j 0 M Q j = x j 0 M
62 simpr φ x Q I Q I + 1 Q j = x Q j = x
63 simplr φ x Q I Q I + 1 Q j = x x Q I Q I + 1
64 62 63 eqeltrd φ x Q I Q I + 1 Q j = x Q j Q I Q I + 1
65 64 adantlr φ x Q I Q I + 1 j 0 M Q j = x Q j Q I Q I + 1
66 elfzoelz I 0 ..^ M I
67 6 66 syl φ I
68 67 ad2antrr φ j 0 M Q j Q I Q I + 1 I
69 24 rexrd φ Q I *
70 69 ad2antrr φ j 0 M Q j Q I Q I + 1 Q I *
71 30 ad2antrr φ j 0 M Q j Q I Q I + 1 Q I + 1 *
72 simpr φ j 0 M Q j Q I Q I + 1 Q j Q I Q I + 1
73 ioogtlb Q I * Q I + 1 * Q j Q I Q I + 1 Q I < Q j
74 70 71 72 73 syl3anc φ j 0 M Q j Q I Q I + 1 Q I < Q j
75 4 ad2antrr φ j 0 M Q j Q I Q I + 1 Q Isom < , < 0 M H
76 22 ad2antrr φ j 0 M Q j Q I Q I + 1 I 0 M
77 simplr φ j 0 M Q j Q I Q I + 1 j 0 M
78 isorel Q Isom < , < 0 M H I 0 M j 0 M I < j Q I < Q j
79 75 76 77 78 syl12anc φ j 0 M Q j Q I Q I + 1 I < j Q I < Q j
80 74 79 mpbird φ j 0 M Q j Q I Q I + 1 I < j
81 iooltub Q I * Q I + 1 * Q j Q I Q I + 1 Q j < Q I + 1
82 70 71 72 81 syl3anc φ j 0 M Q j Q I Q I + 1 Q j < Q I + 1
83 27 ad2antrr φ j 0 M Q j Q I Q I + 1 I + 1 0 M
84 isorel Q Isom < , < 0 M H j 0 M I + 1 0 M j < I + 1 Q j < Q I + 1
85 75 77 83 84 syl12anc φ j 0 M Q j Q I Q I + 1 j < I + 1 Q j < Q I + 1
86 82 85 mpbird φ j 0 M Q j Q I Q I + 1 j < I + 1
87 btwnnz I I < j j < I + 1 ¬ j
88 68 80 86 87 syl3anc φ j 0 M Q j Q I Q I + 1 ¬ j
89 60 61 65 88 syl21anc φ x Q I Q I + 1 j 0 M Q j = x ¬ j
90 89 adantllr φ x Q I Q I + 1 x ran Q j 0 M Q j = x ¬ j
91 59 90 pm2.65da φ x Q I Q I + 1 x ran Q j 0 M ¬ Q j = x
92 91 nrexdv φ x Q I Q I + 1 x ran Q ¬ j 0 M Q j = x
93 57 92 pm2.65da φ x Q I Q I + 1 ¬ x ran Q
94 93 adantr φ x Q I Q I + 1 ¬ x dom F ¬ x ran Q
95 49 94 condan φ x Q I Q I + 1 x dom F
96 95 ralrimiva φ x Q I Q I + 1 x dom F
97 dfss3 Q I Q I + 1 dom F x Q I Q I + 1 x dom F
98 96 97 sylibr φ Q I Q I + 1 dom F
99 98 ad2antrr φ x Q I Q I + 1 ¬ x = Q I Q I Q I + 1 dom F
100 69 ad2antrr φ x Q I Q I + 1 ¬ x = Q I Q I *
101 30 ad2antrr φ x Q I Q I + 1 ¬ x = Q I Q I + 1 *
102 icossre Q I Q I + 1 * Q I Q I + 1
103 24 30 102 syl2anc φ Q I Q I + 1
104 103 sselda φ x Q I Q I + 1 x
105 104 adantr φ x Q I Q I + 1 ¬ x = Q I x
106 24 ad2antrr φ x Q I Q I + 1 ¬ x = Q I Q I
107 69 adantr φ x Q I Q I + 1 Q I *
108 30 adantr φ x Q I Q I + 1 Q I + 1 *
109 simpr φ x Q I Q I + 1 x Q I Q I + 1
110 icogelb Q I * Q I + 1 * x Q I Q I + 1 Q I x
111 107 108 109 110 syl3anc φ x Q I Q I + 1 Q I x
112 111 adantr φ x Q I Q I + 1 ¬ x = Q I Q I x
113 neqne ¬ x = Q I x Q I
114 113 adantl φ x Q I Q I + 1 ¬ x = Q I x Q I
115 106 105 112 114 leneltd φ x Q I Q I + 1 ¬ x = Q I Q I < x
116 icoltub Q I * Q I + 1 * x Q I Q I + 1 x < Q I + 1
117 107 108 109 116 syl3anc φ x Q I Q I + 1 x < Q I + 1
118 117 adantr φ x Q I Q I + 1 ¬ x = Q I x < Q I + 1
119 100 101 105 115 118 eliood φ x Q I Q I + 1 ¬ x = Q I x Q I Q I + 1
120 99 119 sseldd φ x Q I Q I + 1 ¬ x = Q I x dom F
121 120 adantllr φ Q I dom F x Q I Q I + 1 ¬ x = Q I x dom F
122 37 121 pm2.61dan φ Q I dom F x Q I Q I + 1 x dom F
123 122 ralrimiva φ Q I dom F x Q I Q I + 1 x dom F
124 dfss3 Q I Q I + 1 dom F x Q I Q I + 1 x dom F
125 123 124 sylibr φ Q I dom F Q I Q I + 1 dom F
126 1 adantr φ Q I dom F F : dom F cn
127 rescncf Q I Q I + 1 dom F F : dom F cn F Q I Q I + 1 : Q I Q I + 1 cn
128 125 126 127 sylc φ Q I dom F F Q I Q I + 1 : Q I Q I + 1 cn
129 25 31 32 128 icocncflimc φ Q I dom F F Q I Q I + 1 Q I F Q I Q I + 1 Q I Q I + 1 lim Q I
130 24 leidd φ Q I Q I
131 69 30 69 130 7 elicod φ Q I Q I Q I + 1
132 fvres Q I Q I Q I + 1 F Q I Q I + 1 Q I = F Q I
133 131 132 syl φ F Q I Q I + 1 Q I = F Q I
134 133 eqcomd φ F Q I = F Q I Q I + 1 Q I
135 134 adantr φ Q I dom F F Q I = F Q I Q I + 1 Q I
136 ioossico Q I Q I + 1 Q I Q I + 1
137 136 a1i φ Q I dom F Q I Q I + 1 Q I Q I + 1
138 137 resabs1d φ Q I dom F F Q I Q I + 1 Q I Q I + 1 = F Q I Q I + 1
139 138 eqcomd φ Q I dom F F Q I Q I + 1 = F Q I Q I + 1 Q I Q I + 1
140 139 oveq1d φ Q I dom F F Q I Q I + 1 lim Q I = F Q I Q I + 1 Q I Q I + 1 lim Q I
141 129 135 140 3eltr4d φ Q I dom F F Q I F Q I Q I + 1 lim Q I
142 141 ne0d φ Q I dom F F Q I Q I + 1 lim Q I
143 pnfxr +∞ *
144 143 a1i φ +∞ *
145 29 ltpnfd φ Q I + 1 < +∞
146 30 144 145 xrltled φ Q I + 1 +∞
147 iooss2 +∞ * Q I + 1 +∞ Q I Q I + 1 Q I +∞
148 143 146 147 sylancr φ Q I Q I + 1 Q I +∞
149 148 resabs1d φ F Q I +∞ Q I Q I + 1 = F Q I Q I + 1
150 149 oveq1d φ F Q I +∞ Q I Q I + 1 lim Q I = F Q I Q I + 1 lim Q I
151 150 eqcomd φ F Q I Q I + 1 lim Q I = F Q I +∞ Q I Q I + 1 lim Q I
152 151 adantr φ ¬ Q I dom F F Q I Q I + 1 lim Q I = F Q I +∞ Q I Q I + 1 lim Q I
153 limcresi F Q I +∞ lim Q I F Q I +∞ Q I Q I + 1 lim Q I
154 24 adantr φ ¬ Q I dom F Q I
155 simpl φ ¬ Q I dom F φ
156 12 renegcli π
157 156 rexri π *
158 157 a1i φ π *
159 12 rexri π *
160 159 a1i φ π *
161 14 13 24 29 7 8 fourierdlem10 φ π Q I Q I + 1 π
162 161 simpld φ π Q I
163 161 simprd φ Q I + 1 π
164 24 29 13 7 163 ltletrd φ Q I < π
165 158 160 69 162 164 elicod φ Q I π π
166 165 adantr φ ¬ Q I dom F Q I π π
167 simpr φ ¬ Q I dom F ¬ Q I dom F
168 166 167 eldifd φ ¬ Q I dom F Q I π π dom F
169 155 168 jca φ ¬ Q I dom F φ Q I π π dom F
170 eleq1 x = Q I x π π dom F Q I π π dom F
171 170 anbi2d x = Q I φ x π π dom F φ Q I π π dom F
172 oveq1 x = Q I x +∞ = Q I +∞
173 172 reseq2d x = Q I F x +∞ = F Q I +∞
174 id x = Q I x = Q I
175 173 174 oveq12d x = Q I F x +∞ lim x = F Q I +∞ lim Q I
176 175 neeq1d x = Q I F x +∞ lim x F Q I +∞ lim Q I
177 171 176 imbi12d x = Q I φ x π π dom F F x +∞ lim x φ Q I π π dom F F Q I +∞ lim Q I
178 177 2 vtoclg Q I φ Q I π π dom F F Q I +∞ lim Q I
179 154 169 178 sylc φ ¬ Q I dom F F Q I +∞ lim Q I
180 ssn0 F Q I +∞ lim Q I F Q I +∞ Q I Q I + 1 lim Q I F Q I +∞ lim Q I F Q I +∞ Q I Q I + 1 lim Q I
181 153 179 180 sylancr φ ¬ Q I dom F F Q I +∞ Q I Q I + 1 lim Q I
182 152 181 eqnetrd φ ¬ Q I dom F F Q I Q I + 1 lim Q I
183 142 182 pm2.61dan φ F Q I Q I + 1 lim Q I
184 69 adantr φ Q I + 1 dom F Q I *
185 29 adantr φ Q I + 1 dom F Q I + 1
186 7 adantr φ Q I + 1 dom F Q I < Q I + 1
187 simpr Q I + 1 dom F x = Q I + 1 x = Q I + 1
188 simpl Q I + 1 dom F x = Q I + 1 Q I + 1 dom F
189 187 188 eqeltrd Q I + 1 dom F x = Q I + 1 x dom F
190 189 adantll φ Q I + 1 dom F x = Q I + 1 x dom F
191 190 adantlr φ Q I + 1 dom F x Q I Q I + 1 x = Q I + 1 x dom F
192 98 ad2antrr φ x Q I Q I + 1 ¬ x = Q I + 1 Q I Q I + 1 dom F
193 69 ad2antrr φ x Q I Q I + 1 ¬ x = Q I + 1 Q I *
194 30 ad2antrr φ x Q I Q I + 1 ¬ x = Q I + 1 Q I + 1 *
195 69 adantr φ x Q I Q I + 1 Q I *
196 29 adantr φ x Q I Q I + 1 Q I + 1
197 iocssre Q I * Q I + 1 Q I Q I + 1
198 195 196 197 syl2anc φ x Q I Q I + 1 Q I Q I + 1
199 simpr φ x Q I Q I + 1 x Q I Q I + 1
200 198 199 sseldd φ x Q I Q I + 1 x
201 200 adantr φ x Q I Q I + 1 ¬ x = Q I + 1 x
202 30 adantr φ x Q I Q I + 1 Q I + 1 *
203 iocgtlb Q I * Q I + 1 * x Q I Q I + 1 Q I < x
204 195 202 199 203 syl3anc φ x Q I Q I + 1 Q I < x
205 204 adantr φ x Q I Q I + 1 ¬ x = Q I + 1 Q I < x
206 29 ad2antrr φ x Q I Q I + 1 ¬ x = Q I + 1 Q I + 1
207 iocleub Q I * Q I + 1 * x Q I Q I + 1 x Q I + 1
208 195 202 199 207 syl3anc φ x Q I Q I + 1 x Q I + 1
209 208 adantr φ x Q I Q I + 1 ¬ x = Q I + 1 x Q I + 1
210 neqne ¬ x = Q I + 1 x Q I + 1
211 210 necomd ¬ x = Q I + 1 Q I + 1 x
212 211 adantl φ x Q I Q I + 1 ¬ x = Q I + 1 Q I + 1 x
213 201 206 209 212 leneltd φ x Q I Q I + 1 ¬ x = Q I + 1 x < Q I + 1
214 193 194 201 205 213 eliood φ x Q I Q I + 1 ¬ x = Q I + 1 x Q I Q I + 1
215 192 214 sseldd φ x Q I Q I + 1 ¬ x = Q I + 1 x dom F
216 215 adantllr φ Q I + 1 dom F x Q I Q I + 1 ¬ x = Q I + 1 x dom F
217 191 216 pm2.61dan φ Q I + 1 dom F x Q I Q I + 1 x dom F
218 217 ralrimiva φ Q I + 1 dom F x Q I Q I + 1 x dom F
219 dfss3 Q I Q I + 1 dom F x Q I Q I + 1 x dom F
220 218 219 sylibr φ Q I + 1 dom F Q I Q I + 1 dom F
221 1 adantr φ Q I + 1 dom F F : dom F cn
222 rescncf Q I Q I + 1 dom F F : dom F cn F Q I Q I + 1 : Q I Q I + 1 cn
223 220 221 222 sylc φ Q I + 1 dom F F Q I Q I + 1 : Q I Q I + 1 cn
224 184 185 186 223 ioccncflimc φ Q I + 1 dom F F Q I Q I + 1 Q I + 1 F Q I Q I + 1 Q I Q I + 1 lim Q I + 1
225 29 leidd φ Q I + 1 Q I + 1
226 69 30 30 7 225 eliocd φ Q I + 1 Q I Q I + 1
227 fvres Q I + 1 Q I Q I + 1 F Q I Q I + 1 Q I + 1 = F Q I + 1
228 226 227 syl φ F Q I Q I + 1 Q I + 1 = F Q I + 1
229 228 eqcomd φ F Q I + 1 = F Q I Q I + 1 Q I + 1
230 ioossioc Q I Q I + 1 Q I Q I + 1
231 resabs1 Q I Q I + 1 Q I Q I + 1 F Q I Q I + 1 Q I Q I + 1 = F Q I Q I + 1
232 230 231 ax-mp F Q I Q I + 1 Q I Q I + 1 = F Q I Q I + 1
233 232 eqcomi F Q I Q I + 1 = F Q I Q I + 1 Q I Q I + 1
234 233 oveq1i F Q I Q I + 1 lim Q I + 1 = F Q I Q I + 1 Q I Q I + 1 lim Q I + 1
235 234 a1i φ F Q I Q I + 1 lim Q I + 1 = F Q I Q I + 1 Q I Q I + 1 lim Q I + 1
236 229 235 eleq12d φ F Q I + 1 F Q I Q I + 1 lim Q I + 1 F Q I Q I + 1 Q I + 1 F Q I Q I + 1 Q I Q I + 1 lim Q I + 1
237 236 adantr φ Q I + 1 dom F F Q I + 1 F Q I Q I + 1 lim Q I + 1 F Q I Q I + 1 Q I + 1 F Q I Q I + 1 Q I Q I + 1 lim Q I + 1
238 224 237 mpbird φ Q I + 1 dom F F Q I + 1 F Q I Q I + 1 lim Q I + 1
239 238 ne0d φ Q I + 1 dom F F Q I Q I + 1 lim Q I + 1
240 mnfxr −∞ *
241 240 a1i φ −∞ *
242 24 mnfltd φ −∞ < Q I
243 241 69 242 xrltled φ −∞ Q I
244 iooss1 −∞ * −∞ Q I Q I Q I + 1 −∞ Q I + 1
245 240 243 244 sylancr φ Q I Q I + 1 −∞ Q I + 1
246 245 resabs1d φ F −∞ Q I + 1 Q I Q I + 1 = F Q I Q I + 1
247 246 eqcomd φ F Q I Q I + 1 = F −∞ Q I + 1 Q I Q I + 1
248 247 adantr φ ¬ Q I + 1 dom F F Q I Q I + 1 = F −∞ Q I + 1 Q I Q I + 1
249 248 oveq1d φ ¬ Q I + 1 dom F F Q I Q I + 1 lim Q I + 1 = F −∞ Q I + 1 Q I Q I + 1 lim Q I + 1
250 limcresi F −∞ Q I + 1 lim Q I + 1 F −∞ Q I + 1 Q I Q I + 1 lim Q I + 1
251 29 adantr φ ¬ Q I + 1 dom F Q I + 1
252 simpl φ ¬ Q I + 1 dom F φ
253 157 a1i φ ¬ Q I + 1 dom F π *
254 159 a1i φ ¬ Q I + 1 dom F π *
255 30 adantr φ ¬ Q I + 1 dom F Q I + 1 *
256 14 24 29 162 7 lelttrd φ π < Q I + 1
257 256 adantr φ ¬ Q I + 1 dom F π < Q I + 1
258 163 adantr φ ¬ Q I + 1 dom F Q I + 1 π
259 253 254 255 257 258 eliocd φ ¬ Q I + 1 dom F Q I + 1 π π
260 simpr φ ¬ Q I + 1 dom F ¬ Q I + 1 dom F
261 259 260 eldifd φ ¬ Q I + 1 dom F Q I + 1 π π dom F
262 252 261 jca φ ¬ Q I + 1 dom F φ Q I + 1 π π dom F
263 eleq1 x = Q I + 1 x π π dom F Q I + 1 π π dom F
264 263 anbi2d x = Q I + 1 φ x π π dom F φ Q I + 1 π π dom F
265 oveq2 x = Q I + 1 −∞ x = −∞ Q I + 1
266 265 reseq2d x = Q I + 1 F −∞ x = F −∞ Q I + 1
267 id x = Q I + 1 x = Q I + 1
268 266 267 oveq12d x = Q I + 1 F −∞ x lim x = F −∞ Q I + 1 lim Q I + 1
269 268 neeq1d x = Q I + 1 F −∞ x lim x F −∞ Q I + 1 lim Q I + 1
270 264 269 imbi12d x = Q I + 1 φ x π π dom F F −∞ x lim x φ Q I + 1 π π dom F F −∞ Q I + 1 lim Q I + 1
271 270 3 vtoclg Q I + 1 φ Q I + 1 π π dom F F −∞ Q I + 1 lim Q I + 1
272 251 262 271 sylc φ ¬ Q I + 1 dom F F −∞ Q I + 1 lim Q I + 1
273 ssn0 F −∞ Q I + 1 lim Q I + 1 F −∞ Q I + 1 Q I Q I + 1 lim Q I + 1 F −∞ Q I + 1 lim Q I + 1 F −∞ Q I + 1 Q I Q I + 1 lim Q I + 1
274 250 272 273 sylancr φ ¬ Q I + 1 dom F F −∞ Q I + 1 Q I Q I + 1 lim Q I + 1
275 249 274 eqnetrd φ ¬ Q I + 1 dom F F Q I Q I + 1 lim Q I + 1
276 239 275 pm2.61dan φ F Q I Q I + 1 lim Q I + 1
277 183 276 jca φ F Q I Q I + 1 lim Q I F Q I Q I + 1 lim Q I + 1