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

Theorem fourierdlem101 31831
 Description: Integral by substitution for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem101.d
fourierdlem101.p ..^
fourierdlem101.g
fourierdlem101.q
fourierdlem101.6
fourierdlem101.n
fourierdlem101.x
fourierdlem101.f
fourierdlem101.fcn ..^
fourierdlem101.r ..^ lim
fourierdlem101.l ..^ lim
Assertion
Ref Expression
fourierdlem101
Distinct variable groups:   ,,   ,   ,,,   ,   ,,,   ,,,   ,,   ,   ,,,   ,   ,   ,,,   ,,,   ,
Allowed substitution hints:   (,)   (,,,)   (,,,,,)   (,)   (,,,,)   (,,,,)   (,,)   (,,,,)   ()   (,,)   (,,)

Proof of Theorem fourierdlem101
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 461 . . . . 5
2 fourierdlem101.f . . . . . . 7
32ffvelrnda 6032 . . . . . 6
4 fourierdlem101.n . . . . . . . . 9
54adantr 465 . . . . . . . 8
6 pire 22718 . . . . . . . . . . . . 13
76renegcli 9892 . . . . . . . . . . . 12
87a1i 11 . . . . . . . . . . 11
96a1i 11 . . . . . . . . . . 11
10 id 22 . . . . . . . . . . 11
11 eliccre 31427 . . . . . . . . . . 11
128, 9, 10, 11syl3anc 1228 . . . . . . . . . 10
1312adantl 466 . . . . . . . . 9
14 fourierdlem101.x . . . . . . . . . 10
1514adantr 465 . . . . . . . . 9
1613, 15resubcld 9999 . . . . . . . 8
17 fourierdlem101.d . . . . . . . . 9
1817dirkerre 31718 . . . . . . . 8
195, 16, 18syl2anc 661 . . . . . . 7
2019recnd 9634 . . . . . 6
213, 20mulcld 9628 . . . . 5
22 fourierdlem101.g . . . . . 6
2322fvmpt2 5964 . . . . 5
241, 21, 23syl2anc 661 . . . 4
2524eqcomd 2475 . . 3
2625itgeq2dv 22056 . 2
27 fourierdlem101.p . . 3 ..^
28 nfcv 2629 . . . 4
29 nfcv 2629 . . . 4
30 fveq2 5872 . . . . 5
3130oveq1d 6310 . . . 4
3228, 29, 31cbvmpt 4543 . . 3
33 fourierdlem101.6 . . 3
34 fourierdlem101.q . . 3
3521ralrimiva 2881 . . . 4
3622fmpt 6053 . . . 4
3735, 36sylib 196 . . 3
3822reseq1i 5275 . . . . . 6
3938a1i 11 . . . . 5 ..^
40 ioossicc 11622 . . . . . . 7
417a1i 11 . . . . . . . . . 10
4241rexrd 9655 . . . . . . . . 9
4342adantr 465 . . . . . . . 8 ..^
446a1i 11 . . . . . . . . . 10
4544rexrd 9655 . . . . . . . . 9
4645adantr 465 . . . . . . . 8 ..^
4727, 33, 34fourierdlem15 31745 . . . . . . . . 9
4847adantr 465 . . . . . . . 8 ..^
49 simpr 461 . . . . . . . 8 ..^ ..^
5043, 46, 48, 49fourierdlem8 31738 . . . . . . 7 ..^
5140, 50syl5ss 3520 . . . . . 6 ..^
52 resmpt 5329 . . . . . 6
5351, 52syl 16 . . . . 5 ..^
54 eqidd 2468 . . . . 5 ..^
5539, 53, 543eqtrd 2512 . . . 4 ..^
562adantr 465 . . . . . . . 8 ..^
5756, 51feqresmpt 5928 . . . . . . 7 ..^
5857eqcomd 2475 . . . . . 6 ..^
59 fourierdlem101.fcn . . . . . 6 ..^
6058, 59eqeltrd 2555 . . . . 5 ..^
614adantr 465 . . . . . . . . . . . 12
62 simpr 461 . . . . . . . . . . . 12
6317dirkerre 31718 . . . . . . . . . . . 12
6461, 62, 63syl2anc 661 . . . . . . . . . . 11
6564ralrimiva 2881 . . . . . . . . . 10
66 eqid 2467 . . . . . . . . . . 11
6766fmpt 6053 . . . . . . . . . 10
6865, 67sylib 196 . . . . . . . . 9
6968adantr 465 . . . . . . . 8 ..^
70 elioore 11571 . . . . . . . . . . . . 13
7170adantl 466 . . . . . . . . . . . 12
7214adantr 465 . . . . . . . . . . . 12
7371, 72resubcld 9999 . . . . . . . . . . 11
7473adantlr 714 . . . . . . . . . 10 ..^
7574ralrimiva 2881 . . . . . . . . 9 ..^
76 eqid 2467 . . . . . . . . . 10
7776fmpt 6053 . . . . . . . . 9
7875, 77sylib 196 . . . . . . . 8 ..^
79 fcompt 6068 . . . . . . . 8
8069, 78, 79syl2anc 661 . . . . . . 7 ..^
81 nfcv 2629 . . . . . . . . . 10
82 nfcv 2629 . . . . . . . . . 10
83 oveq1 6302 . . . . . . . . . . 11
8483fveq2d 5876 . . . . . . . . . 10
8581, 82, 84cbvmpt 4543 . . . . . . . . 9
8685a1i 11 . . . . . . . 8 ..^
87 eqidd 2468 . . . . . . . . . . 11 ..^
88 simpr 461 . . . . . . . . . . . . 13 ..^
89 eqidd 2468 . . . . . . . . . . . . . . 15 ..^
9083adantl 466 . . . . . . . . . . . . . . 15 ..^
91 simpr 461 . . . . . . . . . . . . . . 15 ..^
92 elioore 11571 . . . . . . . . . . . . . . . . . 18
9392adantl 466 . . . . . . . . . . . . . . . . 17
9414adantr 465 . . . . . . . . . . . . . . . . 17
9593, 94resubcld 9999 . . . . . . . . . . . . . . . 16
9695adantlr 714 . . . . . . . . . . . . . . 15 ..^
9789, 90, 91, 96fvmptd 5962 . . . . . . . . . . . . . 14 ..^
9897adantr 465 . . . . . . . . . . . . 13 ..^
9988, 98eqtrd 2508 . . . . . . . . . . . 12 ..^
10099fveq2d 5876 . . . . . . . . . . 11 ..^
10178ffvelrnda 6032 . . . . . . . . . . 11 ..^
1024ad2antrr 725 . . . . . . . . . . . 12 ..^
10317dirkerre 31718 . . . . . . . . . . . 12
104102, 96, 103syl2anc 661 . . . . . . . . . . 11 ..^
10587, 100, 101, 104fvmptd 5962 . . . . . . . . . 10 ..^
106105eqcomd 2475 . . . . . . . . 9 ..^
107106mpteq2dva 4539 . . . . . . . 8 ..^
10886, 107eqtr2d 2509 . . . . . . 7 ..^
10980, 108eqtr2d 2509 . . . . . 6 ..^
110 eqid 2467 . . . . . . . 8
111 simpr 461 . . . . . . . . . . . . 13
112 ax-resscn 9561 . . . . . . . . . . . . . . 15
113112, 14sseldi 3507 . . . . . . . . . . . . . 14
114113adantr 465 . . . . . . . . . . . . 13
115111, 114negsubd 9948 . . . . . . . . . . . 12
116115eqcomd 2475 . . . . . . . . . . 11
117116mpteq2dva 4539 . . . . . . . . . 10
118113negcld 9929 . . . . . . . . . . 11
119 eqid 2467 . . . . . . . . . . . 12
120119addccncf 21288 . . . . . . . . . . 11
121118, 120syl 16 . . . . . . . . . 10
122117, 121eqeltrd 2555 . . . . . . . . 9
123122adantr 465 . . . . . . . 8 ..^
124 ioossre 11598 . . . . . . . . . 10
125124, 112sstri 3518 . . . . . . . . 9
126125a1i 11 . . . . . . . 8 ..^
127112a1i 11 . . . . . . . 8 ..^
128110, 123, 126, 127, 74cncfmptssg 31531 . . . . . . 7 ..^
129112, 64sseldi 3507 . . . . . . . . . 10
130129, 66fmptd 6056 . . . . . . . . 9
131 ssid 3528 . . . . . . . . . . 11
132131a1i 11 . . . . . . . . . 10
13317dirkerf 31720 . . . . . . . . . . . . . 14
1344, 133syl 16 . . . . . . . . . . . . 13
135134feqmptd 5927 . . . . . . . . . . . 12
136135eqcomd 2475 . . . . . . . . . . 11
13717dirkercncf 31730 . . . . . . . . . . . 12
1384, 137syl 16 . . . . . . . . . . 11
139136, 138eqeltrd 2555 . . . . . . . . . 10
140 cncffvrn 21270 . . . . . . . . . 10
141132, 139, 140syl2anc 661 . . . . . . . . 9
142130, 141mpbird 232 . . . . . . . 8
143142adantr 465 . . . . . . 7 ..^
144128, 143cncfco 21279 . . . . . 6 ..^
145109, 144eqeltrd 2555 . . . . 5 ..^
14660, 145mulcncf 21727 . . . 4 ..^
14755, 146eqeltrd 2555 . . 3 ..^
148 cncff 21265 . . . . . . . 8
14959, 148syl 16 . . . . . . 7 ..^
150134adantr 465 . . . . . . . . . . 11
151124sseli 3505 . . . . . . . . . . . . 13
152151adantl 466 . . . . . . . . . . . 12
15314adantr 465 . . . . . . . . . . . 12
154152, 153resubcld 9999 . . . . . . . . . . 11
155 ffvelrn 6030 . . . . . . . . . . 11
156150, 154, 155syl2anc 661 . . . . . . . . . 10
157112, 156sseldi 3507 . . . . . . . . 9
158 eqid 2467 . . . . . . . . 9
159157, 158fmptd 6056 . . . . . . . 8
160159adantr 465 . . . . . . 7 ..^
161 eqid 2467 . . . . . . 7
162 fourierdlem101.r . . . . . . 7 ..^ lim
163 iftrue 3951 . . . . . . . . . . . . 13
164163adantl 466 . . . . . . . . . . . 12 ..^
165 oveq1 6302 . . . . . . . . . . . . . . 15
166165fveq2d 5876 . . . . . . . . . . . . . 14
167166eqcomd 2475 . . . . . . . . . . . . 13
168167adantl 466 . . . . . . . . . . . 12 ..^
169 eqidd 2468 . . . . . . . . . . . 12 ..^
170164, 168, 1693eqtrd 2512 . . . . . . . . . . 11 ..^
171 iffalse 3954 . . . . . . . . . . . . 13
172171adantl 466 . . . . . . . . . . . 12 ..^
173 eqidd 2468 . . . . . . . . . . . . 13 ..^
174 oveq1 6302 . . . . . . . . . . . . . . 15
175174fveq2d 5876 . . . . . . . . . . . . . 14
176175adantl 466 . . . . . . . . . . . . 13 ..^
177 simpl 457 . . . . . . . . . . . . . . 15
178 vex 3121 . . . . . . . . . . . . . . . . . . 19
179 elsncg 4056 . . . . . . . . . . . . . . . . . . 19
180178, 179ax-mp 5 . . . . . . . . . . . . . . . . . 18
181180notbii 296 . . . . . . . . . . . . . . . . 17
182181biimpri 206 . . . . . . . . . . . . . . . 16
183182adantl 466 . . . . . . . . . . . . . . 15
184 elun 3650 . . . . . . . . . . . . . . . . . . 19
185184biimpi 194 . . . . . . . . . . . . . . . . . 18
186185orcomd 388 . . . . . . . . . . . . . . . . 17
187186adantr 465 . . . . . . . . . . . . . . . 16
188 simpr 461 . . . . . . . . . . . . . . . 16
189 pm2.53 373 . . . . . . . . . . . . . . . 16
190187, 188, 189sylc 60 . . . . . . . . . . . . . . 15
191177, 183, 190syl2anc 661 . . . . . . . . . . . . . 14
192191adantll 713 . . . . . . . . . . . . 13 ..^
193134ad2antrr 725 . . . . . . . . . . . . . . 15 ..^
194 simpr 461 . . . . . . . . . . . . . . . . . . 19 ..^
19512ssriv 3513 . . . . . . . . . . . . . . . . . . . . 21
196 fzossfz 11826 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
197196, 49sseldi 3507 . . . . . . . . . . . . . . . . . . . . . 22 ..^
198 ffvelrn 6030 . . . . . . . . . . . . . . . . . . . . . 22
19948, 197, 198syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21 ..^
200195, 199sseldi 3507 . . . . . . . . . . . . . . . . . . . 20 ..^
201200adantr 465 . . . . . . . . . . . . . . . . . . 19 ..^
202194, 201eqeltrd 2555 . . . . . . . . . . . . . . . . . 18 ..^
203202adantlr 714 . . . . . . . . . . . . . . . . 17 ..^
204192, 70syl 16 . . . . . . . . . . . . . . . . 17 ..^
205203, 204pm2.61dan 789 . . . . . . . . . . . . . . . 16 ..^
20614ad2antrr 725 . . . . . . . . . . . . . . . 16 ..^
207205, 206resubcld 9999 . . . . . . . . . . . . . . 15 ..^
208 ffvelrn 6030 . . . . . . . . . . . . . . 15
209193, 207, 208syl2anc 661 . . . . . . . . . . . . . 14 ..^
210209adantr 465 . . . . . . . . . . . . 13 ..^
211173, 176, 192, 210fvmptd 5962 . . . . . . . . . . . 12 ..^
212 eqidd 2468 . . . . . . . . . . . 12 ..^
213172, 211, 2123eqtrd 2512 . . . . . . . . . . 11 ..^
214170, 213pm2.61dan 789 . . . . . . . . . 10 ..^
215214mpteq2dva 4539 . . . . . . . . 9 ..^
216134adantr 465 . . . . . . . . . . . . . . 15 ..^
217 simpr 461 . . . . . . . . . . . . . . . . . . . 20
218 elun 3650 . . . . . . . . . . . . . . . . . . . 20
219217, 218sylib 196 . . . . . . . . . . . . . . . . . . 19
220219adantlr 714 . . . . . . . . . . . . . . . . . 18 ..^
221151a1i 11 . . . . . . . . . . . . . . . . . . 19 ..^
222 elsni 4058 . . . . . . . . . . . . . . . . . . . . . . 23
223222adantl 466 . . . . . . . . . . . . . . . . . . . . . 22 ..^
224200adantr 465 . . . . . . . . . . . . . . . . . . . . . 22 ..^
225223, 224eqeltrd 2555 . . . . . . . . . . . . . . . . . . . . 21 ..^
226225ex 434 . . . . . . . . . . . . . . . . . . . 20 ..^
227226adantr 465 . . . . . . . . . . . . . . . . . . 19 ..^
228 pm3.44 511 . . . . . . . . . . . . . . . . . . 19
229221, 227, 228syl2anc 661 . . . . . . . . . . . . . . . . . 18 ..^
230220, 229mpd 15 . . . . . . . . . . . . . . . . 17 ..^
23114ad2antrr 725 . . . . . . . . . . . . . . . . 17 ..^
232230, 231resubcld 9999 . . . . . . . . . . . . . . . 16 ..^
233 eqid 2467 . . . . . . . . . . . . . . . 16
234232, 233fmptd 6056 . . . . . . . . . . . . . . 15 ..^
235 fcompt 6068 . . . . . . . . . . . . . . 15
236216, 234, 235syl2anc 661 . . . . . . . . . . . . . 14 ..^
237 eqidd 2468 . . . . . . . . . . . . . . . . 17 ..^
238174adantl 466 . . . . . . . . . . . . . . . . 17 ..^
239 simpr 461 . . . . . . . . . . . . . . . . 17 ..^
240237, 238, 239, 207fvmptd 5962 . . . . . . . . . . . . . . . 16 ..^
241240fveq2d 5876 . . . . . . . . . . . . . . 15 ..^
242241mpteq2dva 4539 . . . . . . . . . . . . . 14 ..^
243236, 242eqtr2d 2509 . . . . . . . . . . . . 13 ..^
244 eqid 2467 . . . . . . . . . . . . . . . 16
245 simpr 461 . . . . . . . . . . . . . . . . . . . . 21
246113adantr 465 . . . . . . . . . . . . . . . . . . . . 21
247 negsub 9879 . . . . . . . . . . . . . . . . . . . . 21
248245, 246, 247syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
249248eqcomd 2475 . . . . . . . . . . . . . . . . . . 19
250249mpteq2dva 4539 . . . . . . . . . . . . . . . . . 18
251 eqid 2467 . . . . . . . . . . . . . . . . . . . 20
252251addccncf 21288 . . . . . . . . . . . . . . . . . . 19
253118, 252syl 16 . . . . . . . . . . . . . . . . . 18
254250, 253eqeltrd 2555 . . . . . . . . . . . . . . . . 17
255254adantr 465 . . . . . . . . . . . . . . . 16 ..^
256112, 200sseldi 3507 . . . . . . . . . . . . . . . . . . 19 ..^
257256snssd 4178 . . . . . . . . . . . . . . . . . 18 ..^
258126, 257jca 532 . . . . . . . . . . . . . . . . 17 ..^
259 unss 3683 . . . . . . . . . . . . . . . . 17
260258, 259sylib 196 . . . . . . . . . . . . . . . 16 ..^
261244, 255, 260, 127, 232cncfmptssg 31531 . . . . . . . . . . . . . . 15 ..^
262135, 142eqeltrd 2555 . . . . . . . . . . . . . . . 16
263262adantr 465 . . . . . . . . . . . . . . 15 ..^
264261, 263cncfco 21279 . . . . . . . . . . . . . 14 ..^
265131a1i 11 . . . . . . . . . . . . . . 15 ..^
266 eqid 2467 . . . . . . . . . . . . . . . 16 fld fld
267 eqid 2467 . . . . . . . . . . . . . . . 16 fldt fldt
268266cnfldtop 21159 . . . . . . . . . . . . . . . . . 18 fld
269 unicntop 31336 . . . . . . . . . . . . . . . . . . 19 fld
270269restid 14706 . . . . . . . . . . . . . . . . . 18 fld fldt fld
271268, 270ax-mp 5 . . . . . . . . . . . . . . . . 17 fldt fld
272271eqcomi 2480 . . . . . . . . . . . . . . . 16 fld fldt
273266, 267, 272cncfcn 21281 . . . . . . . . . . . . . . 15 fldt fld
274260, 265, 273syl2anc 661 . . . . . . . . . . . . . 14 ..^ fldt fld
275264, 274eleqtrd 2557 . . . . . . . . . . . . 13 ..^ fldt fld
276243, 275eqeltrd 2555 . . . . . . . . . . . 12 ..^ fldt fld
277266cnfldtopon 21158 . . . . . . . . . . . . . . 15 fld TopOn
278277a1i 11 . . . . . . . . . . . . . 14 ..^ fld TopOn
279 resttopon 19530 . . . . . . . . . . . . . 14 fld TopOn fldt TopOn
280278, 260, 279syl2anc 661 . . . . . . . . . . . . 13 ..^ fldt TopOn
281 cncnp 19649 . . . . . . . . . . . . 13 fldt TopOn fld TopOn fldt fld fldt fld
282280, 278, 281syl2anc 661 . . . . . . . . . . . 12 ..^ fldt fld fldt fld
283276, 282mpbid 210 . . . . . . . . . . 11 ..^ fldt fld
284283simprd 463 . . . . . . . . . 10 ..^ fldt fld
285 eqidd 2468 . . . . . . . . . . . . 13 ..^
286 elsncg 4056 . . . . . . . . . . . . . 14
287200, 286syl 16 . . . . . . . . . . . . 13 ..^
288285, 287mpbird 232 . . . . . . . . . . . 12 ..^
289288olcd 393 . . . . . . . . . . 11 ..^
290 elun 3650 . . . . . . . . . . 11
291289, 290sylibr 212 . . . . . . . . . 10 ..^
292 fveq2 5872 . . . . . . . . . . . 12 fldt fld fldt fld
293292eleq2d 2537 . . . . . . . . . . 11 fldt fld fldt fld
294293rspccva 3218 . . . . . . . . . 10 fldt fld fldt fld
295284, 291, 294syl2anc 661 . . . . . . . . 9 ..^ fldt fld
296215, 295eqeltrd 2555 . . . . . . . 8 ..^