Theorem fourierdlem100 46634

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.

Step	Hyp	Ref	Expression
1		fourierdlem100.f	. . 3 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
2		fourierdlem100.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
3		fourierdlem100.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
4		elioore 13328	. . . . 5 ⊢ (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → 𝐷 ∈ ℝ)
6	2, 5	iccssred 13387	. . 3 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
7	1, 6	feqresmpt 6909	. 2 ⊢ (𝜑 → (𝐹 ↾ (𝐶[,]𝐷)) = (𝑥 ∈ (𝐶[,]𝐷) ↦ (𝐹‘𝑥)))
8		fourierdlem100.o	. . . 4 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
9		fveq2 6840	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → (𝑝‘𝑖) = (𝑝‘𝑗))
10		oveq1 7374	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
11	10	fveq2d 6844	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑗 + 1)))
12	9, 11	breq12d 5098	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
13	12	cbvralvw 3215	. . . . . . . 8 ⊢ (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))
14	13	anbi2i 624	. . . . . . 7 ⊢ ((((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1))))
15	14	a1i 11	. . . . . 6 ⊢ (𝑝 ∈ (ℝ ↑m (0...𝑚)) → ((((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))))
16	15	rabbiia 3393	. . . . 5 ⊢ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))}
17	16	mpteq2i 5181	. . . 4 ⊢ (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑗 ∈ (0..^𝑚)(𝑝‘𝑗) < (𝑝‘(𝑗 + 1)))})
18	8, 17	eqtri 2759	. . 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 13359	. . . . . . . . 9 ⊢ (𝐷 ∈ (𝐶(,)+∞) ↔ ((𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ) ∧ (𝐶 < 𝐷 ∧ 𝐷 < +∞)))
24	3, 23	sylib 218	. . . . . . . 8 ⊢ (𝜑 → ((𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ) ∧ (𝐶 < 𝐷 ∧ 𝐷 < +∞)))
25	24	simprd 495	. . . . . . 7 ⊢ (𝜑 → (𝐶 < 𝐷 ∧ 𝐷 < +∞))
26	25	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝐶 < 𝐷)
27		id 22	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥)
28	19	eqcomi 2745	. . . . . . . . . . . . 13 ⊢ (𝐵 − 𝐴) = 𝑇
29	28	oveq2i 7378	. . . . . . . . . . . 12 ⊢ (𝑘 · (𝐵 − 𝐴)) = (𝑘 · 𝑇)
30	29	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (𝑘 · (𝐵 − 𝐴)) = (𝑘 · 𝑇))
31	27, 30	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑦 + (𝑘 · (𝐵 − 𝐴))) = (𝑥 + (𝑘 · 𝑇)))
32	31	eleq1d 2821	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
33	32	rexbidv 3161	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
34	33	cbvrabv 3399	. . . . . . 7 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}
35	34	uneq2i 4105	. . . . . 6 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
36		fourierdlem100.n	. . . . . . 7 ⊢ 𝑁 = ((♯‘𝐻) − 1)
37		fourierdlem100.h	. . . . . . . . . 10 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
38	29	eqcomi 2745	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 · 𝑇) = (𝑘 · (𝐵 − 𝐴))
39	38	oveq2i 7378	. . . . . . . . . . . . . . 15 ⊢ (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑘 · (𝐵 − 𝐴)))
40	39	eleq1i 2827	. . . . . . . . . . . . . 14 ⊢ ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
41	40	rexbii 3084	. . . . . . . . . . . . 13 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
42	41	rgenw 3055	. . . . . . . . . . . 12 ⊢ ∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
43		rabbi 3419	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄) ↔ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
44	42, 43	mpbi 230	. . . . . . . . . . 11 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}
45	44	uneq2i 4105	. . . . . . . . . 10 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
46	37, 45	eqtri 2759	. . . . . . . . 9 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
47	46	fveq2i 6843	. . . . . . . 8 ⊢ (♯‘𝐻) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
48	47	oveq1i 7377	. . . . . . 7 ⊢ ((♯‘𝐻) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
49	36, 48	eqtri 2759	. . . . . 6 ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
50		fourierdlem100.s	. . . . . . 7 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
51		isoeq5 7276	. . . . . . . . 9 ⊢ (𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) → (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))))
52	46, 51	ax-mp 5	. . . . . . . 8 ⊢ (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
53	52	iotabii 6483	. . . . . . 7 ⊢ (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
54	50, 53	eqtri 2759	. . . . . 6 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
55	19, 20, 21, 22, 2, 5, 26, 8, 35, 49, 54	fourierdlem54 46588	. . . . 5 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))))
56	55	simpld 494	. . . 4 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
57	56	simpld 494	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
58	56	simprd 495	. . 3 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
59	1, 6	fssresd 6707	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐶[,]𝐷)):(𝐶[,]𝐷)⟶ℂ)
60		ioossicc 13386	. . . . . 6 ⊢ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1)))
61	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ)
62	61	rexrd 11195	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐶 ∈ ℝ*)
63	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐷 ∈ (𝐶(,)+∞))
64	63, 4	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐷 ∈ ℝ)
65	64	rexrd 11195	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐷 ∈ ℝ*)
66	8, 57, 58	fourierdlem15 46550	. . . . . . . 8 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
67	66	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
68		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
69	62, 65, 67, 68	fourierdlem8 46543	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)[,](𝑆‘(𝑗 + 1))) ⊆ (𝐶[,]𝐷))
70	60, 69	sstrid 3933	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ (𝐶[,]𝐷))
71	70	resabs1d 5973	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = (𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
72	21	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℕ)
73	22	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑄 ∈ (𝑃‘𝑀))
74	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐹:ℝ⟶ℂ)
75		fourierdlem100.per	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
76	75	adantlr 716	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
77		fourierdlem100.fcn	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
78	77	adantlr 716	. . . . 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..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐽‘(𝐸‘𝑥))}, ℝ, < ))
85	20, 19, 72, 73, 74, 76, 78, 61, 63, 8, 37, 36, 50, 79, 80, 68, 81, 82, 83, 84	fourierdlem90 46624	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
86	71, 85	eqeltrd 2836	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
87		fourierdlem100.r	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)))
88	87	adantlr 716	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)))
89		eqid 2736	. . . . 5 ⊢ (𝑖 ∈ (0..^𝑀) ↦ 𝑅) = (𝑖 ∈ (0..^𝑀) ↦ 𝑅)
90	20, 19, 72, 73, 74, 76, 78, 88, 61, 63, 8, 37, 36, 50, 79, 80, 68, 81, 84, 89	fourierdlem89 46623	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if((𝐽‘(𝐸‘(𝑆‘𝑗))) = (𝑄‘(𝐼‘(𝑆‘𝑗))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘(𝐼‘(𝑆‘𝑗))), (𝐹‘(𝐽‘(𝐸‘(𝑆‘𝑗))))) ∈ ((𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘𝑗)))
91	71	eqcomd 2742	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) = ((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))))
92	91	oveq1d 7382	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘𝑗)) = (((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘𝑗)))
93	90, 92	eleqtrd 2838	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if((𝐽‘(𝐸‘(𝑆‘𝑗))) = (𝑄‘(𝐼‘(𝑆‘𝑗))), ((𝑖 ∈ (0..^𝑀) ↦ 𝑅)‘(𝐼‘(𝑆‘𝑗))), (𝐹‘(𝐽‘(𝐸‘(𝑆‘𝑗))))) ∈ (((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘𝑗)))
94		fourierdlem100.l	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))
95	94	adantlr 716	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))
96		eqid 2736	. . . . 5 ⊢ (𝑖 ∈ (0..^𝑀) ↦ 𝐿) = (𝑖 ∈ (0..^𝑀) ↦ 𝐿)
97	20, 19, 72, 73, 74, 76, 78, 95, 61, 63, 8, 37, 36, 50, 79, 80, 68, 81, 84, 96	fourierdlem91 46625	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if((𝐸‘(𝑆‘(𝑗 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)), ((𝑖 ∈ (0..^𝑀) ↦ 𝐿)‘(𝐼‘(𝑆‘𝑗))), (𝐹‘(𝐸‘(𝑆‘(𝑗 + 1))))) ∈ ((𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘(𝑗 + 1))))
98	91	oveq1d 7382	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐹 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘(𝑗 + 1))) = (((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘(𝑗 + 1))))
99	97, 98	eleqtrd 2838	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if((𝐸‘(𝑆‘(𝑗 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)), ((𝑖 ∈ (0..^𝑀) ↦ 𝐿)‘(𝐼‘(𝑆‘𝑗))), (𝐹‘(𝐸‘(𝑆‘(𝑗 + 1))))) ∈ (((𝐹 ↾ (𝐶[,]𝐷)) ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘(𝑗 + 1))))
100	18, 57, 58, 59, 86, 93, 99	fourierdlem69 46603	. 2 ⊢ (𝜑 → (𝐹 ↾ (𝐶[,]𝐷)) ∈ 𝐿1)
101	7, 100	eqeltrrd 2837	1 ⊢ (𝜑 → (𝑥 ∈ (𝐶[,]𝐷) ↦ (𝐹‘𝑥)) ∈ 𝐿1)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061  {crab 3389   ∪ cun 3887  ifcif 4466  {cpr 4569   class class class wbr 5085   ↦ cmpt 5166  ran crn 5632   ↾ cres 5633  ℩cio 6452  ⟶wf 6494  ‘cfv 6498   Isom wiso 6499  (class class class)co 7367   ↑_m cmap 8773  supcsup 9353  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043  +∞cpnf 11176  ℝ^*cxr 11178   < clt 11179   ≤ cle 11180   − cmin 11377   / cdiv 11807  ℕcn 12174  ℤcz 12524  (,)cioo 13298  (,]cioc 13299  [,]cicc 13301  ...cfz 13461  ..^cfzo 13608  ⌊cfl 13749  ♯chash 14292  –cn→ccncf 24843  𝐿¹cibl 25584   lim_ℂ climc 25829

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-inf2 9562  ax-cc 10357  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-addf 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-symdif 4193  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-iin 4936  df-disj 5053  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-ofr 7632  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-oadd 8409  df-omul 8410  df-er 8643  df-map 8775  df-pm 8776  df-ixp 8846  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-fi 9324  df-sup 9355  df-inf 9356  df-oi 9425  df-dju 9825  df-card 9863  df-acn 9866  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-xnn0 12511  df-z 12525  df-dec 12645  df-uz 12789  df-q 12899  df-rp 12943  df-xneg 13063  df-xadd 13064  df-xmul 13065  df-ioo 13302  df-ioc 13303  df-ico 13304  df-icc 13305  df-fz 13462  df-fzo 13609  df-fl 13751  df-mod 13829  df-seq 13964  df-exp 14024  df-hash 14293  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198  df-limsup 15433  df-clim 15450  df-rlim 15451  df-sum 15649  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-starv 17235  df-sca 17236  df-vsca 17237  df-ip 17238  df-tset 17239  df-ple 17240  df-ds 17242  df-unif 17243  df-hom 17244  df-cco 17245  df-rest 17385  df-topn 17386  df-0g 17404  df-gsum 17405  df-topgen 17406  df-pt 17407  df-prds 17410  df-xrs 17466  df-qtop 17471  df-imas 17472  df-xps 17474  df-mre 17548  df-mrc 17549  df-acs 17551  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-submnd 18752  df-mulg 19044  df-cntz 19292  df-cmn 19757  df-psmet 21344  df-xmet 21345  df-met 21346  df-bl 21347  df-mopn 21348  df-cnfld 21353  df-top 22859  df-topon 22876  df-topsp 22898  df-bases 22911  df-cld 22984  df-ntr 22985  df-cls 22986  df-nei 23063  df-lp 23101  df-cn 23192  df-cnp 23193  df-cmp 23352  df-tx 23527  df-hmeo 23720  df-xms 24285  df-ms 24286  df-tms 24287  df-cncf 24845  df-ovol 25431  df-vol 25432  df-mbf 25586  df-itg1 25587  df-itg2 25588  df-ibl 25589  df-itg 25590  df-0p 25637  df-limc 25833

This theorem is referenced by:  fourierdlem105  46639