Metamath Proof Explorer

Theorem fourierdlem105

Description: A piecewise continuous function is integrable on any closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem105.p ⊢P=m∈ℕ⟼p∈ℝ0…m|p⁡0=A∧p⁡m=B∧∀i∈0..^mp⁡i<p⁡i+1
fourierdlem105.t ⊢T=B−A
fourierdlem105.m ⊢φ→M∈ℕ
fourierdlem105.q ⊢φ→Q∈P⁡M
fourierdlem105.f ⊢φ→F:ℝ⟶ℂ
fourierdlem105.6 ⊢φ∧x∈ℝ→F⁡x+T=F⁡x
fourierdlem105.fcn ⊢φ∧i∈0..^M→F↾Q⁡iQ⁡i+1:Q⁡iQ⁡i+1⟶cnℂ
fourierdlem105.r ⊢φ∧i∈0..^M→R∈F↾Q⁡iQ⁡i+1limℂQ⁡i
fourierdlem105.l ⊢φ∧i∈0..^M→L∈F↾Q⁡iQ⁡i+1limℂQ⁡i+1
fourierdlem105.c ⊢φ→C∈ℝ
fourierdlem105.d ⊢φ→D∈C+∞
Assertion fourierdlem105 ⊢φ→x∈CD⟼F⁡x∈𝐿1

Proof

Step Hyp Ref Expression
1 fourierdlem105.p ⊢P=m∈ℕ⟼p∈ℝ0…m|p⁡0=A∧p⁡m=B∧∀i∈0..^mp⁡i<p⁡i+1
2 fourierdlem105.t ⊢T=B−A
3 fourierdlem105.m ⊢φ→M∈ℕ
4 fourierdlem105.q ⊢φ→Q∈P⁡M
5 fourierdlem105.f ⊢φ→F:ℝ⟶ℂ
6 fourierdlem105.6 ⊢φ∧x∈ℝ→F⁡x+T=F⁡x
7 fourierdlem105.fcn ⊢φ∧i∈0..^M→F↾Q⁡iQ⁡i+1:Q⁡iQ⁡i+1⟶cnℂ
8 fourierdlem105.r ⊢φ∧i∈0..^M→R∈F↾Q⁡iQ⁡i+1limℂQ⁡i
9 fourierdlem105.l ⊢φ∧i∈0..^M→L∈F↾Q⁡iQ⁡i+1limℂQ⁡i+1
10 fourierdlem105.c ⊢φ→C∈ℝ
11 fourierdlem105.d ⊢φ→D∈C+∞
12 eqid ⊢m∈ℕ⟼p∈ℝ0…m|p⁡0=C∧p⁡m=D∧∀i∈0..^mp⁡i<p⁡i+1=m∈ℕ⟼p∈ℝ0…m|p⁡0=C∧p⁡m=D∧∀i∈0..^mp⁡i<p⁡i+1
13 eqid ⊢CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q−1=CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q−1
14 oveq1 ⊢w=y→w+j⁢T=y+j⁢T
15 14 eleq1d ⊢w=y→w+j⁢T∈ran⁡Q↔y+j⁢T∈ran⁡Q
16 15 rexbidv ⊢w=y→∃j∈ℤw+j⁢T∈ran⁡Q↔∃j∈ℤy+j⁢T∈ran⁡Q
17 oveq1 ⊢j=k→j⁢T=k⁢T
18 17 oveq2d ⊢j=k→y+j⁢T=y+k⁢T
19 18 eleq1d ⊢j=k→y+j⁢T∈ran⁡Q↔y+k⁢T∈ran⁡Q
20 19 cbvrexvw ⊢∃j∈ℤy+j⁢T∈ran⁡Q↔∃k∈ℤy+k⁢T∈ran⁡Q
21 16 20 bitrdi ⊢w=y→∃j∈ℤw+j⁢T∈ran⁡Q↔∃k∈ℤy+k⁢T∈ran⁡Q
22 21 cbvrabv ⊢w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q=y∈CD|∃k∈ℤy+k⁢T∈ran⁡Q
23 22 uneq2i ⊢CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q=CD∪y∈CD|∃k∈ℤy+k⁢T∈ran⁡Q
24 isoeq1 ⊢g=f→gIsom<,<0…CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q−1CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q↔fIsom<,<0…CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q−1CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q
25 24 cbviotavw ⊢ιg|gIsom<,<0…CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q−1CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q=ιf|fIsom<,<0…CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q−1CD∪w∈CD|∃j∈ℤw+j⁢T∈ran⁡Q
26 id ⊢w=x→w=x
27 oveq2 ⊢w=x→B−w=B−x
28 27 oveq1d ⊢w=x→B−wT=B−xT
29 28 fveq2d ⊢w=x→B−wT=B−xT
30 29 oveq1d ⊢w=x→B−wT⁢T=B−xT⁢T
31 26 30 oveq12d ⊢w=x→w+B−wT⁢T=x+B−xT⁢T
32 31 cbvmptv ⊢w∈ℝ⟼w+B−wT⁢T=x∈ℝ⟼x+B−xT⁢T
33 eqeq1 ⊢w=y→w=B↔y=B
34 id ⊢w=y→w=y
35 33 34 ifbieq2d ⊢w=y→ifw=BAw=ify=BAy
36 35 cbvmptv ⊢w∈AB⟼ifw=BAw=y∈AB⟼ify=BAy
37 fveq2 ⊢z=x→w∈ℝ⟼w+B−wT⁢T⁡z=w∈ℝ⟼w+B−wT⁢T⁡x
38 37 fveq2d ⊢z=x→w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡z=w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
39 38 breq2d ⊢z=x→Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡z↔Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
40 39 rabbidv ⊢z=x→j∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡z=j∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
41 fveq2 ⊢j=i→Q⁡j=Q⁡i
42 41 breq1d ⊢j=i→Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x↔Q⁡i≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
43 42 cbvrabv ⊢j∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x=i∈0..^M|Q⁡i≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
44 40 43 eqtrdi ⊢z=x→j∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡z=i∈0..^M|Q⁡i≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡x
45 44 supeq1d ⊢z=x→supj∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡zℝ<=supi∈0..^M|Q⁡i≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡xℝ<
46 45 cbvmptv ⊢z∈ℝ⟼supj∈0..^M|Q⁡j≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡zℝ<=x∈ℝ⟼supi∈0..^M|Q⁡i≤w∈AB⟼ifw=BAw⁡w∈ℝ⟼w+B−wT⁢T⁡xℝ<
47 1 2 3 4 5 6 7 8 9 10 11 12 13 23 25 32 36 46 fourierdlem100 ⊢φ→x∈CD⟼F⁡x∈𝐿1