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 ..^ m p 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 i Q i + 1 : Q i Q i + 1 cn
fourierdlem105.r φ i 0 ..^ M R F Q i Q i + 1 lim Q i
fourierdlem105.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
fourierdlem105.c φ C
fourierdlem105.d φ D C +∞
Assertion fourierdlem105 φ x C D F x 𝐿 1

Proof

Step Hyp Ref Expression
1 fourierdlem105.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p 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 i Q i + 1 : Q i Q i + 1 cn
8 fourierdlem105.r φ i 0 ..^ M R F Q i Q i + 1 lim Q i
9 fourierdlem105.l φ i 0 ..^ M L F Q i Q i + 1 lim 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 ..^ m p i < p i + 1 = m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1
13 eqid C D w C D | j w + j T ran Q 1 = C D w C D | 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 C D | j w + j T ran Q = y C D | k y + k T ran Q
23 22 uneq2i C D w C D | j w + j T ran Q = C D y C D | k y + k T ran Q
24 isoeq1 g = f g Isom < , < 0 C D w C D | j w + j T ran Q 1 C D w C D | j w + j T ran Q f Isom < , < 0 C D w C D | j w + j T ran Q 1 C D w C D | j w + j T ran Q
25 24 cbviotavw ι g | g Isom < , < 0 C D w C D | j w + j T ran Q 1 C D w C D | j w + j T ran Q = ι f | f Isom < , < 0 C D w C D | j w + j T ran Q 1 C D w C D | 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 w T = B x T
29 28 fveq2d w = x B w T = B x T
30 29 oveq1d w = x B w T T = B x T T
31 26 30 oveq12d w = x w + B w T T = x + B x T T
32 31 cbvmptv w w + B w T T = x x + B x T T
33 eqeq1 w = y w = B y = B
34 id w = y w = y
35 33 34 ifbieq2d w = y if w = B A w = if y = B A y
36 35 cbvmptv w A B if w = B A w = y A B if y = B A y
37 fveq2 z = x w w + B w T T z = w w + B w T T x
38 37 fveq2d z = x w A B if w = B A w w w + B w T T z = w A B if w = B A w w w + B w T T x
39 38 breq2d z = x Q j w A B if w = B A w w w + B w T T z Q j w A B if w = B A w w w + B w T T x
40 39 rabbidv z = x j 0 ..^ M | Q j w A B if w = B A w w w + B w T T z = j 0 ..^ M | Q j w A B if w = B A w w w + B w T T x
41 fveq2 j = i Q j = Q i
42 41 breq1d j = i Q j w A B if w = B A w w w + B w T T x Q i w A B if w = B A w w w + B w T T x
43 42 cbvrabv j 0 ..^ M | Q j w A B if w = B A w w w + B w T T x = i 0 ..^ M | Q i w A B if w = B A w w w + B w T T x
44 40 43 eqtrdi z = x j 0 ..^ M | Q j w A B if w = B A w w w + B w T T z = i 0 ..^ M | Q i w A B if w = B A w w w + B w T T x
45 44 supeq1d z = x sup j 0 ..^ M | Q j w A B if w = B A w w w + B w T T z < = sup i 0 ..^ M | Q i w A B if w = B A w w w + B w T T x <
46 45 cbvmptv z sup j 0 ..^ M | Q j w A B if w = B A w w w + B w T T z < = x sup i 0 ..^ M | Q i w A B if w = B A w w w + B w T T x <
47 1 2 3 4 5 6 7 8 9 10 11 12 13 23 25 32 36 46 fourierdlem100 φ x C D F x 𝐿 1