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 46248

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 7412	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (𝑤 mod (2 · π)) = (𝑦 mod (2 · π)))
3	2	eqeq1d 2737	. . . . . 6 ⊢ (𝑤 = 𝑦 → ((𝑤 mod (2 · π)) = 0 ↔ (𝑦 mod (2 · π)) = 0))
4		oveq2 7413	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → ((𝑘 + (1 / 2)) · 𝑤) = ((𝑘 + (1 / 2)) · 𝑦))
5	4	fveq2d 6880	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (sin‘((𝑘 + (1 / 2)) · 𝑤)) = (sin‘((𝑘 + (1 / 2)) · 𝑦)))
6		oveq1 7412	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (𝑤 / 2) = (𝑦 / 2))
7	6	fveq2d 6880	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (sin‘(𝑤 / 2)) = (sin‘(𝑦 / 2)))
8	7	oveq2d 7421	. . . . . . 7 ⊢ (𝑤 = 𝑦 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑦 / 2))))
9	5, 8	oveq12d 7423	. . . . . 6 ⊢ (𝑤 = 𝑦 → ((sin‘((𝑘 + (1 / 2)) · 𝑤)) / ((2 · π) · (sin‘(𝑤 / 2)))) = ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
10	3, 9	ifbieq2d 4527	. . . . 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 5225	. . . 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 7413	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (2 · 𝑘) = (2 · 𝑚))
13	12	oveq1d 7420	. . . . . . 7 ⊢ (𝑘 = 𝑚 → ((2 · 𝑘) + 1) = ((2 · 𝑚) + 1))
14	13	oveq1d 7420	. . . . . 6 ⊢ (𝑘 = 𝑚 → (((2 · 𝑘) + 1) / (2 · π)) = (((2 · 𝑚) + 1) / (2 · π)))
15		oveq1 7412	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → (𝑘 + (1 / 2)) = (𝑚 + (1 / 2)))
16	15	oveq1d 7420	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → ((𝑘 + (1 / 2)) · 𝑦) = ((𝑚 + (1 / 2)) · 𝑦))
17	16	fveq2d 6880	. . . . . . 7 ⊢ (𝑘 = 𝑚 → (sin‘((𝑘 + (1 / 2)) · 𝑦)) = (sin‘((𝑚 + (1 / 2)) · 𝑦)))
18	17	oveq1d 7420	. . . . . 6 ⊢ (𝑘 = 𝑚 → ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
19	14, 18	ifeq12d 4522	. . . . 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 5215	. . . 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 2782	. . 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 5225	. 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 7412	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (𝑤 + (𝑗 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
27	26	eleq1d 2819	. . . . . . 7 ⊢ (𝑤 = 𝑦 → ((𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
28	27	rexbidv 3164	. . . . . 6 ⊢ (𝑤 = 𝑦 → (∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
29	28	cbvrabv 3426	. . . . 5 ⊢ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
30	29	uneq2i 4140	. . . 4 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
31	30	fveq2i 6879	. . 3 ⊢ (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) = (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
32	31	oveq1i 7415	. 2 ⊢ ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
33		oveq1 7412	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
34	33	oveq2d 7421	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑗 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
35	34	eleq1d 2819	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
36	35	cbvrexvw 3221	. . . . . . . . 9 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄)
37	36	a1i 11	. . . . . . . 8 ⊢ (𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
38	37	rabbiia 3419	. . . . . . 7 ⊢ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
39	38	uneq2i 4140	. . . . . 6 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
40		isoeq5 7314	. . . . . 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 7421	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → (𝑤 + (𝑘 · 𝑇)) = (𝑤 + (𝑗 · 𝑇)))
44	43	eleq1d 2819	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → ((𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
45	44	cbvrexvw 3221	. . . . . . . . . . . 12 ⊢ (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄)
46	45	a1i 11	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) → (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
47	46	rabbiia 3419	. . . . . . . . . 10 ⊢ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}
48	47	uneq2i 4140	. . . . . . . . 9 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})
49	48	fveq2i 6879	. . . . . . . 8 ⊢ (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
50	49	oveq1i 7415	. . . . . . 7 ⊢ ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
51	50	oveq2i 7416	. . . . . 6 ⊢ (0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)) = (0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1))
52		isoeq4 7313	. . . . . 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 7310	. . . 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 6492	. 2 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
58		fourierdlem113.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℝ)
59		pire 26418	. . . . 5 ⊢ π ∈ ℝ
60	59	renegcli 11544	. . . 4 ⊢ -π ∈ ℝ
61	60	a1i 11	. . 3 ⊢ (𝜑 → -π ∈ ℝ)
62	59	a1i 11	. . 3 ⊢ (𝜑 → π ∈ ℝ)
63		negpilt0 45309	. . . 4 ⊢ -π < 0
64	63	a1i 11	. . 3 ⊢ (𝜑 → -π < 0)
65		pipos 26420	. . . 4 ⊢ 0 < π
66	65	a1i 11	. . 3 ⊢ (𝜑 → 0 < π)
67		picn 26419	. . . . 5 ⊢ π ∈ ℂ
68	67	2timesi 12378	. . . 4 ⊢ (2 · π) = (π + π)
69		fourierdlem113.t	. . . 4 ⊢ 𝑇 = (2 · π)
70	67, 67	subnegi 11562	. . . 4 ⊢ (π − -π) = (π + π)
71	68, 69, 70	3eqtr4i 2768	. . 3 ⊢ 𝑇 = (π − -π)
72	23	fourierdlem2 46138	. . . . . . . 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 8863	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
77	75, 76	syl 17	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
78		fzfid 13991	. . . 4 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
79		rnffi 45199	. . . 4 ⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin)
80	77, 78, 79	syl2anc 584	. . 3 ⊢ (𝜑 → ran 𝑄 ∈ Fin)
81	23, 24, 25	fourierdlem15 46151	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
82		frn 6713	. . . 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 6709	. . . . . 6 ⊢ (𝑄:(0...𝑀)⟶(-π[,]π) → Fun 𝑄)
87	81, 86	syl 17	. . . . 5 ⊢ (𝜑 → Fun 𝑄)
88	24	nnnn0d 12562	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
89		nn0uz 12894	. . . . . . . 8 ⊢ ℕ₀ = (ℤ_≥‘0)
90	88, 89	eleqtrdi 2844	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
91		eluzfz2 13549	. . . . . . 7 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
92	90, 91	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
93		fdm 6715	. . . . . . . 8 ⊢ (𝑄:(0...𝑀)⟶(-π[,]π) → dom 𝑄 = (0...𝑀))
94	81, 93	syl 17	. . . . . . 7 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
95	94	eqcomd 2741	. . . . . 6 ⊢ (𝜑 → (0...𝑀) = dom 𝑄)
96	92, 95	eleqtrd 2836	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ dom 𝑄)
97		fvelrn 7066	. . . . 5 ⊢ ((Fun 𝑄 ∧ 𝑀 ∈ dom 𝑄) → (𝑄‘𝑀) ∈ ran 𝑄)
98	87, 96, 97	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
99	85, 98	eqeltrrd 2835	. . 3 ⊢ (𝜑 → π ∈ ran 𝑄)
100		fourierdlem113.e	. . 3 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
101		fourierdlem113.exq	. . 3 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄)
102		eqid 2735	. . 3 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
103		isoeq1 7310	. . . . 5 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
104	30, 48, 39	3eqtr4ri 2769	. . . . . 6 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
105		isoeq5 7314	. . . . . 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 6492	. . 3 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
109		eqid 2735	. . 3 ⊢ {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
110	61, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109	fourierdlem51 46186	. 2 ⊢ (𝜑 → 𝑋 ∈ ran (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
111		fourierdlem113.per	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
112		ax-resscn 11186	. . . 4 ⊢ ℝ ⊆ ℂ
113	112	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℂ)
114		ioossre 13424	. . . . . . 7 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
115	114	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
116	1, 115	fssresd 6745	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
117	112	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
118	116, 117	fssd 6723	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
119	118	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
120	114	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
121	1, 117	fssd 6723	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
122	121	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
123		ssid 3981	. . . . . . 7 ⊢ ℝ ⊆ ℝ
124	123	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℝ)
125		eqid 2735	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
126		tgioo4 24744	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
127	125, 126	dvres 25864	. . . . . 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 5885	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
130		ioontr 45540	. . . . . . 7 ⊢ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))
131	130	reseq2i 5963	. . . . . 6 ⊢ ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
132	131	dmeqi 5884	. . . . 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 24837	. . . . 5 ⊢ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
136		fdm 6715	. . . . 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 2774	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
139		dvcn 25875	. . 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 3969	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
142	77	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
143		fzofzp1 13780	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
144	143	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
145	142, 144	ffvelcdmd 7075	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
146	145	rexrd 11285	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
147		elfzofz 13692	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
148	147	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
149	142, 148	ffvelcdmd 7075	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
150	74	simprrd 773	. . . . 5 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
151	150	r19.21bi 3234	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
152	125, 146, 149, 151	lptioo1cn 45675	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
153	116	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
154	123	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ ⊆ ℝ)
155	117, 121, 154	dvbss 25854	. . . . . . 7 ⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ ℝ)
156		dvfre 25907	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
157	1, 154, 156	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
158		0re 11237	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
159	60, 158, 59	lttri 11361	. . . . . . . . 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 45643	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
166	149	rexrd 11285	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
167	125, 166, 145, 151	lptioo2cn 45674	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
168		fourierdlem113.dvub	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
169	163, 141, 167, 168, 125	ellimciota 45643	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
170	121	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
171		zre 12592	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
172	171	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
173		2re 12314	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
174	173, 59	remulcli 11251	. . . . . . . . . . . . . 14 ⊢ (2 · π) ∈ ℝ
175	174	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · π) ∈ ℝ)
176	69, 175	eqeltrid 2838	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℝ)
177	176	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
178	172, 177	remulcld 11265	. . . . . . . . . 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 45333	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹‘𝑡))
185		eqid 2735	. . . . . . . . . 10 ⊢ (ℝ D 𝐹) = (ℝ D 𝐹)
186	170, 178, 184, 185	fperdvper 45948	. . . . . . . . 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 6876	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑄‘𝑗) = (𝑄‘𝑖))
191		oveq1 7412	. . . . . . . . . 10 ⊢ (𝑗 = 𝑖 → (𝑗 + 1) = (𝑖 + 1))
192	191	fveq2d 6880	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑄‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)))
193	190, 192	oveq12d 7423	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
194	193	cbvmptv 5225	. . . . . . 7 ⊢ (𝑗 ∈ (0..^𝑀) ↦ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1)))) = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
195		eqid 2735	. . . . . . 7 ⊢ (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇))) = (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇)))
196	155, 157, 61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195	fourierdlem71 46206	. . . . . 6 ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
197	196	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
198		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0..^𝑀))
199		nfra1 3266	. . . . . . . . 9 ⊢ Ⅎ𝑡∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧
200	198, 199	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
201	128, 131	eqtrdi 2786	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
202	201	fveq1d 6878	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡))
203		fvres 6895	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
204	202, 203	sylan9eq 2790	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
205	204	fveq2d 6880	. . . . . . . . . . 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 6000	. . . . . . . . . . . . . 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 3959	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ dom (ℝ D 𝐹))
213		rspa 3231	. . . . . . . . . . 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 5141	. . . . . . . . 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 3240	. . . . . . 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 3155	. . . . 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 45962	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
222	119, 141, 152, 221, 125	ellimciota 45643	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
223	149, 145, 153, 138, 220	ioodvbdlimc2 45964	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
224	119, 141, 167, 223, 125	ellimciota 45643	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
225		frel 6711	. . . . . . 7 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ → Rel (ℝ D 𝐹))
226	157, 225	syl 17	. . . . . 6 ⊢ (𝜑 → Rel (ℝ D 𝐹))
227		resindm 6017	. . . . . 6 ⊢ (Rel (ℝ D 𝐹) → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
228	226, 227	syl 17	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
229		inss2 4213	. . . . . . 7 ⊢ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
230	229	a1i 11	. . . . . 6 ⊢ (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
231	157, 230	fssresd 6745	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
232	228, 231	feq1dd 6691	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
233	232, 117	fssd 6723	. . 3 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℂ)
234		ioosscn 13425	. . . . 5 ⊢ (-∞(,)𝑋) ⊆ ℂ
235		ssinss1 4221	. . . . 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 2817	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℝ ↔ 𝑦 ∈ ℝ))
245	244	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ 𝑦 ∈ ℝ)))
246		oveq1 7412	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
247	246	fveq2d 6880	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
248		fveq2 6876	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
249	247, 248	eqeq12d 2751	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)))
250	245, 249	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))))
251	250, 111	chvarvv 1998	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))
252	251	ad4ant14 752	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))
253	240, 241, 242, 243, 252	fperiodmul 45333	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))
254	170, 178, 253, 185	fperdvper 45948	. . . . . . . 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 7413	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (π − 𝑤) = (π − 𝑥))
258	257	oveq1d 7420	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((π − 𝑤) / 𝑇) = ((π − 𝑥) / 𝑇))
259	258	fveq2d 6880	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (⌊‘((π − 𝑤) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
260	259	oveq1d 7420	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
261	260	cbvmptv 5225	. . . . . 6 ⊢ (𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
262		eqid 2735	. . . . . 6 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥)))
263	61, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209	fourierdlem41 46177	. . . . 5 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))))
264	263	simpld 494	. . . 4 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)))
265	125	cnfldtop 24722	. . . . . . . . 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 11292	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
269	268	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → -∞ ∈ ℝ^*)
270		rexr 11281	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℝ^*)
271		mnflt 13139	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → -∞ < 𝑦)
272	269, 270, 271	xrltled 13166	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → -∞ ≤ 𝑦)
273		iooss1 13397	. . . . . . . . . . 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 4216	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)))
278		unicntop 24724	. . . . . . . . 9 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
279	278	lpss3 23082	. . . . . . . 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 45674	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)))
286	281, 285	sseldd 3959	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
287	286	rexlimdv3a 3145	. . . 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 7413	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (π − 𝑦) = (π − 𝑥))
291	290	oveq1d 7420	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((π − 𝑦) / 𝑇) = ((π − 𝑥) / 𝑇))
292	291	fveq2d 6880	. . . . . 6 ⊢ (𝑦 = 𝑥 → (⌊‘((π − 𝑦) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
293	292	oveq1d 7420	. . . . 5 ⊢ (𝑦 = 𝑥 → ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
294	293	cbvmptv 5225	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
295		id 22	. . . . . 6 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
296		fveq2 6876	. . . . . 6 ⊢ (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧) = ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥))
297	295, 296	oveq12d 7423	. . . . 5 ⊢ (𝑧 = 𝑥 → (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧)) = (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
298	297	cbvmptv 5225	. . . 4 ⊢ (𝑧 ∈ ℝ ↦ (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
299	61, 62, 161, 23, 71, 24, 25, 155, 157, 256, 289, 134, 169, 58, 294, 298	fourierdlem49 46184	. . 3 ⊢ (𝜑 → (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ≠ ∅)
300	233, 237, 288, 299, 125	ellimciota 45643	. 2 ⊢ (𝜑 → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋)) ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
301		resindm 6017	. . . . . 6 ⊢ (Rel (ℝ D 𝐹) → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
302	226, 301	syl 17	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
303		inss2 4213	. . . . . . 7 ⊢ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
304	303	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
305	157, 304	fssresd 6745	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
306	302, 305	feq1dd 6691	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
307	306, 117	fssd 6723	. . 3 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℂ)
308		ioosscn 13425	. . . . 5 ⊢ (𝑋(,)+∞) ⊆ ℂ
309		ssinss1 4221	. . . . 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 11289	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ^*
316	315	a1i 11	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → +∞ ∈ ℝ^*)
317		ltpnf 13136	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → 𝑦 < +∞)
318	270, 316, 317	xrltled 13166	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → 𝑦 ≤ +∞)
319		iooss2 13398	. . . . . . . . . . 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 4216	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)))
324	278	lpss3 23082	. . . . . . . 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 45675	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)))
331	326, 330	sseldd 3959	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
332	331	rexlimdv3a 3145	. . . 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 46183	. . 3 ⊢ (𝜑 → (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ≠ ∅)
336	307, 311, 333, 335, 125	ellimciota 45643	. 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 6876	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
342		oveq1 7412	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (𝑛 · 𝑋) = (𝑘 · 𝑋))
343	342	fveq2d 6880	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑋)) = (cos‘(𝑘 · 𝑋)))
344	341, 343	oveq12d 7423	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))))
345		fveq2 6876	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝐵‘𝑛) = (𝐵‘𝑘))
346	342	fveq2d 6880	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑋)) = (sin‘(𝑘 · 𝑋)))
347	345, 346	oveq12d 7423	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
348	344, 347	oveq12d 7423	. . . . . 6 ⊢ (𝑛 = 𝑘 → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
349	348	cbvsumv 15712	. . . . 5 ⊢ Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑘 ∈ (1...𝑚)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
350		oveq2 7413	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
351	350	eqcomd 2741	. . . . . 6 ⊢ (𝑗 = 𝑚 → (1...𝑚) = (1...𝑗))
352	351	sumeq1d 15716	. . . . 5 ⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑚)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
353	349, 352	eqtr2id 2783	. . . 4 ⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
354	353	oveq2d 7421	. . 3 ⊢ (𝑗 = 𝑚 → (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
355	354	cbvmptv 5225	. 2 ⊢ (𝑗 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))) = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
356		fourierdlem113.15	. 2 ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
357		fdm 6715	. . . . . 6 ⊢ (𝐹:ℝ⟶ℝ → dom 𝐹 = ℝ)
358	1, 357	syl 17	. . . . 5 ⊢ (𝜑 → dom 𝐹 = ℝ)
359	358, 154	eqsstrd 3993	. . . 4 ⊢ (𝜑 → dom 𝐹 ⊆ ℝ)
360	358	feq2d 6692	. . . . 5 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℝ ↔ 𝐹:ℝ⟶ℝ))
361	1, 360	mpbird 257	. . . 4 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ)
362	359	sselda 3958	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ dom 𝐹) → 𝑡 ∈ ℝ)
363	362	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑡 ∈ ℝ)
364	171	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
365	177	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
366	364, 365	remulcld 11265	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
367	363, 366	readdcld 11264	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ ℝ)
368	358	eqcomd 2741	. . . . . 6 ⊢ (𝜑 → ℝ = dom 𝐹)
369	368	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → ℝ = dom 𝐹)
370	367, 369	eleqtrd 2836	. . . 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 46206	. . 3 ⊢ (𝜑 → ∃𝑢 ∈ ℝ ∀𝑡 ∈ dom 𝐹(abs‘(𝐹‘𝑡)) ≤ 𝑢)
375	358	raleqdv 3305	. . . 4 ⊢ (𝜑 → (∀𝑡 ∈ dom 𝐹(abs‘(𝐹‘𝑡)) ≤ 𝑢 ↔ ∀𝑡 ∈ ℝ (abs‘(𝐹‘𝑡)) ≤ 𝑢))
376	375	rexbidv 3164	. . 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 46247	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 1540 ∈ wcel 2108 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 {crab 3415 ∪ cun 3924 ∩ cin 3925 ⊆ wss 3926 ∅c0 4308 ifcif 4500 {cpr 4603 class class class wbr 5119 ↦ cmpt 5201 dom cdm 5654 ran crn 5655 ↾ cres 5656 Rel wrel 5659 ℩cio 6482 Fun wfun 6525 ⟶wf 6527 ‘cfv 6531 Isom wiso 6532 (class class class)co 7405 ↑_m cmap 8840 Fincfn 8959 ℂcc 11127 ℝcr 11128 0cc0 11129 1c1 11130 + caddc 11132 · cmul 11134 +∞cpnf 11266 -∞cmnf 11267 ℝ^*cxr 11268 < clt 11269 ≤ cle 11270 − cmin 11466 -cneg 11467 / cdiv 11894 ℕcn 12240 2c2 12295 ℕ₀cn0 12501 ℤcz 12588 ℤ_≥cuz 12852 (,)cioo 13362 (,]cioc 13363 [,)cico 13364 [,]cicc 13365 ...cfz 13524 ..^cfzo 13671 ⌊cfl 13807 mod cmo 13886 seqcseq 14019 ♯chash 14348 abscabs 15253 ⇝ cli 15500 Σcsu 15702 sincsin 16079 cosccos 16080 πcpi 16082 TopOpenctopn 17435 topGenctg 17451 ℂ_fldccnfld 21315 Topctop 22831 intcnt 22955 limPtclp 23072 –cn→ccncf 24820 ∫citg 25571 lim_ℂ climc 25815 D cdv 25816

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-inf2 9655 ax-cc 10449 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206 ax-pre-sup 11207 ax-addf 11208

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-symdif 4228 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-disj 5087 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7671 df-ofr 7672 df-om 7862 df-1st 7988 df-2nd 7989 df-supp 8160 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-oadd 8484 df-omul 8485 df-er 8719 df-map 8842 df-pm 8843 df-ixp 8912 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-fsupp 9374 df-fi 9423 df-sup 9454 df-inf 9455 df-oi 9524 df-dju 9915 df-card 9953 df-acn 9956 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-div 11895 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12502 df-xnn0 12575 df-z 12589 df-dec 12709 df-uz 12853 df-q 12965 df-rp 13009 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-ioo 13366 df-ioc 13367 df-ico 13368 df-icc 13369 df-fz 13525 df-fzo 13672 df-fl 13809 df-mod 13887 df-seq 14020 df-exp 14080 df-fac 14292 df-bc 14321 df-hash 14349 df-shft 15086 df-cj 15118 df-re 15119 df-im 15120 df-sqrt 15254 df-abs 15255 df-limsup 15487 df-clim 15504 df-rlim 15505 df-sum 15703 df-ef 16083 df-sin 16085 df-cos 16086 df-pi 16088 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17252 df-plusg 17284 df-mulr 17285 df-starv 17286 df-sca 17287 df-vsca 17288 df-ip 17289 df-tset 17290 df-ple 17291 df-ds 17293 df-unif 17294 df-hom 17295 df-cco 17296 df-rest 17436 df-topn 17437 df-0g 17455 df-gsum 17456 df-topgen 17457 df-pt 17458 df-prds 17461 df-xrs 17516 df-qtop 17521 df-imas 17522 df-xps 17524 df-mre 17598 df-mrc 17599 df-acs 17601 df-mgm 18618 df-sgrp 18697 df-mnd 18713 df-submnd 18762 df-mulg 19051 df-cntz 19300 df-cmn 19763 df-psmet 21307 df-xmet 21308 df-met 21309 df-bl 21310 df-mopn 21311 df-fbas 21312 df-fg 21313 df-cnfld 21316 df-top 22832 df-topon 22849 df-topsp 22871 df-bases 22884 df-cld 22957 df-ntr 22958 df-cls 22959 df-nei 23036 df-lp 23074 df-perf 23075 df-cn 23165 df-cnp 23166 df-t1 23252 df-haus 23253 df-cmp 23325 df-tx 23500 df-hmeo 23693 df-fil 23784 df-fm 23876 df-flim 23877 df-flf 23878 df-xms 24259 df-ms 24260 df-tms 24261 df-cncf 24822 df-ovol 25417 df-vol 25418 df-mbf 25572 df-itg1 25573 df-itg2 25574 df-ibl 25575 df-itg 25576 df-0p 25623 df-ditg 25800 df-limc 25819 df-dv 25820

This theorem is referenced by: fourierdlem114 46249

W3C validator