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 46606

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 7377	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (𝑤 mod (2 · π)) = (𝑦 mod (2 · π)))
3	2	eqeq1d 2739	. . . . . 6 ⊢ (𝑤 = 𝑦 → ((𝑤 mod (2 · π)) = 0 ↔ (𝑦 mod (2 · π)) = 0))
4		oveq2 7378	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → ((𝑘 + (1 / 2)) · 𝑤) = ((𝑘 + (1 / 2)) · 𝑦))
5	4	fveq2d 6848	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (sin‘((𝑘 + (1 / 2)) · 𝑤)) = (sin‘((𝑘 + (1 / 2)) · 𝑦)))
6		oveq1 7377	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (𝑤 / 2) = (𝑦 / 2))
7	6	fveq2d 6848	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (sin‘(𝑤 / 2)) = (sin‘(𝑦 / 2)))
8	7	oveq2d 7386	. . . . . . 7 ⊢ (𝑤 = 𝑦 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑦 / 2))))
9	5, 8	oveq12d 7388	. . . . . 6 ⊢ (𝑤 = 𝑦 → ((sin‘((𝑘 + (1 / 2)) · 𝑤)) / ((2 · π) · (sin‘(𝑤 / 2)))) = ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
10	3, 9	ifbieq2d 4508	. . . . 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 5204	. . . 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 7378	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (2 · 𝑘) = (2 · 𝑚))
13	12	oveq1d 7385	. . . . . . 7 ⊢ (𝑘 = 𝑚 → ((2 · 𝑘) + 1) = ((2 · 𝑚) + 1))
14	13	oveq1d 7385	. . . . . 6 ⊢ (𝑘 = 𝑚 → (((2 · 𝑘) + 1) / (2 · π)) = (((2 · 𝑚) + 1) / (2 · π)))
15		oveq1 7377	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝑘 + (1 / 2)) = (𝑚 + (1 / 2)))
16	15	oveq1d 7385	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → ((𝑘 + (1 / 2)) · 𝑦) = ((𝑚 + (1 / 2)) · 𝑦))
17	16	fveq2d 6848	. . . . . . 7 ⊢ (𝑘 = 𝑚 → (sin‘((𝑘 + (1 / 2)) · 𝑦)) = (sin‘((𝑚 + (1 / 2)) · 𝑦)))
18	17	oveq1d 7385	. . . . . 6 ⊢ (𝑘 = 𝑚 → ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
19	14, 18	ifeq12d 4503	. . . . 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 5194	. . . 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 2784	. . 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 5204	. 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 7377	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (𝑤 + (𝑗 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
27	26	eleq1d 2822	. . . . . . 7 ⊢ (𝑤 = 𝑦 → ((𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
28	27	rexbidv 3162	. . . . . 6 ⊢ (𝑤 = 𝑦 → (∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
29	28	cbvrabv 3411	. . . . 5 ⊢ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
30	29	uneq2i 4119	. . . 4 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
31	30	fveq2i 6847	. . 3 ⊢ (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) = (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
32	31	oveq1i 7380	. 2 ⊢ ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
33		oveq1 7377	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
34	33	oveq2d 7386	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑗 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
35	34	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
36	35	cbvrexvw 3217	. . . . . . . . 9 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄)
37	36	a1i 11	. . . . . . . 8 ⊢ (𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
38	37	rabbiia 3405	. . . . . . 7 ⊢ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
39	38	uneq2i 4119	. . . . . 6 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
40		isoeq5 7279	. . . . . 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 7386	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → (𝑤 + (𝑘 · 𝑇)) = (𝑤 + (𝑗 · 𝑇)))
44	43	eleq1d 2822	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → ((𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
45	44	cbvrexvw 3217	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄)
46	45	a1i 11	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) → (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
47	46	rabbiia 3405	. . . . . . . . . 10 ⊢ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}
48	47	uneq2i 4119	. . . . . . . . 9 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})
49	48	fveq2i 6847	. . . . . . . 8 ⊢ (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
50	49	oveq1i 7380	. . . . . . 7 ⊢ ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
51	50	oveq2i 7381	. . . . . 6 ⊢ (0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)) = (0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1))
52		isoeq4 7278	. . . . . 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 7275	. . . 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 6466	. 2 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
58		fourierdlem113.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℝ)
59		pire 26439	. . . . 5 ⊢ π ∈ ℝ
60	59	renegcli 11456	. . . 4 ⊢ -π ∈ ℝ
61	60	a1i 11	. . 3 ⊢ (𝜑 → -π ∈ ℝ)
62	59	a1i 11	. . 3 ⊢ (𝜑 → π ∈ ℝ)
63		negpilt0 45672	. . . 4 ⊢ -π < 0
64	63	a1i 11	. . 3 ⊢ (𝜑 → -π < 0)
65		pipos 26441	. . . 4 ⊢ 0 < π
66	65	a1i 11	. . 3 ⊢ (𝜑 → 0 < π)
67		picn 26440	. . . . 5 ⊢ π ∈ ℂ
68	67	2timesi 12292	. . . 4 ⊢ (2 · π) = (π + π)
69		fourierdlem113.t	. . . 4 ⊢ 𝑇 = (2 · π)
70	67, 67	subnegi 11474	. . . 4 ⊢ (π − -π) = (π + π)
71	68, 69, 70	3eqtr4i 2770	. . 3 ⊢ 𝑇 = (π − -π)
72	23	fourierdlem2 46496	. . . . . . . 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 8800	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
77	75, 76	syl 17	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
78		fzfid 13910	. . . 4 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
79		rnffi 45563	. . . 4 ⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin)
80	77, 78, 79	syl2anc 585	. . 3 ⊢ (𝜑 → ran 𝑄 ∈ Fin)
81	23, 24, 25	fourierdlem15 46509	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
82		frn 6679	. . . 4 ⊢ (𝑄:(0...𝑀)⟶(-π[,]π) → ran 𝑄 ⊆ (-π[,]π))
83	81, 82	syl 17	. . 3 ⊢ (𝜑 → ran 𝑄 ⊆ (-π[,]π))
84	74	simprd 495	. . . . 5 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
85	84	simplrd 770	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = π)
86		ffun 6675	. . . . . 6 ⊢ (𝑄:(0...𝑀)⟶(-π[,]π) → Fun 𝑄)
87	81, 86	syl 17	. . . . 5 ⊢ (𝜑 → Fun 𝑄)
88	24	nnnn0d 12476	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
89		nn0uz 12803	. . . . . . . 8 ⊢ ℕ₀ = (ℤ_≥‘0)
90	88, 89	eleqtrdi 2847	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
91		eluzfz2 13462	. . . . . . 7 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
92	90, 91	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
93		fdm 6681	. . . . . . . 8 ⊢ (𝑄:(0...𝑀)⟶(-π[,]π) → dom 𝑄 = (0...𝑀))
94	81, 93	syl 17	. . . . . . 7 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
95	94	eqcomd 2743	. . . . . 6 ⊢ (𝜑 → (0...𝑀) = dom 𝑄)
96	92, 95	eleqtrd 2839	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ dom 𝑄)
97		fvelrn 7032	. . . . 5 ⊢ ((Fun 𝑄 ∧ 𝑀 ∈ dom 𝑄) → (𝑄‘𝑀) ∈ ran 𝑄)
98	87, 96, 97	syl2anc 585	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
99	85, 98	eqeltrrd 2838	. . 3 ⊢ (𝜑 → π ∈ ran 𝑄)
100		fourierdlem113.e	. . 3 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
101		fourierdlem113.exq	. . 3 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄)
102		eqid 2737	. . 3 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
103		isoeq1 7275	. . . . 5 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
104	30, 48, 39	3eqtr4ri 2771	. . . . . 6 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
105		isoeq5 7279	. . . . . 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 6466	. . 3 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
109		eqid 2737	. . 3 ⊢ {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
110	61, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109	fourierdlem51 46544	. 2 ⊢ (𝜑 → 𝑋 ∈ ran (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
111		fourierdlem113.per	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
112		ax-resscn 11097	. . . 4 ⊢ ℝ ⊆ ℂ
113	112	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℂ)
114		ioossre 13337	. . . . . . 7 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
115	114	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
116	1, 115	fssresd 6711	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
117	112	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
118	116, 117	fssd 6689	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
119	118	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
120	114	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
121	1, 117	fssd 6689	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
122	121	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
123		ssid 3958	. . . . . . 7 ⊢ ℝ ⊆ ℝ
124	123	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℝ)
125		eqid 2737	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
126		tgioo4 24766	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
127	125, 126	dvres 25885	. . . . . 6 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
128	113, 122, 124, 120, 127	syl22anc 839	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
129	128	dmeqd 5864	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
130		ioontr 45900	. . . . . . 7 ⊢ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))
131	130	reseq2i 5945	. . . . . 6 ⊢ ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
132	131	dmeqi 5863	. . . . 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 24859	. . . . 5 ⊢ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
136		fdm 6681	. . . . 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 2776	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
139		dvcn 25896	. . 3 ⊢ (((ℝ ⊆ ℂ ∧ (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ) ∧ dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
140	113, 119, 120, 138, 139	syl31anc 1376	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
141	120, 113	sstrd 3946	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
142	77	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
143		fzofzp1 13694	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
144	143	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
145	142, 144	ffvelcdmd 7041	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
146	145	rexrd 11196	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
147		elfzofz 13605	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
148	147	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
149	142, 148	ffvelcdmd 7041	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
150	74	simprrd 774	. . . . 5 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
151	150	r19.21bi 3230	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
152	125, 146, 149, 151	lptioo1cn 46033	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
153	116	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
154	123	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ ⊆ ℝ)
155	117, 121, 154	dvbss 25875	. . . . . . 7 ⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ ℝ)
156		dvfre 25928	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
157	1, 154, 156	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
158		0re 11148	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
159	60, 158, 59	lttri 11273	. . . . . . . . 9 ⊢ ((-π < 0 ∧ 0 < π) → -π < π)
160	63, 65, 159	mp2an 693	. . . . . . . 8 ⊢ -π < π
161	160	a1i 11	. . . . . . 7 ⊢ (𝜑 → -π < π)
162	84	simplld 768	. . . . . . 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 46003	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
166	149	rexrd 11196	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
167	125, 166, 145, 151	lptioo2cn 46032	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
168		fourierdlem113.dvub	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
169	163, 141, 167, 168, 125	ellimciota 46003	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
170	121	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
171		zre 12506	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
172	171	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
173		2re 12233	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
174	173, 59	remulcli 11162	. . . . . . . . . . . . . 14 ⊢ (2 · π) ∈ ℝ
175	174	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · π) ∈ ℝ)
176	69, 175	eqeltrid 2841	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℝ)
177	176	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
178	172, 177	remulcld 11176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
179	170	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
180	177	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℝ)
181		simplr 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑘 ∈ ℤ)
182		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
183	111	ad4ant14 753	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
184	179, 180, 181, 182, 183	fperiodmul 45695	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹‘𝑡))
185		eqid 2737	. . . . . . . . . 10 ⊢ (ℝ D 𝐹) = (ℝ D 𝐹)
186	170, 178, 184, 185	fperdvper 46306	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ dom (ℝ D 𝐹)) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡)))
187	186	an32s 653	. . . . . . . 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 6844	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑄‘𝑗) = (𝑄‘𝑖))
191		oveq1 7377	. . . . . . . . . 10 ⊢ (𝑗 = 𝑖 → (𝑗 + 1) = (𝑖 + 1))
192	191	fveq2d 6848	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑄‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)))
193	190, 192	oveq12d 7388	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
194	193	cbvmptv 5204	. . . . . . 7 ⊢ (𝑗 ∈ (0..^𝑀) ↦ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1)))) = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
195		eqid 2737	. . . . . . 7 ⊢ (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇))) = (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇)))
196	155, 157, 61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195	fourierdlem71 46564	. . . . . 6 ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
197	196	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
198		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0..^𝑀))
199		nfra1 3262	. . . . . . . . 9 ⊢ Ⅎ𝑡∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧
200	198, 199	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
201	128, 131	eqtrdi 2788	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
202	201	fveq1d 6846	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡))
203		fvres 6863	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
204	202, 203	sylan9eq 2792	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
205	204	fveq2d 6848	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡)))
206	205	adantlr 716	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡)))
207		simplr 769	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
208		ssdmres 5982	. . . . . . . . . . . . . 14 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
209	137, 208	sylibr 234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹))
210	209	ad2antrr 727	. . . . . . . . . . . 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 3936	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ dom (ℝ D 𝐹))
213		rspa 3227	. . . . . . . . . . 11 ⊢ ((∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
214	207, 212, 213	syl2anc 585	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
215	206, 214	eqbrtrd 5122	. . . . . . . . 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 3236	. . . . . . 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 3153	. . . . 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 46320	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
222	119, 141, 152, 221, 125	ellimciota 46003	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
223	149, 145, 153, 138, 220	ioodvbdlimc2 46322	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
224	119, 141, 167, 223, 125	ellimciota 46003	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
225		frel 6677	. . . . . . 7 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ → Rel (ℝ D 𝐹))
226	157, 225	syl 17	. . . . . 6 ⊢ (𝜑 → Rel (ℝ D 𝐹))
227		resindm 5999	. . . . . 6 ⊢ (Rel (ℝ D 𝐹) → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
228	226, 227	syl 17	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
229		inss2 4192	. . . . . . 7 ⊢ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
230	229	a1i 11	. . . . . 6 ⊢ (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
231	157, 230	fssresd 6711	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
232	228, 231	feq1dd 6655	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
233	232, 117	fssd 6689	. . 3 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℂ)
234		ioosscn 13338	. . . . 5 ⊢ (-∞(,)𝑋) ⊆ ℂ
235		ssinss1 4200	. . . . 5 ⊢ ((-∞(,)𝑋) ⊆ ℂ → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
236	234, 235	ax-mp 5	. . . 4 ⊢ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ
237	236	a1i 11	. . 3 ⊢ (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
238		3simpb 1150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → (𝜑 ∧ 𝑘 ∈ ℤ))
239		simp2 1138	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ dom (ℝ D 𝐹))
240	170	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
241	177	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
242		simplr 769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℤ)
243		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
244		eleq1w 2820	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℝ ↔ 𝑦 ∈ ℝ))
245	244	anbi2d 631	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ 𝑦 ∈ ℝ)))
246		oveq1 7377	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
247	246	fveq2d 6848	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
248		fveq2 6844	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
249	247, 248	eqeq12d 2753	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)))
250	245, 249	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))))
251	250, 111	chvarvv 1991	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))
252	251	ad4ant14 753	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))
253	240, 241, 242, 243, 252	fperiodmul 45695	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))
254	170, 178, 253, 185	fperdvper 46306	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥)))
255	238, 239, 254	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥)))
256	255	simpld 494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹))
257		oveq2 7378	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (π − 𝑤) = (π − 𝑥))
258	257	oveq1d 7385	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((π − 𝑤) / 𝑇) = ((π − 𝑥) / 𝑇))
259	258	fveq2d 6848	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (⌊‘((π − 𝑤) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
260	259	oveq1d 7385	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
261	260	cbvmptv 5204	. . . . . 6 ⊢ (𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
262		eqid 2737	. . . . . 6 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥)))
263	61, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209	fourierdlem41 46535	. . . . 5 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))))
264	263	simpld 494	. . . 4 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)))
265	125	cnfldtop 24744	. . . . . . . . 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 11203	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
269	268	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → -∞ ∈ ℝ^*)
270		rexr 11192	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℝ^*)
271		mnflt 13051	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → -∞ < 𝑦)
272	269, 270, 271	xrltled 13078	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → -∞ ≤ 𝑦)
273		iooss1 13310	. . . . . . . . . . 11 ⊢ ((-∞ ∈ ℝ^* ∧ -∞ ≤ 𝑦) → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
274	269, 272, 273	syl2anc 585	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
275	274	3ad2ant2 1135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
276		simp3 1139	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))
277	275, 276	ssind 4195	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)))
278		unicntop 24746	. . . . . . . . 9 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
279	278	lpss3 23105	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ ∧ (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
280	266, 267, 277, 279	syl3anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
281	280	3adant3l 1182	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
282	270	3ad2ant2 1135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑦 ∈ ℝ^*)
283	58	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ℝ)
284		simp3l 1203	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑦 < 𝑋)
285	125, 282, 283, 284	lptioo2cn 46032	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)))
286	281, 285	sseldd 3936	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
287	286	rexlimdv3a 3143	. . . 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 7378	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (π − 𝑦) = (π − 𝑥))
291	290	oveq1d 7385	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((π − 𝑦) / 𝑇) = ((π − 𝑥) / 𝑇))
292	291	fveq2d 6848	. . . . . 6 ⊢ (𝑦 = 𝑥 → (⌊‘((π − 𝑦) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
293	292	oveq1d 7385	. . . . 5 ⊢ (𝑦 = 𝑥 → ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
294	293	cbvmptv 5204	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
295		id 22	. . . . . 6 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
296		fveq2 6844	. . . . . 6 ⊢ (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧) = ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥))
297	295, 296	oveq12d 7388	. . . . 5 ⊢ (𝑧 = 𝑥 → (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧)) = (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
298	297	cbvmptv 5204	. . . 4 ⊢ (𝑧 ∈ ℝ ↦ (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
299	61, 62, 161, 23, 71, 24, 25, 155, 157, 256, 289, 134, 169, 58, 294, 298	fourierdlem49 46542	. . 3 ⊢ (𝜑 → (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ≠ ∅)
300	233, 237, 288, 299, 125	ellimciota 46003	. 2 ⊢ (𝜑 → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋)) ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
301		resindm 5999	. . . . . 6 ⊢ (Rel (ℝ D 𝐹) → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
302	226, 301	syl 17	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
303		inss2 4192	. . . . . . 7 ⊢ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
304	303	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
305	157, 304	fssresd 6711	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
306	302, 305	feq1dd 6655	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
307	306, 117	fssd 6689	. . 3 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℂ)
308		ioosscn 13338	. . . . 5 ⊢ (𝑋(,)+∞) ⊆ ℂ
309		ssinss1 4200	. . . . 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 11200	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ^*
316	315	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → +∞ ∈ ℝ^*)
317		ltpnf 13048	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → 𝑦 < +∞)
318	270, 316, 317	xrltled 13078	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → 𝑦 ≤ +∞)
319		iooss2 13311	. . . . . . . . . . 11 ⊢ ((+∞ ∈ ℝ^* ∧ 𝑦 ≤ +∞) → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
320	316, 318, 319	syl2anc 585	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
321	320	3ad2ant2 1135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
322		simp3 1139	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))
323	321, 322	ssind 4195	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)))
324	278	lpss3 23105	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ ∧ (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
325	313, 314, 323, 324	syl3anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
326	325	3adant3l 1182	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
327	270	3ad2ant2 1135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑦 ∈ ℝ^*)
328	58	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ℝ)
329		simp3l 1203	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 < 𝑦)
330	125, 327, 328, 329	lptioo1cn 46033	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)))
331	326, 330	sseldd 3936	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
332	331	rexlimdv3a 3143	. . . 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 46541	. . 3 ⊢ (𝜑 → (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ≠ ∅)
336	307, 311, 333, 335, 125	ellimciota 46003	. 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 6844	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
342		oveq1 7377	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 · 𝑋) = (𝑘 · 𝑋))
343	342	fveq2d 6848	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑋)) = (cos‘(𝑘 · 𝑋)))
344	341, 343	oveq12d 7388	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))))
345		fveq2 6844	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝐵‘𝑛) = (𝐵‘𝑘))
346	342	fveq2d 6848	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑋)) = (sin‘(𝑘 · 𝑋)))
347	345, 346	oveq12d 7388	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
348	344, 347	oveq12d 7388	. . . . . 6 ⊢ (𝑛 = 𝑘 → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
349	348	cbvsumv 15633	. . . . 5 ⊢ Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑘 ∈ (1...𝑚)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
350		oveq2 7378	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
351	350	eqcomd 2743	. . . . . 6 ⊢ (𝑗 = 𝑚 → (1...𝑚) = (1...𝑗))
352	351	sumeq1d 15637	. . . . 5 ⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑚)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
353	349, 352	eqtr2id 2785	. . . 4 ⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
354	353	oveq2d 7386	. . 3 ⊢ (𝑗 = 𝑚 → (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
355	354	cbvmptv 5204	. 2 ⊢ (𝑗 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))) = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
356		fourierdlem113.15	. 2 ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
357		fdm 6681	. . . . . 6 ⊢ (𝐹:ℝ⟶ℝ → dom 𝐹 = ℝ)
358	1, 357	syl 17	. . . . 5 ⊢ (𝜑 → dom 𝐹 = ℝ)
359	358, 154	eqsstrd 3970	. . . 4 ⊢ (𝜑 → dom 𝐹 ⊆ ℝ)
360	358	feq2d 6656	. . . . 5 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℝ ↔ 𝐹:ℝ⟶ℝ))
361	1, 360	mpbird 257	. . . 4 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ)
362	359	sselda 3935	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ dom 𝐹) → 𝑡 ∈ ℝ)
363	362	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑡 ∈ ℝ)
364	171	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
365	177	adantlr 716	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
366	364, 365	remulcld 11176	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
367	363, 366	readdcld 11175	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ ℝ)
368	358	eqcomd 2743	. . . . . 6 ⊢ (𝜑 → ℝ = dom 𝐹)
369	368	ad2antrr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → ℝ = dom 𝐹)
370	367, 369	eleqtrd 2839	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ dom 𝐹)
371		id 22	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝜑 ∧ 𝑘 ∈ ℤ))
372	371	adantlr 716	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝜑 ∧ 𝑘 ∈ ℤ))
373	372, 363, 184	syl2anc 585	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹‘𝑡))
374	359, 361, 61, 62, 161, 71, 24, 77, 162, 85, 140, 222, 224, 370, 373, 194, 195	fourierdlem71 46564	. . 3 ⊢ (𝜑 → ∃𝑢 ∈ ℝ ∀𝑡 ∈ dom 𝐹(abs‘(𝐹‘𝑡)) ≤ 𝑢)
375	358	raleqdv 3298	. . . 4 ⊢ (𝜑 → (∀𝑡 ∈ dom 𝐹(abs‘(𝐹‘𝑡)) ≤ 𝑢 ↔ ∀𝑡 ∈ ℝ (abs‘(𝐹‘𝑡)) ≤ 𝑢))
376	375	rexbidv 3162	. . 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 46605	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 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3401 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 ∅c0 4287 ifcif 4481 {cpr 4584 class class class wbr 5100 ↦ cmpt 5181 dom cdm 5634 ran crn 5635 ↾ cres 5636 Rel wrel 5639 ℩cio 6456 Fun wfun 6496 ⟶wf 6498 ‘cfv 6502 Isom wiso 6503 (class class class)co 7370 ↑_m cmap 8777 Fincfn 8897 ℂcc 11038 ℝcr 11039 0cc0 11040 1c1 11041 + caddc 11043 · cmul 11045 +∞cpnf 11177 -∞cmnf 11178 ℝ^*cxr 11179 < clt 11180 ≤ cle 11181 − cmin 11378 -cneg 11379 / cdiv 11808 ℕcn 12159 2c2 12214 ℕ₀cn0 12415 ℤcz 12502 ℤ_≥cuz 12765 (,)cioo 13275 (,]cioc 13276 [,)cico 13277 [,]cicc 13278 ...cfz 13437 ..^cfzo 13584 ⌊cfl 13724 mod cmo 13803 seqcseq 13938 ♯chash 14267 abscabs 15171 ⇝ cli 15421 Σcsu 15623 sincsin 16000 cosccos 16001 πcpi 16003 TopOpenctopn 17355 topGenctg 17371 ℂ_fldccnfld 21326 Topctop 22854 intcnt 22978 limPtclp 23095 –cn→ccncf 24842 ∫citg 25592 lim_ℂ climc 25836 D cdv 25837

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 2709 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-inf2 9564 ax-cc 10359 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117 ax-pre-sup 11118 ax-addf 11119

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 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-symdif 4207 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-disj 5068 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-se 5588 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-isom 6511 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-of 7634 df-ofr 7635 df-om 7821 df-1st 7945 df-2nd 7946 df-supp 8115 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-1o 8409 df-2o 8410 df-oadd 8413 df-omul 8414 df-er 8647 df-map 8779 df-pm 8780 df-ixp 8850 df-en 8898 df-dom 8899 df-sdom 8900 df-fin 8901 df-fsupp 9279 df-fi 9328 df-sup 9359 df-inf 9360 df-oi 9429 df-dju 9827 df-card 9865 df-acn 9868 df-pnf 11182 df-mnf 11183 df-xr 11184 df-ltxr 11185 df-le 11186 df-sub 11380 df-neg 11381 df-div 11809 df-nn 12160 df-2 12222 df-3 12223 df-4 12224 df-5 12225 df-6 12226 df-7 12227 df-8 12228 df-9 12229 df-n0 12416 df-xnn0 12489 df-z 12503 df-dec 12622 df-uz 12766 df-q 12876 df-rp 12920 df-xneg 13040 df-xadd 13041 df-xmul 13042 df-ioo 13279 df-ioc 13280 df-ico 13281 df-icc 13282 df-fz 13438 df-fzo 13585 df-fl 13726 df-mod 13804 df-seq 13939 df-exp 13999 df-fac 14211 df-bc 14240 df-hash 14268 df-shft 15004 df-cj 15036 df-re 15037 df-im 15038 df-sqrt 15172 df-abs 15173 df-limsup 15408 df-clim 15425 df-rlim 15426 df-sum 15624 df-ef 16004 df-sin 16006 df-cos 16007 df-pi 16009 df-struct 17088 df-sets 17105 df-slot 17123 df-ndx 17135 df-base 17151 df-ress 17172 df-plusg 17204 df-mulr 17205 df-starv 17206 df-sca 17207 df-vsca 17208 df-ip 17209 df-tset 17210 df-ple 17211 df-ds 17213 df-unif 17214 df-hom 17215 df-cco 17216 df-rest 17356 df-topn 17357 df-0g 17375 df-gsum 17376 df-topgen 17377 df-pt 17378 df-prds 17381 df-xrs 17437 df-qtop 17442 df-imas 17443 df-xps 17445 df-mre 17519 df-mrc 17520 df-acs 17522 df-mgm 18579 df-sgrp 18658 df-mnd 18674 df-submnd 18723 df-mulg 19015 df-cntz 19263 df-cmn 19728 df-psmet 21318 df-xmet 21319 df-met 21320 df-bl 21321 df-mopn 21322 df-fbas 21323 df-fg 21324 df-cnfld 21327 df-top 22855 df-topon 22872 df-topsp 22894 df-bases 22907 df-cld 22980 df-ntr 22981 df-cls 22982 df-nei 23059 df-lp 23097 df-perf 23098 df-cn 23188 df-cnp 23189 df-t1 23275 df-haus 23276 df-cmp 23348 df-tx 23523 df-hmeo 23716 df-fil 23807 df-fm 23899 df-flim 23900 df-flf 23901 df-xms 24281 df-ms 24282 df-tms 24283 df-cncf 24844 df-ovol 25438 df-vol 25439 df-mbf 25593 df-itg1 25594 df-itg2 25595 df-ibl 25596 df-itg 25597 df-0p 25644 df-ditg 25821 df-limc 25840 df-dv 25841

This theorem is referenced by: fourierdlem114 46607

W3C validator