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 46966

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 7423	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (𝑤 mod (2 · π)) = (𝑦 mod (2 · π)))
3	2	eqeq1d 2767	. . . . . 6 ⊢ (𝑤 = 𝑦 → ((𝑤 mod (2 · π)) = 0 ↔ (𝑦 mod (2 · π)) = 0))
4		oveq2 7424	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → ((𝑘 + (1 / 2)) · 𝑤) = ((𝑘 + (1 / 2)) · 𝑦))
5	4	fveq2d 6889	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (sin‘((𝑘 + (1 / 2)) · 𝑤)) = (sin‘((𝑘 + (1 / 2)) · 𝑦)))
6		fvoveq1 7439	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (sin‘(𝑤 / 2)) = (sin‘(𝑦 / 2)))
7	6	oveq2d 7432	. . . . . . 7 ⊢ (𝑤 = 𝑦 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑦 / 2))))
8	5, 7	oveq12d 7434	. . . . . 6 ⊢ (𝑤 = 𝑦 → ((sin‘((𝑘 + (1 / 2)) · 𝑤)) / ((2 · π) · (sin‘(𝑤 / 2)))) = ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
9	3, 8	ifbieq2d 4516	. . . . 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))))))
10	9	cbvmptv 5217	. . . 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))))))
11		oveq2 7424	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (2 · 𝑘) = (2 · 𝑚))
12	11	oveq1d 7431	. . . . . . 7 ⊢ (𝑘 = 𝑚 → ((2 · 𝑘) + 1) = ((2 · 𝑚) + 1))
13	12	oveq1d 7431	. . . . . 6 ⊢ (𝑘 = 𝑚 → (((2 · 𝑘) + 1) / (2 · π)) = (((2 · 𝑚) + 1) / (2 · π)))
14		oveq1 7423	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (𝑘 + (1 / 2)) = (𝑚 + (1 / 2)))
15	14	fvoveq1d 7438	. . . . . . 7 ⊢ (𝑘 = 𝑚 → (sin‘((𝑘 + (1 / 2)) · 𝑦)) = (sin‘((𝑚 + (1 / 2)) · 𝑦)))
16	15	oveq1d 7431	. . . . . 6 ⊢ (𝑘 = 𝑚 → ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
17	13, 16	ifeq12d 4511	. . . . 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))))))
18	17	mpteq2dv 5207	. . . 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)))))))
19	10, 18	eqtrid 2812	. . 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)))))))
20	19	cbvmptv 5217	. 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)))))))
21		fourierdlem113.p	. 2 ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
22		fourierdlem113.m	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
23		fourierdlem113.q	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
24		oveq1 7423	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (𝑤 + (𝑗 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
25	24	eleq1d 2850	. . . . . . 7 ⊢ (𝑤 = 𝑦 → ((𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
26	25	rexbidv 3191	. . . . . 6 ⊢ (𝑤 = 𝑦 → (∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
27	26	cbvrabv 3428	. . . . 5 ⊢ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
28	27	uneq2i 4119	. . . 4 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
29	28	fveq2i 6888	. . 3 ⊢ (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) = (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
30	29	oveq1i 7426	. 2 ⊢ ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
31		oveq1 7423	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
32	31	oveq2d 7432	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
33	32	eleq1d 2850	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
34	33	cbvrexvw 3246	. . . . . . . 8 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄)
35	34	rabbii 3423	. . . . . . 7 ⊢ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
36	35	uneq2i 4119	. . . . . 6 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
37		isoeq5 7325	. . . . . 6 ⊢ (({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}) → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
38	36, 37	ax-mp 5	. . . . 5 ⊢ (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
39	38	a1i 11	. . . 4 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
40	31	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (𝑤 + (𝑘 · 𝑇)) = (𝑤 + (𝑗 · 𝑇)))
41	40	eleq1d 2850	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑗 → ((𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
42	41	cbvrexvw 3246	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄)
43	42	rabbii 3423	. . . . . . . . . 10 ⊢ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}
44	43	uneq2i 4119	. . . . . . . . 9 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})
45	44	fveq2i 6888	. . . . . . . 8 ⊢ (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
46	45	oveq1i 7426	. . . . . . 7 ⊢ ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
47	46	oveq2i 7427	. . . . . 6 ⊢ (0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)) = (0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1))
48		isoeq4 7324	. . . . . 6 ⊢ ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)) = (0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)) → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
49	47, 48	ax-mp 5	. . . . 5 ⊢ (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
50	49	a1i 11	. . . 4 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
51		isoeq1 7321	. . . 4 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
52	39, 50, 51	3bitrd 308	. . 3 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
53	52	cbviotavw 6504	. 2 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
54		fourierdlem113.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℝ)
55		pire 26650	. . . . 5 ⊢ π ∈ ℝ
56	55	renegcli 11530	. . . 4 ⊢ -π ∈ ℝ
57	56	a1i 11	. . 3 ⊢ (𝜑 → -π ∈ ℝ)
58	55	a1i 11	. . 3 ⊢ (𝜑 → π ∈ ℝ)
59		negpilt0 46033	. . . 4 ⊢ -π < 0
60	59	a1i 11	. . 3 ⊢ (𝜑 → -π < 0)
61		pipos 26654	. . . 4 ⊢ 0 < π
62	61	a1i 11	. . 3 ⊢ (𝜑 → 0 < π)
63		picn 26652	. . . . 5 ⊢ π ∈ ℂ
64	63	2timesi 12389	. . . 4 ⊢ (2 · π) = (π + π)
65		fourierdlem113.t	. . . 4 ⊢ 𝑇 = (2 · π)
66	63, 63	subnegi 11548	. . . 4 ⊢ (π − -π) = (π + π)
67	64, 65, 66	3eqtr4i 2798	. . 3 ⊢ 𝑇 = (π − -π)
68	21	fourierdlem2 46856	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
69	22, 68	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
70	23, 69	mpbid 235	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
71	70	simpld 500	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
72		elmapi 8848	. . . . 5 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
73	71, 72	syl 18	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
74		fzfid 14023	. . . 4 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
75		rnffi 45926	. . . 4 ⊢ ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin)
76	73, 74, 75	syl2anc 596	. . 3 ⊢ (𝜑 → ran 𝑄 ∈ Fin)
77	21, 22, 23	fourierdlem15 46869	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
78	77	frnd 6718	. . 3 ⊢ (𝜑 → ran 𝑄 ⊆ (-π[,]π))
79	70	simprd 501	. . . . 5 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
80	79	simplrd 782	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = π)
81	77	ffund 6714	. . . . 5 ⊢ (𝜑 → Fun 𝑄)
82	22	nnnn0d 12576	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
83		nn0uz 12912	. . . . . . . 8 ⊢ ℕ₀ = (ℤ_≥‘0)
84	82, 83	eleqtrdi 2875	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
85		eluzfz2 13572	. . . . . . 7 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
86	84, 85	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
87	77	fdmd 6720	. . . . . . 7 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
88	87	eqcomd 2771	. . . . . 6 ⊢ (𝜑 → (0...𝑀) = dom 𝑄)
89	86, 88	eleqtrd 2867	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ dom 𝑄)
90		fvelrn 7075	. . . . 5 ⊢ ((Fun 𝑄 ∧ 𝑀 ∈ dom 𝑄) → (𝑄‘𝑀) ∈ ran 𝑄)
91	81, 89, 90	syl2anc 596	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ran 𝑄)
92	80, 91	eqeltrrd 2866	. . 3 ⊢ (𝜑 → π ∈ ran 𝑄)
93		fourierdlem113.e	. . 3 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
94		fourierdlem113.exq	. . 3 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄)
95		eqid 2765	. . 3 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
96		isoeq1 7321	. . . . 5 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
97	28, 44, 36	3eqtr4ri 2799	. . . . . 6 ⊢ ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
98		isoeq5 7325	. . . . . 6 ⊢ (({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) → (𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
99	97, 98	ax-mp 5	. . . . 5 ⊢ (𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
100	96, 99	bitrdi 290	. . . 4 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
101	100	cbviotavw 6504	. . 3 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
102		eqid 2765	. . 3 ⊢ {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
103	57, 58, 60, 62, 67, 76, 78, 92, 93, 54, 94, 95, 101, 102	fourierdlem51 46904	. 2 ⊢ (𝜑 → 𝑋 ∈ ran (℩𝑔𝑔 Isom < , < ((0...((♯‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
104		fourierdlem113.per	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
105		ax-resscn 11168	. . . 4 ⊢ ℝ ⊆ ℂ
106	105	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℂ)
107		ioossre 13446	. . . . . . 7 ⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
108	107	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
109	1, 108	fssresd 6749	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
110	105	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℂ)
111	109, 110	fssd 6727	. . . 4 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
112	111	adantr 486	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
113	107	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
114	1, 110	fssd 6727	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
115	114	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
116		ssidd 3961	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℝ)
117		eqid 2765	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
118		tgioo4 24993	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
119	117, 118	dvres 26101	. . . . . 6 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
120	106, 115, 116, 113, 119	syl22anc 852	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
121	120	dmeqd 5897	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))))
122		ioontr 46260	. . . . . . 7 ⊢ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))
123	122	reseq2i 5977	. . . . . 6 ⊢ ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
124	123	dmeqi 5896	. . . . 5 ⊢ dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
125	124	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
126		fourierdlem113.dvcn	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
127		cncff 25083	. . . . 5 ⊢ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
128		fdm 6719	. . . . 5 ⊢ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
129	126, 127, 128	3syl 19	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
130	121, 125, 129	3eqtrd 2804	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
131		dvcn 26111	. . 3 ⊢ (((ℝ ⊆ ℂ ∧ (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ) ∧ dom (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
132	106, 112, 113, 130, 131	syl31anc 1400	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
133	113, 106	sstrd 3948	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
134	73	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
135		fzofzp1 13806	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
136	135	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
137	134, 136	ffvelcdmd 7084	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
138	137	rexrd 11270	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ^*)
139		elfzofz 13717	. . . . . 6 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
140	139	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
141	134, 140	ffvelcdmd 7084	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
142	70	simprrd 786	. . . . 5 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
143	142	r19.21bi 3259	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
144	117, 138, 141, 143	lptioo1cn 46393	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
145	109	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
146		ssidd 3961	. . . . . . . 8 ⊢ (𝜑 → ℝ ⊆ ℝ)
147	110, 114, 146	dvbss 26091	. . . . . . 7 ⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ ℝ)
148		dvfre 26141	. . . . . . . 8 ⊢ ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
149	1, 146, 148	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
150		0re 11221	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
151	56, 150, 55	lttri 11347	. . . . . . . . 9 ⊢ ((-π < 0 ∧ 0 < π) → -π < π)
152	59, 61, 151	mp2an 705	. . . . . . . 8 ⊢ -π < π
153	152	a1i 11	. . . . . . 7 ⊢ (𝜑 → -π < π)
154	79	simplld 780	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) = -π)
155	126, 127	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
156		fourierdlem113.dvlb	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
157	155, 133, 144, 156, 117	ellimciota 46363	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
158	141	rexrd 11270	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ^*)
159	117, 158, 137, 143	lptioo2cn 46392	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
160		fourierdlem113.dvub	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
161	155, 133, 159, 160, 117	ellimciota 46363	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∈ (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
162	114	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
163		zre 12606	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
164	163	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
165		2pire 26651	. . . . . . . . . . . . . 14 ⊢ (2 · π) ∈ ℝ
166	165	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · π) ∈ ℝ)
167	65, 166	eqeltrid 2869	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℝ)
168	167	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
169	164, 168	remulcld 11250	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
170	162	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
171	168	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℝ)
172		simplr 781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑘 ∈ ℤ)
173		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
174	104	ad4ant14 765	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
175	170, 171, 172, 173, 174	fperiodmul 46056	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹‘𝑡))
176		eqid 2765	. . . . . . . . . 10 ⊢ (ℝ D 𝐹) = (ℝ D 𝐹)
177	162, 169, 175, 176	fperdvper 46666	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑡 ∈ dom (ℝ D 𝐹)) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡)))
178	177	an32s 665	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡)))
179	178	simpld 500	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹))
180	178	simprd 501	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡))
181		fveq2 6885	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑄‘𝑗) = (𝑄‘𝑖))
182		fvoveq1 7439	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑄‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)))
183	181, 182	oveq12d 7434	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
184	183	cbvmptv 5217	. . . . . . 7 ⊢ (𝑗 ∈ (0..^𝑀) ↦ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1)))) = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
185		eqid 2765	. . . . . . 7 ⊢ (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇))) = (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇)))
186	147, 149, 57, 58, 153, 67, 22, 73, 154, 80, 126, 157, 161, 179, 180, 184, 185	fourierdlem71 46924	. . . . . 6 ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
187	186	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
188		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0..^𝑀))
189		nfra1 3291	. . . . . . . . 9 ⊢ Ⅎ𝑡∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧
190	188, 189	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
191	120, 123	eqtrdi 2816	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
192	191	fveq1d 6887	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡))
193		fvres 6904	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
194	192, 193	sylan9eq 2820	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
195	194	fveq2d 6889	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡)))
196	195	adantlr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡)))
197		simplr 781	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
198		ssdmres 6014	. . . . . . . . . . . . 13 ⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
199	129, 198	sylibr 237	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹))
200	199	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹))
201		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
202	200, 201	sseldd 3939	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ dom (ℝ D 𝐹))
203		rspa 3256	. . . . . . . . . 10 ⊢ ((∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 ∧ 𝑡 ∈ dom (ℝ D 𝐹)) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
204	197, 202, 203	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
205	196, 204	eqbrtrd 5135	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
206	190, 205	ralrimia 3266	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) → ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
207	206	ex 418	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 → ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
208	207	reximdv 3182	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
209	187, 208	mpd 16	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
210	141, 137, 145, 130, 209	ioodvbdlimc1 46680	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
211	112, 133, 144, 210, 117	ellimciota 46363	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
212	141, 137, 145, 130, 209	ioodvbdlimc2 46682	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
213	112, 133, 159, 212, 117	ellimciota 46363	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
214		resindm 6031	. . . . . 6 ⊢ ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋))
215	214	a1i 11	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
216		inss2 4190	. . . . . . 7 ⊢ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
217	216	a1i 11	. . . . . 6 ⊢ (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
218	149, 217	fssresd 6749	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
219	215, 218	feq1dd 6692	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
220	219, 110	fssd 6727	. . 3 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℂ)
221		ioosscn 13447	. . . . 5 ⊢ (-∞(,)𝑋) ⊆ ℂ
222		ssinss1 4198	. . . . 5 ⊢ ((-∞(,)𝑋) ⊆ ℂ → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
223	221, 222	ax-mp 5	. . . 4 ⊢ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ
224	223	a1i 11	. . 3 ⊢ (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
225		3simpb 1167	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → (𝜑 ∧ 𝑘 ∈ ℤ))
226		simp2 1155	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ dom (ℝ D 𝐹))
227	162	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
228	168	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
229		simplr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℤ)
230		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
231		eleq1w 2848	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ ℝ ↔ 𝑦 ∈ ℝ))
232	231	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ 𝑦 ∈ ℝ)))
233		fvoveq1 7439	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
234		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
235	233, 234	eqeq12d 2781	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)))
236	232, 235	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))))
237	236, 104	chvarvv 2022	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))
238	237	ad4ant14 765	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))
239	227, 228, 229, 230, 238	fperiodmul 46056	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))
240	162, 169, 239, 176	fperdvper 46666	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℤ) ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥)))
241	225, 226, 240	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥)))
242	241	simpld 500	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹))
243		oveq2 7424	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (π − 𝑤) = (π − 𝑥))
244	243	fvoveq1d 7438	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (⌊‘((π − 𝑤) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
245	244	oveq1d 7431	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
246	245	cbvmptv 5217	. . . . . 6 ⊢ (𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
247		eqid 2765	. . . . . 6 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥)))
248	57, 58, 153, 67, 242, 54, 246, 247, 21, 22, 23, 199	fourierdlem41 46895	. . . . 5 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))))
249	248	simpld 500	. . . 4 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)))
250	117	cnfldtop 24971	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) ∈ Top
251		mnfxr 11277	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
252		rexr 11266	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℝ^*)
253	252	mnfled 13173	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → -∞ ≤ 𝑦)
254		iooss1 13419	. . . . . . . . . . 11 ⊢ ((-∞ ∈ ℝ^* ∧ -∞ ≤ 𝑦) → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
255	251, 253, 254	sylancr 599	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
256	255	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
257		simp3 1156	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))
258	256, 257	ssind 4193	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)))
259		unicntop 24973	. . . . . . . . 9 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
260	259	lpss3 23331	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ ∧ (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
261	250, 223, 258, 260	mp3an12i 1494	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
262	261	3adant3l 1199	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
263	252	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑦 ∈ ℝ^*)
264	54	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ℝ)
265		simp3l 1220	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑦 < 𝑋)
266	117, 263, 264, 265	lptioo2cn 46392	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝑦(,)𝑋)))
267	262, 266	sseldd 3939	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
268	267	rexlimdv3a 3172	. . . 4 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)))))
269	249, 268	mpd 16	. . 3 ⊢ (𝜑 → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
270	241	simprd 501	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥))
271		oveq2 7424	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (π − 𝑦) = (π − 𝑥))
272	271	fvoveq1d 7438	. . . . . 6 ⊢ (𝑦 = 𝑥 → (⌊‘((π − 𝑦) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
273	272	oveq1d 7431	. . . . 5 ⊢ (𝑦 = 𝑥 → ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
274	273	cbvmptv 5217	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
275		id 23	. . . . . 6 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
276		fveq2 6885	. . . . . 6 ⊢ (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧) = ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥))
277	275, 276	oveq12d 7434	. . . . 5 ⊢ (𝑧 = 𝑥 → (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧)) = (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
278	277	cbvmptv 5217	. . . 4 ⊢ (𝑧 ∈ ℝ ↦ (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
279	57, 58, 153, 21, 67, 22, 23, 147, 149, 242, 270, 126, 161, 54, 274, 278	fourierdlem49 46902	. . 3 ⊢ (𝜑 → (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ≠ ∅)
280	220, 224, 269, 279, 117	ellimciota 46363	. 2 ⊢ (𝜑 → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋)) ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
281		resindm 6031	. . . . . 6 ⊢ ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞))
282	281	a1i 11	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
283		inss2 4190	. . . . . . 7 ⊢ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
284	283	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
285	149, 284	fssresd 6749	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
286	282, 285	feq1dd 6692	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
287	286, 110	fssd 6727	. . 3 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℂ)
288		ioosscn 13447	. . . . 5 ⊢ (𝑋(,)+∞) ⊆ ℂ
289		ssinss1 4198	. . . . 5 ⊢ ((𝑋(,)+∞) ⊆ ℂ → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
290	288, 289	ax-mp 5	. . . 4 ⊢ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ
291	290	a1i 11	. . 3 ⊢ (𝜑 → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
292	248	simprd 501	. . . 4 ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)))
293		pnfxr 11274	. . . . . . . . . . 11 ⊢ +∞ ∈ ℝ^*
294	252	pnfged 13168	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ → 𝑦 ≤ +∞)
295		iooss2 13420	. . . . . . . . . . 11 ⊢ ((+∞ ∈ ℝ^* ∧ 𝑦 ≤ +∞) → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
296	293, 294, 295	sylancr 599	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
297	296	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
298		simp3 1156	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))
299	297, 298	ssind 4193	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)))
300	259	lpss3 23331	. . . . . . . 8 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ ∧ (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
301	250, 290, 299, 300	mp3an12i 1494	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
302	301	3adant3l 1199	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
303	252	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑦 ∈ ℝ^*)
304	54	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ℝ)
305		simp3l 1220	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 < 𝑦)
306	117, 303, 304, 305	lptioo1cn 46393	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘(𝑋(,)𝑦)))
307	302, 306	sseldd 3939	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
308	307	rexlimdv3a 3172	. . . 4 ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)))))
309	292, 308	mpd 16	. . 3 ⊢ (𝜑 → 𝑋 ∈ ((limPt‘(TopOpen‘ℂ_fld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
310		biid 264	. . . 4 ⊢ (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ ℤ) ∧ 𝑤 = (𝑋 + (𝑘 · 𝑇))) ↔ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ ℤ) ∧ 𝑤 = (𝑋 + (𝑘 · 𝑇))))
311	57, 58, 153, 21, 67, 22, 23, 149, 242, 270, 126, 157, 54, 274, 278, 310	fourierdlem48 46901	. . 3 ⊢ (𝜑 → (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ≠ ∅)
312	287, 291, 309, 311, 117	ellimciota 46363	. 2 ⊢ (𝜑 → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim_ℂ 𝑋)) ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
313		fourierdlem113.l	. 2 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
314		fourierdlem113.r	. 2 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
315		fourierdlem113.a	. 2 ⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
316		fourierdlem113.b	. 2 ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
317		fveq2 6885	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
318		fvoveq1 7439	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑋)) = (cos‘(𝑘 · 𝑋)))
319	317, 318	oveq12d 7434	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))))
320		fveq2 6885	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝐵‘𝑛) = (𝐵‘𝑘))
321		fvoveq1 7439	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑋)) = (sin‘(𝑘 · 𝑋)))
322	320, 321	oveq12d 7434	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
323	319, 322	oveq12d 7434	. . . . . 6 ⊢ (𝑛 = 𝑘 → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
324	323	cbvsumv 15767	. . . . 5 ⊢ Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑘 ∈ (1...𝑚)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
325		oveq2 7424	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
326	325	eqcomd 2771	. . . . . 6 ⊢ (𝑗 = 𝑚 → (1...𝑚) = (1...𝑗))
327	326	sumeq1d 15771	. . . . 5 ⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑚)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
328	324, 327	eqtr2id 2813	. . . 4 ⊢ (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
329	328	oveq2d 7432	. . 3 ⊢ (𝑗 = 𝑚 → (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
330	329	cbvmptv 5217	. 2 ⊢ (𝑗 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))) = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
331		fourierdlem113.15	. 2 ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
332	1	fdmd 6720	. . . . 5 ⊢ (𝜑 → dom 𝐹 = ℝ)
333	332	eqimssd 3994	. . . 4 ⊢ (𝜑 → dom 𝐹 ⊆ ℝ)
334	1	ffdmd 6740	. . . 4 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ)
335	333	sselda 3938	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ dom 𝐹) → 𝑡 ∈ ℝ)
336	335	adantr 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑡 ∈ ℝ)
337	163	adantl 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
338	168	adantlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
339	337, 338	remulcld 11250	. . . . . 6 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
340	336, 339	readdcld 11249	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ ℝ)
341	332	eqcomd 2771	. . . . . 6 ⊢ (𝜑 → ℝ = dom 𝐹)
342	341	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → ℝ = dom 𝐹)
343	340, 342	eleqtrd 2867	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ dom 𝐹)
344		id 23	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (𝜑 ∧ 𝑘 ∈ ℤ))
345	344	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝜑 ∧ 𝑘 ∈ ℤ))
346	345, 336, 175	syl2anc 596	. . . 4 ⊢ (((𝜑 ∧ 𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹‘𝑡))
347	333, 334, 57, 58, 153, 67, 22, 73, 154, 80, 132, 211, 213, 343, 346, 184, 185	fourierdlem71 46924	. . 3 ⊢ (𝜑 → ∃𝑢 ∈ ℝ ∀𝑡 ∈ dom 𝐹(abs‘(𝐹‘𝑡)) ≤ 𝑢)
348	332	raleqdv 3325	. . . 4 ⊢ (𝜑 → (∀𝑡 ∈ dom 𝐹(abs‘(𝐹‘𝑡)) ≤ 𝑢 ↔ ∀𝑡 ∈ ℝ (abs‘(𝐹‘𝑡)) ≤ 𝑢))
349	348	rexbidv 3191	. . 3 ⊢ (𝜑 → (∃𝑢 ∈ ℝ ∀𝑡 ∈ dom 𝐹(abs‘(𝐹‘𝑡)) ≤ 𝑢 ↔ ∃𝑢 ∈ ℝ ∀𝑡 ∈ ℝ (abs‘(𝐹‘𝑡)) ≤ 𝑢))
350	347, 349	mpbid 235	. 2 ⊢ (𝜑 → ∃𝑢 ∈ ℝ ∀𝑡 ∈ ℝ (abs‘(𝐹‘𝑡)) ≤ 𝑢)
351	1, 20, 21, 22, 23, 30, 53, 54, 103, 65, 104, 132, 211, 213, 126, 280, 312, 313, 314, 315, 316, 330, 331, 350, 186, 54	fourierdlem112 46965	1 ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 {crab 3418 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4286 ifcif 4489 {cpr 4593 class class class wbr 5111 ↦ cmpt 5194 dom cdm 5663 ran crn 5664 ↾ cres 5665 ℩cio 6494 Fun wfun 6534 ⟶wf 6536 ‘cfv 6540 Isom wiso 6541 (class class class)co 7416 ↑_m cmap 8826 Fincfn 8945 ℂcc 11109 ℝcr 11110 0cc0 11111 1c1 11112 + caddc 11114 · cmul 11116 +∞cpnf 11251 -∞cmnf 11252 ℝ^*cxr 11253 < clt 11254 ≤ cle 11255 − cmin 11452 -cneg 11453 / cdiv 11882 ℕcn 12244 2c2 12306 ℕ₀cn0 12515 ℤcz 12602 ℤ_≥cuz 12874 (,)cioo 13384 (,]cioc 13385 [,)cico 13386 [,]cicc 13387 ...cfz 13547 ..^cfzo 13695 ⌊cfl 13837 mod cmo 13916 seqcseq 14051 ♯chash 14380 abscabs 15305 ⇝ cli 15555 Σcsu 15757 sincsin 16135 cosccos 16136 πcpi 16138 TopOpenctopn 17492 topGenctg 17508 ℂ_fldccnfld 21552 Topctop 23080 intcnt 23204 limPtclp 23321 –cn→ccncf 25066 ∫citg 25808 lim_ℂ climc 26052 D cdv 26053

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-inf2 9613 ax-cc 10430 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188 ax-pre-sup 11189 ax-addf 11190

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-symdif 4206 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-disj 5079 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7680 df-ofr 7681 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-oadd 8459 df-omul 8460 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9325 df-fi 9374 df-sup 9405 df-inf 9406 df-oi 9475 df-dju 9899 df-card 9937 df-acn 9940 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-div 11883 df-nn 12245 df-2 12314 df-3 12315 df-4 12316 df-5 12317 df-6 12318 df-7 12319 df-8 12320 df-9 12321 df-n0 12516 df-xnn0 12589 df-z 12603 df-dec 12724 df-uz 12875 df-q 12985 df-rp 13029 df-xneg 13149 df-xadd 13150 df-xmul 13151 df-ioo 13388 df-ioc 13389 df-ico 13390 df-icc 13391 df-fz 13548 df-fzo 13696 df-fl 13839 df-mod 13917 df-seq 14052 df-exp 14112 df-fac 14324 df-bc 14353 df-hash 14381 df-shft 15124 df-cj 15170 df-re 15171 df-im 15172 df-sqrt 15306 df-abs 15307 df-limsup 15542 df-clim 15559 df-rlim 15560 df-sum 15758 df-ef 16139 df-sin 16141 df-cos 16142 df-pi 16144 df-struct 17225 df-sets 17242 df-slot 17260 df-ndx 17272 df-base 17288 df-ress 17309 df-plusg 17341 df-mulr 17342 df-starv 17343 df-sca 17344 df-vsca 17345 df-ip 17346 df-tset 17347 df-ple 17348 df-ds 17350 df-unif 17351 df-hom 17352 df-cco 17353 df-rest 17493 df-topn 17494 df-0g 17512 df-gsum 17513 df-topgen 17514 df-pt 17515 df-prds 17518 df-xrs 17574 df-qtop 17579 df-imas 17580 df-xps 17582 df-mre 17656 df-mrc 17657 df-acs 17659 df-mgm 18716 df-sgrp 18799 df-mnd 18815 df-submnd 18866 df-mulg 19158 df-cntz 19411 df-cmn 19876 df-psmet 21544 df-xmet 21545 df-met 21546 df-bl 21547 df-mopn 21548 df-fbas 21549 df-fg 21550 df-cnfld 21553 df-top 23081 df-topon 23098 df-topsp 23120 df-bases 23133 df-cld 23206 df-ntr 23207 df-cls 23208 df-nei 23285 df-lp 23323 df-perf 23324 df-cn 23414 df-cnp 23415 df-t1 23501 df-haus 23502 df-cmp 23574 df-tx 23750 df-hmeo 23943 df-fil 24034 df-fm 24126 df-flim 24127 df-flf 24128 df-xms 24508 df-ms 24509 df-tms 24510 df-cncf 25068 df-ovol 25654 df-vol 25655 df-mbf 25809 df-itg1 25810 df-itg2 25811 df-ibl 25812 df-itg 25813 df-0p 25860 df-ditg 26037 df-limc 26056 df-dv 26057

This theorem is used by: fourierdlem114 46967

W3C validator