Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem100 Structured version   Visualization version   GIF version

Theorem fourierdlem100 44437
Description: A piecewise continuous function is integrable on any closed interval. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierlemiblglemlem.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem100.t 𝑇 = (𝐵𝐴)
fourierdlem100.m (𝜑𝑀 ∈ ℕ)
fourierdlem100.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem100.f (𝜑𝐹:ℝ⟶ℂ)
fourierdlem100.per ((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
fourierdlem100.fcn ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
fourierdlem100.r ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
fourierdlem100.l ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
fourierdlem100.c (𝜑𝐶 ∈ ℝ)
fourierdlem100.d (𝜑𝐷 ∈ (𝐶(,)+∞))
fourierdlem100.o 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem100.n 𝑁 = ((♯‘𝐻) − 1)
fourierdlem100.h 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
fourierdlem100.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
fourierdlem100.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
fourierdlem100.j 𝐽 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
fourierdlem100.i 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐽‘(𝐸𝑥))}, ℝ, < ))
Assertion
Ref Expression
fourierdlem100 (𝜑 → (𝑥 ∈ (𝐶[,]𝐷) ↦ (𝐹𝑥)) ∈ 𝐿1)
Distinct variable groups:   𝐴,𝑓,𝑘,𝑦   𝐴,𝑖,𝑥,𝑘,𝑦   𝐴,𝑚,𝑝,𝑖   𝐵,𝑓,𝑘,𝑦   𝐵,𝑖,𝑥   𝐵,𝑚,𝑝   𝐶,𝑓,𝑦   𝐶,𝑖,𝑚,𝑝   𝑥,𝐶   𝐷,𝑓,𝑦   𝐷,𝑖,𝑚,𝑝   𝑥,𝐷   𝑓,𝐸,𝑘,𝑦   𝑖,𝐸,𝑥   𝑖,𝐹,𝑥,𝑦   𝑓,𝐻,𝑦   𝑥,𝐻   𝑓,𝐼,𝑘,𝑦   𝑖,𝐼,𝑥   𝑖,𝐽,𝑥,𝑦   𝑥,𝐿,𝑦   𝑖,𝑀,𝑚,𝑝   𝑥,𝑀,𝑦   𝑓,𝑁,𝑘,𝑦   𝑖,𝑁,𝑥   𝑚,𝑁,𝑝   𝑄,𝑓,𝑘,𝑦   𝑄,𝑖,𝑥   𝑄,𝑝   𝑥,𝑅,𝑦   𝑆,𝑓,𝑘,𝑦   𝑆,𝑖,𝑥   𝑆,𝑝   𝑇,𝑓,𝑘,𝑦   𝑇,𝑖,𝑥   𝜑,𝑓,𝑘,𝑦   𝜑,𝑖,𝑥
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝐶(𝑘)   𝐷(𝑘)   𝑃(𝑥,𝑦,𝑓,𝑖,𝑘,𝑚,𝑝)   𝑄(𝑚)   𝑅(𝑓,𝑖,𝑘,𝑚,𝑝)   𝑆(𝑚)   𝑇(𝑚,𝑝)   𝐸(𝑚,𝑝)   𝐹(𝑓,𝑘,𝑚,𝑝)   𝐻(𝑖,𝑘,𝑚,𝑝)   𝐼(𝑚,𝑝)   𝐽(𝑓,𝑘,𝑚,𝑝)   𝐿(𝑓,𝑖,𝑘,𝑚,𝑝)   𝑀(𝑓,𝑘)   𝑂(𝑥,𝑦,𝑓,𝑖,𝑘,𝑚,𝑝)

