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 syl6bb ⊢ 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