fourierdlem113 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem113 46257

Description: Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem113.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem113.t	⊢ 𝑇 = (2 · π)
fourierdlem113.per	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
fourierdlem113.x	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem113.l	⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
fourierdlem113.r	⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
fourierdlem113.p	⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem113.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem113.q	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem113.dvcn	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
fourierdlem113.dvlb	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
fourierdlem113.dvub	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
fourierdlem113.a	⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem113.b	⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem113.15	⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
fourierdlem113.e	⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
fourierdlem113.exq	⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄)

**Assertion**
Ref	Expression
fourierdlem113	⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))

Distinct variable groups: 𝐴,𝑛 𝐵,𝑛 𝑥,𝐸 𝑖,𝐹,𝑛,𝑥 𝑖,𝐿,𝑛 𝑖,𝑀,𝑥,𝑛 𝑀,𝑝,𝑖,𝑛 𝑄,𝑖,𝑥,𝑛 𝑄,𝑝 𝑅,𝑖,𝑛 𝑇,𝑖,𝑥,𝑛 𝑇,𝑝 𝑖,𝑋,𝑥,𝑛 𝑋,𝑝 𝜑,𝑖,𝑥,𝑛 Allowed substitution hints: 𝜑(𝑝) 𝐴(𝑥,𝑖,𝑝) 𝐵(𝑥,𝑖,𝑝) 𝑃(𝑥,𝑖,𝑛,𝑝) 𝑅(𝑥,𝑝) 𝑆(𝑥,𝑖,𝑛,𝑝) 𝐸(𝑖,𝑛,𝑝) 𝐹(𝑝) 𝐿(𝑥,𝑝)