Proof of Theorem fourierdlem100
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem100.f . . 3 (𝜑𝐹:ℝ⟶ℂ)
2 fourierdlem100.c . . . 4 (𝜑𝐶 ∈ ℝ)
3 fourierdlem100.d . . . . 5 (𝜑𝐷 ∈ (𝐶(,)+∞))
4 elioore 13294 . . . . 5 (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
53, 4syl 17 . . . 4 (𝜑𝐷 ∈ ℝ)
62, 5iccssred 13351 . . 3 (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
71, 6feqresmpt 6911 . 2 (𝜑 → (𝐹 ↾ (𝐶[,]𝐷)) = (𝑥 ∈ (𝐶[,]𝐷) ↦ (𝐹𝑥)))
8 fourierdlem100.o . . . 4 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
9 fveq2 6842 . . . . . . . . . 10 (𝑖 = 𝑗 → (𝑝𝑖) = (𝑝𝑗))
10 oveq1 7364 . . . . . . . . . . 11 (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
1110fveq2d 6846 . . . . . . . . . 10 (𝑖 = 𝑗 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑗 + 1)))
129, 11breq12d 5118 . . . . . . . . 9 (𝑖 = 𝑗 → ((𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑝𝑗) < (𝑝‘(𝑗 + 1))))
1312cbvralvw 3225 . . . . . . . 8 (∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))
1413anbi2i 623 . . . . . . 7 ((((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1))))
1514a1i 11 . . . . . 6 (𝑝 ∈ (ℝ ↑m (0...𝑚)) → ((((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))))
1615rabbiia 3411 . . . . 5 {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))}
1716mpteq2i 5210 . . . 4 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))})
188, 17eqtri 2764 . . 3 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝𝑗) < (𝑝‘(𝑗 + 1)))})
19 fourierdlem100.t . . . . . 6 𝑇 = (𝐵𝐴)
20 fourierlemiblglemlem.p . . . . . 6 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
21 fourierdlem100.m . . . . . 6 (𝜑𝑀 ∈ ℕ)
22 fourierdlem100.q . . . . . 6 (𝜑𝑄 ∈ (𝑃𝑀))
23 elioo4g 13324 . . . . . . . . 9 (𝐷 ∈ (𝐶(,)+∞) ↔ ((𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐷 ∈ ℝ) ∧ (𝐶 < 𝐷𝐷 < +∞)))
243, 23sylib 217 . . . . . . . 8 (𝜑 → ((𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ*𝐷 ∈ ℝ) ∧ (𝐶 < 𝐷𝐷 < +∞)))
2524simprd 496 . . . . . . 7 (𝜑 → (𝐶 < 𝐷𝐷 < +∞))
2625simpld 495 . . . . . 6 (𝜑𝐶 < 𝐷)
27 id 22 . . . . . . . . . . 11 (𝑦 = 𝑥𝑦 = 𝑥)
2819eqcomi 2745 . . . . . . . . . . . . 13 (𝐵𝐴) = 𝑇
2928oveq2i 7368 . . . . . . . . . . . 12 (𝑘 · (𝐵𝐴)) = (𝑘 · 𝑇)
3029a1i 11 . . . . . . . . . . 11 (𝑦 = 𝑥 → (𝑘 · (𝐵𝐴)) = (𝑘 · 𝑇))
3127, 30oveq12d 7375 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑦 + (𝑘 · (𝐵𝐴))) = (𝑥 + (𝑘 · 𝑇)))
3231eleq1d 2822 . . . . . . . . 9 (𝑦 = 𝑥 → ((𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
3332rexbidv 3175 . . . . . . . 8 (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
3433cbvrabv 3417 . . . . . . 7 {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}
3534uneq2i 4120 . . . . . 6 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
36 fourierdlem100.n . . . . . . 7 𝑁 = ((♯‘𝐻) − 1)
37 fourierdlem100.h . . . . . . . . . 10 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
3829eqcomi 2745 . . . . . . . . . . . . . . . 16 (𝑘 · 𝑇) = (𝑘 · (𝐵𝐴))
3938oveq2i 7368 . . . . . . . . . . . . . . 15 (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑘 · (𝐵𝐴)))
4039eleq1i 2828 . . . . . . . . . . . . . 14 ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄)
4140rexbii 3097 . . . . . . . . . . . . 13 (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄)
4241rgenw 3068 . . . . . . . . . . . 12 𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄)
43 rabbi 3432 . . . . . . . . . . . 12 (∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄) ↔ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})
4442, 43mpbi 229 . . . . . . . . . . 11 {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}
4544uneq2i 4120 . . . . . . . . . 10 ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})
4637, 45eqtri 2764 . . . . . . . . 9 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})
4746fveq2i 6845 . . . . . . . 8 (♯‘𝐻) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))
4847oveq1i 7367 . . . . . . 7 ((♯‘𝐻) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})) − 1)
4936, 48eqtri 2764 . . . . . 6 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})) − 1)
50 fourierdlem100.s . . . . . . 7 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
51 isoeq5 7266 . . . . . . . . 9 (𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}) → (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))))
5246, 51ax-mp 5 . . . . . . . 8 (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})))
5352iotabii 6481 . . . . . . 7 (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})))
5450, 53eqtri 2764 . . . . . 6 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄})))
5519, 20, 21, 22, 2, 5, 26, 8, 35, 49, 54fourierdlem54 44391 . . . . 5 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵𝐴))) ∈ ran 𝑄}))))
5655simpld 495 . . . 4 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
5756simpld 495 . . 3 (𝜑𝑁 ∈ ℕ)
5856simprd 496 . . 3 (𝜑𝑆 ∈ (𝑂𝑁))
591, 6fssresd 6709 . . 3 (𝜑 → (𝐹 ↾ (𝐶[,]𝐷)):(𝐶[,]𝐷)⟶ℂ)
60 ioossicc 13350 . . . . . 6 ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆𝑗)[,](𝑆‘(𝑗 + 1)))
612adantr 481 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
6261rexrd 11205 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ*)
633adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐷 ∈ (𝐶(,)+∞))
6463, 4syl 17 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐷 ∈ ℝ)
6564rexrd 11205 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐷 ∈ ℝ*)
668, 57, 58fourierdlem15 44353 . . . . . . . 8 (𝜑𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
6766adantr 481 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
68 simpr 485 . . . . . . 7 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
6962, 65, 67, 68fourierdlem8 44346 . . . . . 6 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐶[,]𝐷))
7060, 69sstrid 3955 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐶[,]𝐷))
7170resabs1d 5968 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
7221adantr 481 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℕ)
7322adantr 481 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝑄 ∈ (𝑃𝑀))
741adantr 481 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℂ)
75 fourierdlem100.per . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
7675adantlr 713 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
77 fourierdlem100.fcn . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
7877adantlr 713 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
79 fourierdlem100.e . . . . 5 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
80 fourierdlem100.j . . . . 5 𝐽 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
81 eqid 2736 . . . . 5 ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1))))
82 eqid 2736 . . . . 5 (𝐹 ↾ ((𝐽‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1))))) = (𝐹 ↾ ((𝐽‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))
83 eqid 2736 . . . . 5 (𝑦 ∈ (((𝐽‘(𝐸‘(𝑆𝑗))) + ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))))(,)((𝐸‘(𝑆‘(𝑗 + 1))) + ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))))) ↦ ((𝐹 ↾ ((𝐽‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))‘(𝑦 − ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1))))))) = (𝑦 ∈ (((𝐽‘(𝐸‘(𝑆𝑗))) + ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))))(,)((𝐸‘(𝑆‘(𝑗 + 1))) + ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))))) ↦ ((𝐹 ↾ ((𝐽‘(𝐸‘(𝑆𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))))‘(𝑦 − ((𝑆‘(𝑗 + 1)) − (𝐸‘(𝑆‘(𝑗 + 1)))))))
84 fourierdlem100.i . . . . 5 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄𝑖) ≤ (𝐽‘(𝐸𝑥))}, ℝ, < ))
8520, 19, 72, 73, 74, 76, 78, 61, 63, 8, 37, 36, 50, 79, 80, 68, 81, 82, 83, 84fourierdlem90 44427 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
8671, 85eqeltrd 2838 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
87 fourierdlem100.r . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
8887adantlr 713 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
89 eqid 2736 . . . . 5 (𝑖 ∈ (0..^𝑀) ↦ 𝑅) = (𝑖 ∈ (0..^𝑀) ↦ 𝑅)
9020, 19, 72, 73, 74, 76, 78, 88, 61, 63, 8, 37, 36, 50, 79, 80, 68, 81, 84, 89fourierdlem89 44426 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → if((𝐽‘(𝐸‘(𝑆𝑗))) = (𝑄‘(𝐼‘(𝑆𝑗))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘(𝐼‘(𝑆𝑗))), (𝐹‘(𝐽‘(𝐸‘(𝑆𝑗))))) ∈ ((𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
9171eqcomd 2742 . . . . 5 ((𝜑𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))))
9291oveq1d 7372 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)) = (((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
9390, 92eleqtrd 2840 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → if((𝐽‘(𝐸‘(𝑆𝑗))) = (𝑄‘(𝐼‘(𝑆𝑗))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘(𝐼‘(𝑆𝑗))), (𝐹‘(𝐽‘(𝐸‘(𝑆𝑗))))) ∈ (((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆𝑗)))
94 fourierdlem100.l . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
9594adantlr 713 . . . . 5 (((𝜑𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
96 eqid 2736 . . . . 5 (𝑖 ∈ (0..^𝑀) ↦ 𝐿) = (𝑖 ∈ (0..^𝑀) ↦ 𝐿)
9720, 19, 72, 73, 74, 76, 78, 95, 61, 63, 8, 37, 36, 50, 79, 80, 68, 81, 84, 96fourierdlem91 44428 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → if((𝐸‘(𝑆‘(𝑗 + 1))) = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)), ((𝑖 ∈ (0..^𝑀) ↦ 𝐿)‘(𝐼‘(𝑆𝑗))), (𝐹‘(𝐸‘(𝑆‘(𝑗 + 1))))) ∈ ((𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
9891oveq1d 7372 . . . 4 ((𝜑𝑗 ∈ (0..^𝑁)) → ((𝐹 ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))) = (((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
9997, 98eleqtrd 2840 . . 3 ((𝜑𝑗 ∈ (0..^𝑁)) → if((𝐸‘(𝑆‘(𝑗 + 1))) = (𝑄‘((𝐼‘(𝑆𝑗)) + 1)), ((𝑖 ∈ (0..^𝑀) ↦ 𝐿)‘(𝐼‘(𝑆𝑗))), (𝐹‘(𝐸‘(𝑆‘(𝑗 + 1))))) ∈ (((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆𝑗)(,)(𝑆‘(𝑗 + 1)))) lim (𝑆‘(𝑗 + 1))))
10018, 57, 58, 59, 86, 93, 99fourierdlem69 44406 . 2 (𝜑 → (𝐹 ↾ (𝐶[,]𝐷)) ∈ 𝐿1)
1017, 100eqeltrrd 2839 1 (𝜑 → (𝑥 ∈ (𝐶[,]𝐷) ↦ (𝐹𝑥)) ∈ 𝐿1)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  {crab 3407  cun 3908  ifcif 4486  {cpr 4588   class class class wbr 5105  cmpt 5188  ran crn 5634  cres 5635  cio 6446  wf 6492  cfv 6496   Isom wiso 6497  (class class class)co 7357  m cmap 8765  supcsup 9376  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  +∞cpnf 11186  *cxr 11188   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  cz 12499  (,)cioo 13264  (,]cioc 13265  [,]cicc 13267  ...cfz 13424  ..^cfzo 13567  cfl 13695  chash 14230  cnccncf 24239  𝐿1cibl 24981   lim climc 25226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cc 10371  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-symdif 4202  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-ofr 7618  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-omul 8417  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-dju 9837  df-card 9875  df-acn 9878  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-xnn0 12486  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-cn 22578  df-cnp 22579  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-ovol 24828  df-vol 24829  df-mbf 24983  df-itg1 24984  df-itg2 24985  df-ibl 24986  df-itg 24987  df-0p 25034  df-limc 25230
This theorem is referenced by:  fourierdlem105  44442
  Copyright terms: Public domain W3C validator