Step | Hyp | Ref
| Expression |
1 | | fourierdlem105.p |
. 2
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
2 | | fourierdlem105.t |
. 2
⊢ 𝑇 = (𝐵 − 𝐴) |
3 | | fourierdlem105.m |
. 2
⊢ (𝜑 → 𝑀 ∈ ℕ) |
4 | | fourierdlem105.q |
. 2
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
5 | | fourierdlem105.f |
. 2
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
6 | | fourierdlem105.6 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
7 | | fourierdlem105.fcn |
. 2
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
8 | | fourierdlem105.r |
. 2
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
9 | | fourierdlem105.l |
. 2
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
10 | | fourierdlem105.c |
. 2
⊢ (𝜑 → 𝐶 ∈ ℝ) |
11 | | fourierdlem105.d |
. 2
⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞)) |
12 | | eqid 2738 |
. 2
⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ
↑m (0...𝑚))
∣ (((𝑝‘0) =
𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
13 | | eqid 2738 |
. 2
⊢
((♯‘({𝐶,
𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1) |
14 | | oveq1 7177 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑤 + (𝑗 · 𝑇)) = (𝑦 + (𝑗 · 𝑇))) |
15 | 14 | eleq1d 2817 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄)) |
16 | 15 | rexbidv 3207 |
. . . . 5
⊢ (𝑤 = 𝑦 → (∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄)) |
17 | | oveq1 7177 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝑗 · 𝑇) = (𝑘 · 𝑇)) |
18 | 17 | oveq2d 7186 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑦 + (𝑗 · 𝑇)) = (𝑦 + (𝑘 · 𝑇))) |
19 | 18 | eleq1d 2817 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
20 | 19 | cbvrexvw 3350 |
. . . . 5
⊢
(∃𝑗 ∈
ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄) |
21 | 16, 20 | bitrdi 290 |
. . . 4
⊢ (𝑤 = 𝑦 → (∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
22 | 21 | cbvrabv 3393 |
. . 3
⊢ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} |
23 | 22 | uneq2i 4050 |
. 2
⊢ ({𝐶, 𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) |
24 | | isoeq1 7083 |
. . 3
⊢ (𝑔 = 𝑓 → (𝑔 Isom < , <
((0...((♯‘({𝐶,
𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , <
((0...((♯‘({𝐶,
𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})))) |
25 | 24 | cbviotavw 6305 |
. 2
⊢
(℩𝑔𝑔 Isom < , <
((0...((♯‘({𝐶,
𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , <
((0...((♯‘({𝐶,
𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({𝐶, 𝐷} ∪ {𝑤 ∈ (𝐶[,]𝐷) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}))) |
26 | | id 22 |
. . . 4
⊢ (𝑤 = 𝑥 → 𝑤 = 𝑥) |
27 | | oveq2 7178 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (𝐵 − 𝑤) = (𝐵 − 𝑥)) |
28 | 27 | oveq1d 7185 |
. . . . . 6
⊢ (𝑤 = 𝑥 → ((𝐵 − 𝑤) / 𝑇) = ((𝐵 − 𝑥) / 𝑇)) |
29 | 28 | fveq2d 6678 |
. . . . 5
⊢ (𝑤 = 𝑥 → (⌊‘((𝐵 − 𝑤) / 𝑇)) = (⌊‘((𝐵 − 𝑥) / 𝑇))) |
30 | 29 | oveq1d 7185 |
. . . 4
⊢ (𝑤 = 𝑥 → ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) |
31 | 26, 30 | oveq12d 7188 |
. . 3
⊢ (𝑤 = 𝑥 → (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
32 | 31 | cbvmptv 5133 |
. 2
⊢ (𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
33 | | eqeq1 2742 |
. . . 4
⊢ (𝑤 = 𝑦 → (𝑤 = 𝐵 ↔ 𝑦 = 𝐵)) |
34 | | id 22 |
. . . 4
⊢ (𝑤 = 𝑦 → 𝑤 = 𝑦) |
35 | 33, 34 | ifbieq2d 4440 |
. . 3
⊢ (𝑤 = 𝑦 → if(𝑤 = 𝐵, 𝐴, 𝑤) = if(𝑦 = 𝐵, 𝐴, 𝑦)) |
36 | 35 | cbvmptv 5133 |
. 2
⊢ (𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤)) = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) |
37 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → ((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑧) = ((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥)) |
38 | 37 | fveq2d 6678 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑧)) = ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥))) |
39 | 38 | breq2d 5042 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑄‘𝑗) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑧)) ↔ (𝑄‘𝑗) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥)))) |
40 | 39 | rabbidv 3381 |
. . . . 5
⊢ (𝑧 = 𝑥 → {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑧))} = {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥))}) |
41 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑗 = 𝑖 → (𝑄‘𝑗) = (𝑄‘𝑖)) |
42 | 41 | breq1d 5040 |
. . . . . 6
⊢ (𝑗 = 𝑖 → ((𝑄‘𝑗) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥)) ↔ (𝑄‘𝑖) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥)))) |
43 | 42 | cbvrabv 3393 |
. . . . 5
⊢ {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥))} |
44 | 40, 43 | eqtrdi 2789 |
. . . 4
⊢ (𝑧 = 𝑥 → {𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑧))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥))}) |
45 | 44 | supeq1d 8983 |
. . 3
⊢ (𝑧 = 𝑥 → sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑧))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < )) |
46 | 45 | cbvmptv 5133 |
. 2
⊢ (𝑧 ∈ ℝ ↦
sup({𝑗 ∈ (0..^𝑀) ∣ (𝑄‘𝑗) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑧))}, ℝ, < )) = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ ((𝑤 ∈ (𝐴(,]𝐵) ↦ if(𝑤 = 𝐵, 𝐴, 𝑤))‘((𝑤 ∈ ℝ ↦ (𝑤 + ((⌊‘((𝐵 − 𝑤) / 𝑇)) · 𝑇)))‘𝑥))}, ℝ, < )) |
47 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 23, 25, 32, 36, 46 | fourierdlem100 43289 |
1
⊢ (𝜑 → (𝑥 ∈ (𝐶[,]𝐷) ↦ (𝐹‘𝑥)) ∈
𝐿1) |