Proof of Theorem fourierdlem113 Dummy variables 𝑗 𝑘 𝑚 𝑤 𝑦 𝑡 𝑢 𝑧 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem113.f	. 2 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
2		oveq1 7348	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (𝑤 mod (2 · π)) = (𝑦 mod (2 · π)))
3	2	eqeq1d 2733	. . . . . 6 ⊢ (𝑤 = 𝑦 → ((𝑤 mod (2 · π)) = 0 ↔ (𝑦 mod (2 · π)) = 0))
4		oveq2 7349	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → ((𝑘 + (1 / 2)) · 𝑤) = ((𝑘 + (1 / 2)) · 𝑦))
5	4	fveq2d 6821	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (sin‘((𝑘 + (1 / 2)) · 𝑤)) = (sin‘((𝑘 + (1 / 2)) · 𝑦)))
6		oveq1 7348	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (𝑤 / 2) = (𝑦 / 2))
7	6	fveq2d 6821	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (sin‘(𝑤 / 2)) = (sin‘(𝑦 / 2)))
8	7	oveq2d 7357	. . . . . . 7 ⊢ (𝑤 = 𝑦 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑦 / 2))))
9	5, 8	oveq12d 7359	. . . . . 6 ⊢ (𝑤 = 𝑦 → ((sin‘((𝑘 + (1 / 2)) · 𝑤)) / ((2 · π) · (sin‘(𝑤 / 2)))) = ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
10	3, 9	ifbieq2d 4497	. . . . 5 ⊢ (𝑤 = 𝑦 → if((𝑤 mod (2 · π)) = 0, (((2 · 𝑘) + 1) / (2 · π)), ((sin‘((𝑘 + (1 / 2)) · 𝑤)) / ((2 · π) · (sin‘(𝑤 / 2))))) = if((𝑦 mod (2 · π)) = 0, (((2 · 𝑘) + 1) / (2 · π)), ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))))
11	10	cbvmptv 5190	. . . 4 ⊢ (𝑤 ∈ ℝ ↦ if((𝑤 mod (2 · π)) = 0, (((2 · 𝑘) + 1) / (2 · π)), ((sin‘((𝑘 + (1 / 2)) · 𝑤)) / ((2 · π) · (sin‘(𝑤 / 2)))))) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑘) + 1) / (2 · π)), ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))))
12		oveq2 7349	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (2 · 𝑘) = (2 · 𝑚))
13	12	oveq1d 7356	. . . . . . 7 ⊢ (𝑘 = 𝑚 → ((2 · 𝑘) + 1) = ((2 · 𝑚) + 1))
14	13	oveq1d 7356	. . . . . 6 ⊢ (𝑘 = 𝑚 → (((2 · 𝑘) + 1) / (2 · π)) = (((2 · 𝑚) + 1) / (2 · π)))
15		oveq1 7348	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝑘 + (1 / 2)) = (𝑚 + (1 / 2)))
16	15	oveq1d 7356	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → ((𝑘 + (1 / 2)) · 𝑦) = ((𝑚 + (1 / 2)) · 𝑦))
17	16	fveq2d 6821	. . . . . . 7 ⊢ (𝑘 = 𝑚 → (sin‘((𝑘 + (1 / 2)) · 𝑦)) = (sin‘((𝑚 + (1 / 2)) · 𝑦)))
18	17	oveq1d 7356	. . . . . 6 ⊢ (𝑘 = 𝑚 → ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
19	14, 18	ifeq12d 4492	. . . . 5 ⊢ (𝑘 = 𝑚 → if((𝑦 mod (2 · π)) = 0, (((2 · 𝑘) + 1) / (2 · π)), ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))) = if((𝑦 mod (2 · π)) = 0, (((2 · 𝑚) + 1) / (2 · π)), ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2))))))
20	19	mpteq2dv 5180	. . . 4 ⊢ (𝑘 = 𝑚 → (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑘) + 1) / (2 · π)), ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑚) + 1) / (2 · π)), ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
21	11, 20	eqtrid 2778	. . 3 ⊢ (𝑘 = 𝑚 → (𝑤 ∈ ℝ ↦ if((𝑤 mod (2 · π)) = 0, (((2 · 𝑘) + 1) / (2 · π)), ((sin‘((𝑘 + (1 / 2)) · 𝑤)) / ((2 · π) · (sin‘(𝑤 / 2)))))) = (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑚) + 1) / (2 · π)), ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
22	21	cbvmptv 5190	. 2 ⊢ (𝑘 ∈ ℕ ↦ (𝑤 ∈ ℝ ↦ if((𝑤 mod (2 · π)) = 0, (((2 · 𝑘) + 1) / (2 · π)), ((sin‘((𝑘 + (1 / 2)) · 𝑤)) / ((2 · π) · (sin‘(𝑤 / 2))))))) = (𝑚 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑚) + 1) / (2 · π)), ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))
23		fourierdlem113.p	. 2 ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
24		fourierdlem113.m	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
25		fourierdlem113.q	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
26		oveq1 7348	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (𝑤 + (𝑗 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
27	26	eleq1d 2816	. . . . . . 7 ⊢ (𝑤 = 𝑦 → ((𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
28	27	rexbidv 3156	. . . . . 6 ⊢ (𝑤 = 𝑦 → (∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
29	28	cbvrabv 3405	. . . . 5 ⊢ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
30	29	uneq2i 4110	. . . 4 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
31	30	fveq2i 6820	. . 3 ⊢ (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) = (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
32	31	oveq1i 7351	. 2 ⊢ ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
33		oveq1 7348	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
34	33	oveq2d 7357	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑗 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
35	34	eleq1d 2816	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
36	35	cbvrexvw 3211	. . . . . . . . 9 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄)
37	36	a1i 11	. . . . . . . 8 ⊢ (𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
38	37	rabbiia 3399	. . . . . . 7 ⊢ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
39	38	uneq2i 4110	. . . . . 6 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
40		isoeq5 7250	. . . . . 6 ⊢ (({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}) → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
41	39, 40	ax-mp 5	. . . . 5 ⊢ (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
42	41	a1i 11	. . . 4 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
43	33	oveq2d 7357	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → (𝑤 + (𝑘 · 𝑇)) = (𝑤 + (𝑗 · 𝑇)))
44	43	eleq1d 2816	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → ((𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
45	44	cbvrexvw 3211	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄)
46	45	a1i 11	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) → (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
47	46	rabbiia 3399	. . . . . . . . . 10 ⊢ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}
48	47	uneq2i 4110	. . . . . . . . 9 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})
49	48	fveq2i 6820	. . . . . . . 8 ⊢ (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
50	49	oveq1i 7351	. . . . . . 7 ⊢ ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
51	50	oveq2i 7352	. . . . . 6 ⊢ (0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)) = (0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1))
52		isoeq4 7249	. . . . . 6 ⊢ ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)) = (0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)) → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
53	51, 52	ax-mp 5	. . . . 5 ⊢ (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
54	53	a1i 11	. . . 4 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
55		isoeq1 7246	. . . 4 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
56	42, 54, 55	3bitrd 305	. . 3 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
57	56	cbviotavw 6440	. 2 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
58		fourierdlem113.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℝ)
59		pire 26388	. . . . 5 ⊢ π ∈ ℝ
60	59	renegcli 11417	. . . 4 ⊢ -π ∈ ℝ
61	60	a1i 11	. . 3 ⊢ (𝜑 → -π ∈ ℝ)
62	59	a1i 11	. . 3 ⊢ (𝜑 → π ∈ ℝ)
63		negpilt0 45322	. . . 4 ⊢ -π < 0
64	63	a1i 11	. . 3 ⊢ (𝜑 → -π < 0)
65		pipos 26390	. . . 4 ⊢ 0 < π
66	65	a1i 11	. . 3 ⊢ (𝜑 → 0 < π)
67		picn 26389	. . . . 5 ⊢ π ∈ ℂ
68	67	2timesi 12253	. . . 4 ⊢ (2 · π) = (π + π)
69		fourierdlem113.t	. . . 4 ⊢ 𝑇 = (2 · π)
70	67, 67	subnegi 11435	. . . 4 ⊢ (π − -π) = (π + π)
71	68, 69, 70	3eqtr4i 2764	. . 3 ⊢ 𝑇 = (π − -π)
72	23	fourierdlem2 46147	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
73	24, 72	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
74	25, 73	mpbid 232	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
75	74	simpld 494	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
76		elmapi 8768	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
77	75, 76	syl 17	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
78		fzfid 13875	. . . 4 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
79		rnffi 45212	. . . 4 ⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin)
80	77, 78, 79	syl2anc 584	. . 3 ⊢ (𝜑 → ran 𝑄 ∈ Fin)
81	23, 24, 25	fourierdlem15 46160	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
82		frn 6653	. . . 4 ⊢ (𝑄:(0...𝑀)⟶(-π[,]π) → ran 𝑄 ⊆ (-π[,]π))
83	81, 82	syl 17	. . 3 ⊢ (𝜑 → ran 𝑄 ⊆ (-π[,]π))
84	74	simprd 495	. . . . 5 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
85	84	simplrd 769	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = π)
86		ffun 6649	. . . . . 6 ⊢ (𝑄:(0...𝑀)⟶(-π[,]π) → Fun 𝑄)
87	81, 86	syl 17	. . . . 5 ⊢ (𝜑 → Fun 𝑄)
88	24	nnnn0d 12437	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
89		nn0uz 12769	. . . . . . . 8 ⊢ ℕ₀ = (ℤ_≥‘0)
90	88, 89	eleqtrdi 2841	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
91		eluzfz2 13427	. . . . . . 7 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
92	90, 91	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
93		fdm 6655	. . . . . . . 8 ⊢ (𝑄:(0...𝑀)⟶(-π[,]π) → dom 𝑄 = (0...𝑀))
94	81, 93	syl 17	. . . . . . 7 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
95	94	eqcomd 2737	. . . . . 6 ⊢ (𝜑 → (0...𝑀) = dom 𝑄)
96	92, 95	eleqtrd 2833	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ dom 𝑄)
97		fvelrn 7004	. . . . 5 ⊢ ((Fun 𝑄 ∧ 𝑀 ∈ dom 𝑄) → (𝑄‘𝑀) ∈ ran 𝑄)
98	87, 96, 97	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
99	85, 98	eqeltrrd 2832	. . 3 ⊢ (𝜑 → π ∈ ran 𝑄)
100		fourierdlem113.e	. . 3 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
101		fourierdlem113.exq	. . 3 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄)
102		eqid 2731	. . 3 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
103		isoeq1 7246	. . . . 5 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
104	30, 48, 39	3eqtr4ri 2765	. . . . . 6 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
105		isoeq5 7250	. . . . . 6 ⊢ (({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) → (𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
106	104, 105	ax-mp 5	. . . . 5 ⊢ (𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
107	103, 106	bitrdi 287	. . . 4 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
108	107	cbviotavw 6440	. . 3 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
109		eqid 2731	. . 3 ⊢ {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
110	61, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109	fourierdlem51 46195	. 2 ⊢ (𝜑 → 𝑋 ∈ ran (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
111		fourierdlem113.per	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
112		ax-resscn 11058	. . . 4 ⊢ ℝ ⊆ ℂ
113	112	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℂ)
114		ioossre 13302	. . . . . . 7 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
115	114	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
116	1, 115	fssresd 6685	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
117	112	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
118	116, 117	fssd 6663	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
119	118	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
120	114	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
121	1, 117	fssd 6663	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
122	121	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
123		ssid 3952	. . . . . . 7 ⊢ ℝ ⊆ ℝ
124	123	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℝ)
125		eqid 2731	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
126		tgioo4 24715	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
127	125, 126	dvres 25834	. . . . . 6 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
128	113, 122, 124, 120, 127	syl22anc 838	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
129	128	dmeqd 5840	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
130		ioontr 45551	. . . . . . 7 ⊢ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))
131	130	reseq2i 5920	. . . . . 6 ⊢ ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
132	131	dmeqi 5839	. . . . 5 ⊢ dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
133	132	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
134		fourierdlem113.dvcn	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
135		cncff 24808	. . . . 5 ⊢ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
136		fdm 6655	. . . . 5 ⊢ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
137	134, 135, 136	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
138	129, 133, 137	3eqtrd 2770	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
139		dvcn 25845	. . 3 ⊢ (((ℝ ⊆ ℂ ∧ (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ) ∧ dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
140	113, 119, 120, 138, 139	syl31anc 1375	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
141	120, 113	sstrd 3940	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
142	77	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
143		fzofzp1 13659	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
144	143	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
145	142, 144	ffvelcdmd 7013	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
146	145	rexrd 11157	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
147		elfzofz 13570	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
148	147	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
149	142, 148	ffvelcdmd 7013	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
150	74	simprrd 773	. . . . 5 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
151	150	r19.21bi 3224	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
152	125, 146, 149, 151	lptioo1cn 45684	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
153	116	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
154	123	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ ⊆ ℝ)
155	117, 121, 154	dvbss 25824	. . . . . . 7 ⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ ℝ)
156		dvfre 25877	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
157	1, 154, 156	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
158		0re 11109	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
159	60, 158, 59	lttri 11234	. . . . . . . . 9 ⊢ ((-π < 0 ∧ 0 < π) → -π < π)
160	63, 65, 159	mp2an 692	. . . . . . . 8 ⊢ -π < π
161	160	a1i 11	. . . . . . 7 ⊢ (𝜑 → -π < π)
162	84	simplld 767	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) = -π)
163	134, 135	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
164		fourierdlem113.dvlb	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
165	163, 141, 152, 164, 125	ellimciota 45654	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
166	149	rexrd 11157	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
167	125, 166, 145, 151	lptioo2cn 45683	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
168		fourierdlem113.dvub	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
169	163, 141, 167, 168, 125	ellimciota 45654	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
170	121	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
171		zre 12467	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
172	171	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
173		2re 12194	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
174	173, 59	remulcli 11123	. . . . . . . . . . . . . 14 ⊢ (2 · π) ∈ ℝ
175	174	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · π) ∈ ℝ)
176	69, 175	eqeltrid 2835	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℝ)
177	176	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
178	172, 177	remulcld 11137	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
179	170	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
180	177	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℝ)
181		simplr 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑘 ∈ ℤ)
182		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
183	111	ad4ant14 752	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
184	179, 180, 181, 182, 183	fperiodmul 45345	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹‘𝑡))
185		eqid 2731	. . . . . . . . . 10 ⊢ (ℝ D 𝐹) = (ℝ D 𝐹)
186	170, 178, 184, 185	fperdvper 45957	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ dom (ℝ D 𝐹)) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡)))
187	186	an32s 652	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡)))
188	187	simpld 494	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹))
189	187	simprd 495	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡))
190		fveq2 6817	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑄‘𝑗) = (𝑄‘𝑖))
191		oveq1 7348	. . . . . . . . . 10 ⊢ (𝑗 = 𝑖 → (𝑗 + 1) = (𝑖 + 1))
192	191	fveq2d 6821	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑄‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)))
193	190, 192	oveq12d 7359	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
194	193	cbvmptv 5190	. . . . . . 7 ⊢ (𝑗 ∈ (0..^𝑀) ↦ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1)))) = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
195		eqid 2731	. . . . . . 7 ⊢ (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇))) = (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇)))
196	155, 157, 61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195	fourierdlem71 46215	. . . . . 6 ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
197	196	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
198		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0..^𝑀))
199		nfra1 3256	. . . . . . . . 9 ⊢ Ⅎ𝑡∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧
200	198, 199	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
201	128, 131	eqtrdi 2782	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
202	201	fveq1d 6819	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡))
203		fvres 6836	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
204	202, 203	sylan9eq 2786	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
205	204	fveq2d 6821	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡)))
206	205	adantlr 715	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡)))
207		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
208		ssdmres 5957	. . . . . . . . . . . . . 14 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
209	137, 208	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹))
210	209	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹))
211		simpr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
212	210, 211	sseldd 3930	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ dom (ℝ D 𝐹))
213		rspa 3221	. . . . . . . . . . 11 ⊢ ((∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
214	207, 212, 213	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
215	206, 214	eqbrtrd 5108	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
216	215	ex 412	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
217	200, 216	ralrimi 3230	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) → ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
218	217	ex 412	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 → ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
219	218	reximdv 3147	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
220	197, 219	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
221	149, 145, 153, 138, 220	ioodvbdlimc1 45971	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
222	119, 141, 152, 221, 125	ellimciota 45654	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
223	149, 145, 153, 138, 220	ioodvbdlimc2 45973	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
224	119, 141, 167, 223, 125	ellimciota 45654	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
225		frel 6651	. . . . . . 7 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ → Rel (ℝ D 𝐹))
226	157, 225	syl 17	. . . . . 6 ⊢ (𝜑 → Rel (ℝ D 𝐹))
227		resindm 5974	. . . . . 6 ⊢ (Rel (ℝ D 𝐹) → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
228	226, 227	syl 17	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
229		inss2 4183	. . . . . . 7 ⊢ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
230	229	a1i 11	. . . . . 6 ⊢ (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
231	157, 230	fssresd 6685	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
232	228, 231	feq1dd 6629	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
233	232, 117	fssd 6663	. . 3 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℂ)
234		ioosscn 13303	. . . . 5 ⊢ (-∞(,)𝑋) ⊆ ℂ
235		ssinss1 4191	. . . . 5 ⊢ ((-∞(,)𝑋) ⊆ ℂ → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
236	234, 235	ax-mp 5	. . . 4 ⊢ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ
237	236	a1i 11	. . 3 ⊢ (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
238		3simpb 1149	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → (𝜑 ∧ 𝑘 ∈ ℤ))
239		simp2 1137	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ dom (ℝ D 𝐹))
240	170	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
241	177	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
242		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℤ)
243		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
244		eleq1w 2814	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℝ ↔ 𝑦 ∈ ℝ))
245	244	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ 𝑦 ∈ ℝ)))
246		oveq1 7348	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
247	246	fveq2d 6821	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
248		fveq2 6817	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
249	247, 248	eqeq12d 2747	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)))
250	245, 249	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))))
251	250, 111	chvarvv 1990	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))
252	251	ad4ant14 752	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))
253	240, 241, 242, 243, 252	fperiodmul 45345	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))
254	170, 178, 253, 185	fperdvper 45957	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥)))
255	238, 239, 254	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥)))
256	255	simpld 494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹))
257		oveq2 7349	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (π − 𝑤) = (π − 𝑥))
258	257	oveq1d 7356	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((π − 𝑤) / 𝑇) = ((π − 𝑥) / 𝑇))
259	258	fveq2d 6821	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (⌊‘((π − 𝑤) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
260	259	oveq1d 7356	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
261	260	cbvmptv 5190	. . . . . 6 ⊢ (𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
262		eqid 2731	. . . . . 6 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥)))
263	61, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209	fourierdlem41 46186	. . . . 5 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))))
264	263	simpld 494	. . . 4 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)))
265	125	cnfldtop 24693	. . . . . . . . 9 ⊢ (TopOpen‘ℂ_fld) ∈ Top
266	265	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (TopOpen‘ℂ_fld) ∈ Top)
267	236	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
268		mnfxr 11164	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
269	268	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → -∞ ∈ ℝ^*)
270		rexr 11153	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℝ^*)
271		mnflt 13017	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → -∞ < 𝑦)
272	269, 270, 271	xrltled 13044	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → -∞ ≤ 𝑦)
273		iooss1 13275	. . . . . . . . . . 11 ⊢ ((-∞ ∈ ℝ^* ∧ -∞ ≤ 𝑦) → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
274	269, 272, 273	syl2anc 584	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
275	274	3ad2ant2 1134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
276		simp3 1138	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))
277	275, 276	ssind 4186	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)))
278		unicntop 24695	. . . . . . . . 9 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
279	278	lpss3 23054	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ ∧ (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
280	266, 267, 277, 279	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
281	280	3adant3l 1181	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
282	270	3ad2ant2 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑦 ∈ ℝ^*)
283	58	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ℝ)
284		simp3l 1202	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑦 < 𝑋)
285	125, 282, 283, 284	lptioo2cn 45683	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)))
286	281, 285	sseldd 3930	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
287	286	rexlimdv3a 3137	. . . 4 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)))))
288	264, 287	mpd 15	. . 3 ⊢ (𝜑 → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
289	255	simprd 495	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥))
290		oveq2 7349	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (π − 𝑦) = (π − 𝑥))
291	290	oveq1d 7356	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((π − 𝑦) / 𝑇) = ((π − 𝑥) / 𝑇))
292	291	fveq2d 6821	. . . . . 6 ⊢ (𝑦 = 𝑥 → (⌊‘((π − 𝑦) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
293	292	oveq1d 7356	. . . . 5 ⊢ (𝑦 = 𝑥 → ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
294	293	cbvmptv 5190	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
295		id 22	. . . . . 6 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
296		fveq2 6817	. . . . . 6 ⊢ (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧) = ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥))
297	295, 296	oveq12d 7359	. . . . 5 ⊢ (𝑧 = 𝑥 → (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧)) = (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
298	297	cbvmptv 5190	. . . 4 ⊢ (𝑧 ∈ ℝ ↦ (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
299	61, 62, 161, 23, 71, 24, 25, 155, 157, 256, 289, 134, 169, 58, 294, 298	fourierdlem49 46193	. . 3 ⊢ (𝜑 → (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ≠ ∅)
300	233, 237, 288, 299, 125	ellimciota 45654	. 2 ⊢ (𝜑 → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋)) ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
301		resindm 5974	. . . . . 6 ⊢ (Rel (ℝ D 𝐹) → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
302	226, 301	syl 17	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
303		inss2 4183	. . . . . . 7 ⊢ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
304	303	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
305	157, 304	fssresd 6685	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
306	302, 305	feq1dd 6629	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
307	306, 117	fssd 6663	. . 3 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℂ)
308		ioosscn 13303	. . . . 5 ⊢ (𝑋(,)+∞) ⊆ ℂ
309		ssinss1 4191	. . . . 5 ⊢ ((𝑋(,)+∞) ⊆ ℂ → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
310	308, 309	ax-mp 5	. . . 4 ⊢ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ
311	310	a1i 11	. . 3 ⊢ (𝜑 → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
312	263	simprd 495	. . . 4 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)))
313	265	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (TopOpen‘ℂ_fld) ∈ Top)
314	310	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
315		pnfxr 11161	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ^*
316	315	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → +∞ ∈ ℝ^*)
317		ltpnf 13014	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → 𝑦 < +∞)
318	270, 316, 317	xrltled 13044	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → 𝑦 ≤ +∞)
319		iooss2 13276	. . . . . . . . . . 11 ⊢ ((+∞ ∈ ℝ^* ∧ 𝑦 ≤ +∞) → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
320	316, 318, 319	syl2anc 584	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
321	320	3ad2ant2 1134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
322		simp3 1138	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))
323	321, 322	ssind 4186	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)))
324	278	lpss3 23054	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ ∧ (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
325	313, 314, 323, 324	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
326	325	3adant3l 1181	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
327	270	3ad2ant2 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑦 ∈ ℝ^*)
328	58	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ℝ)
329		simp3l 1202	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 < 𝑦)
330	125, 327, 328, 329	lptioo1cn 45684	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)))
331	326, 330	sseldd 3930	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
332	331	rexlimdv3a 3137	. . . 4 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)))))
333	312, 332	mpd 15	. . 3 ⊢ (𝜑 → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
334		biid 261	. . . 4 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ ℤ) ∧ 𝑤 = (𝑋 + (𝑘 · 𝑇))) ↔ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ ℤ) ∧ 𝑤 = (𝑋 + (𝑘 · 𝑇))))
335	61, 62, 161, 23, 71, 24, 25, 157, 256, 289, 134, 165, 58, 294, 298, 334	fourierdlem48 46192	. . 3 ⊢ (𝜑 → (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ≠ ∅)
336	307, 311, 333, 335, 125	ellimciota 45654	. 2 ⊢ (𝜑 → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim_ℂ 𝑋)) ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
337		fourierdlem113.l	. 2 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
338		fourierdlem113.r	. 2 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
339		fourierdlem113.a	. 2 ⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
340		fourierdlem113.b	. 2 ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
341		fveq2 6817	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
342		oveq1 7348	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 · 𝑋) = (𝑘 · 𝑋))
343	342	fveq2d 6821	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑋)) = (cos‘(𝑘 · 𝑋)))
344	341, 343	oveq12d 7359	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))))
345		fveq2 6817	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝐵‘𝑛) = (𝐵‘𝑘))
346	342	fveq2d 6821	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑋)) = (sin‘(𝑘 · 𝑋)))
347	345, 346	oveq12d 7359	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
348	344, 347	oveq12d 7359	. . . . . 6 ⊢ (𝑛 = 𝑘 → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
349	348	cbvsumv 15598	. . . . 5 ⊢ Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑘 ∈ (1...𝑚)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
350		oveq2 7349	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
351	350	eqcomd 2737	. . . . . 6 ⊢ (𝑗 = 𝑚 → (1...𝑚) = (1...𝑗))
352	351	sumeq1d 15602	. . . . 5 ⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑚)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
353	349, 352	eqtr2id 2779	. . . 4 ⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
354	353	oveq2d 7357	. . 3 ⊢ (𝑗 = 𝑚 → (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
355	354	cbvmptv 5190	. 2 ⊢ (𝑗 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))) = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
356		fourierdlem113.15	. 2 ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
357		fdm 6655	. . . . . 6 ⊢ (𝐹:ℝ⟶ℝ → dom 𝐹 = ℝ)
358	1, 357	syl 17	. . . . 5 ⊢ (𝜑 → dom 𝐹 = ℝ)
359	358, 154	eqsstrd 3964	. . . 4 ⊢ (𝜑 → dom 𝐹 ⊆ ℝ)
360	358	feq2d 6630	. . . . 5 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℝ ↔ 𝐹:ℝ⟶ℝ))
361	1, 360	mpbird 257	. . . 4 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ)
362	359	sselda 3929	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ dom 𝐹) → 𝑡 ∈ ℝ)
363	362	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑡 ∈ ℝ)
364	171	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
365	177	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
366	364, 365	remulcld 11137	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
367	363, 366	readdcld 11136	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ ℝ)
368	358	eqcomd 2737	. . . . . 6 ⊢ (𝜑 → ℝ = dom 𝐹)
369	368	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → ℝ = dom 𝐹)
370	367, 369	eleqtrd 2833	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ dom 𝐹)
371		id 22	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝜑 ∧ 𝑘 ∈ ℤ))
372	371	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝜑 ∧ 𝑘 ∈ ℤ))
373	372, 363, 184	syl2anc 584	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹‘𝑡))
374	359, 361, 61, 62, 161, 71, 24, 77, 162, 85, 140, 222, 224, 370, 373, 194, 195	fourierdlem71 46215	. . 3 ⊢ (𝜑 → ∃𝑢 ∈ ℝ ∀𝑡 ∈ dom 𝐹(abs‘(𝐹‘𝑡)) ≤ 𝑢)
375	358	raleqdv 3292	. . . 4 ⊢ (𝜑 → (∀𝑡 ∈ dom 𝐹(abs‘(𝐹‘𝑡)) ≤ 𝑢 ↔ ∀𝑡 ∈ ℝ (abs‘(𝐹‘𝑡)) ≤ 𝑢))
376	375	rexbidv 3156	. . 3 ⊢ (𝜑 → (∃𝑢 ∈ ℝ ∀𝑡 ∈ dom 𝐹(abs‘(𝐹‘𝑡)) ≤ 𝑢 ↔ ∃𝑢 ∈ ℝ ∀𝑡 ∈ ℝ (abs‘(𝐹‘𝑡)) ≤ 𝑢))
377	374, 376	mpbid 232	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ℝ ∀𝑡 ∈ ℝ (abs‘(𝐹‘𝑡)) ≤ 𝑢)
378	1, 22, 23, 24, 25, 32, 57, 58, 110, 69, 111, 140, 222, 224, 134, 300, 336, 337, 338, 339, 340, 355, 356, 377, 196, 58	fourierdlem112 46256	1 ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 {crab 3395 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 ∅c0 4278 ifcif 4470 {cpr 4573 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5611 ran crn 5612 ↾ cres 5613 Rel wrel 5616 ℩cio 6430 Fun wfun 6470 ⟶wf 6472 ‘cfv 6476 Isom wiso 6477 (class class class)co 7341 ↑_m cmap 8745 Fincfn 8864 ℂcc 10999 ℝcr 11000 0cc0 11001 1c1 11002 + caddc 11004 · cmul 11006 +∞cpnf 11138 -∞cmnf 11139 ℝ^*cxr 11140 < clt 11141 ≤ cle 11142 − cmin 11339 -cneg 11340 / cdiv 11769 ℕcn 12120 2c2 12175 ℕ₀cn0 12376 ℤcz 12463 ℤ_≥cuz 12727 (,)cioo 13240 (,]cioc 13241 [,)cico 13242 [,]cicc 13243 ...cfz 13402 ..^cfzo 13549 ⌊cfl 13689 mod cmo 13768 seqcseq 13903 ♯chash 14232 abscabs 15136 ⇝ cli 15386 Σcsu 15588 sincsin 15965 cosccos 15966 πcpi 15968 TopOpenctopn 17320 topGenctg 17336 ℂ_fldccnfld 21286 Topctop 22803 intcnt 22927 limPtclp 23044 –cn→ccncf 24791 ∫citg 25541 lim_ℂ climc 25785 D cdv 25786

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-inf2 9526 ax-cc 10321 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078 ax-pre-sup 11079 ax-addf 11080

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-symdif 4198 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-tp 4576 df-op 4578 df-uni 4855 df-int 4893 df-iun 4938 df-iin 4939 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-se 5565 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-isom 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7605 df-ofr 7606 df-om 7792 df-1st 7916 df-2nd 7917 df-supp 8086 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-2o 8381 df-oadd 8384 df-omul 8385 df-er 8617 df-map 8747 df-pm 8748 df-ixp 8817 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-fsupp 9241 df-fi 9290 df-sup 9321 df-inf 9322 df-oi 9391 df-dju 9789 df-card 9827 df-acn 9830 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-div 11770 df-nn 12121 df-2 12183 df-3 12184 df-4 12185 df-5 12186 df-6 12187 df-7 12188 df-8 12189 df-9 12190 df-n0 12377 df-xnn0 12450 df-z 12464 df-dec 12584 df-uz 12728 df-q 12842 df-rp 12886 df-xneg 13006 df-xadd 13007 df-xmul 13008 df-ioo 13244 df-ioc 13245 df-ico 13246 df-icc 13247 df-fz 13403 df-fzo 13550 df-fl 13691 df-mod 13769 df-seq 13904 df-exp 13964 df-fac 14176 df-bc 14205 df-hash 14233 df-shft 14969 df-cj 15001 df-re 15002 df-im 15003 df-sqrt 15137 df-abs 15138 df-limsup 15373 df-clim 15390 df-rlim 15391 df-sum 15589 df-ef 15969 df-sin 15971 df-cos 15972 df-pi 15974 df-struct 17053 df-sets 17070 df-slot 17088 df-ndx 17100 df-base 17116 df-ress 17137 df-plusg 17169 df-mulr 17170 df-starv 17171 df-sca 17172 df-vsca 17173 df-ip 17174 df-tset 17175 df-ple 17176 df-ds 17178 df-unif 17179 df-hom 17180 df-cco 17181 df-rest 17321 df-topn 17322 df-0g 17340 df-gsum 17341 df-topgen 17342 df-pt 17343 df-prds 17346 df-xrs 17401 df-qtop 17406 df-imas 17407 df-xps 17409 df-mre 17483 df-mrc 17484 df-acs 17486 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-submnd 18687 df-mulg 18976 df-cntz 19224 df-cmn 19689 df-psmet 21278 df-xmet 21279 df-met 21280 df-bl 21281 df-mopn 21282 df-fbas 21283 df-fg 21284 df-cnfld 21287 df-top 22804 df-topon 22821 df-topsp 22843 df-bases 22856 df-cld 22929 df-ntr 22930 df-cls 22931 df-nei 23008 df-lp 23046 df-perf 23047 df-cn 23137 df-cnp 23138 df-t1 23224 df-haus 23225 df-cmp 23297 df-tx 23472 df-hmeo 23665 df-fil 23756 df-fm 23848 df-flim 23849 df-flf 23850 df-xms 24230 df-ms 24231 df-tms 24232 df-cncf 24793 df-ovol 25387 df-vol 25388 df-mbf 25542 df-itg1 25543 df-itg2 25544 df-ibl 25545 df-itg 25546 df-0p 25593 df-ditg 25770 df-limc 25789 df-dv 25790

This theorem is referenced by: fourierdlem114 46258

W3C validator