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

Theorem fourierdlem113 39743
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 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (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 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹𝑥) · (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.
StepHypRef Expression
1 fourierdlem113.f . 2 (𝜑𝐹:ℝ⟶ℝ)
2 oveq1 6611 . . . . . . 7 (𝑤 = 𝑦 → (𝑤 mod (2 · π)) = (𝑦 mod (2 · π)))
32eqeq1d 2623 . . . . . 6 (𝑤 = 𝑦 → ((𝑤 mod (2 · π)) = 0 ↔ (𝑦 mod (2 · π)) = 0))
4 oveq2 6612 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑘 + (1 / 2)) · 𝑤) = ((𝑘 + (1 / 2)) · 𝑦))
54fveq2d 6152 . . . . . . 7 (𝑤 = 𝑦 → (sin‘((𝑘 + (1 / 2)) · 𝑤)) = (sin‘((𝑘 + (1 / 2)) · 𝑦)))
6 oveq1 6611 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑤 / 2) = (𝑦 / 2))
76fveq2d 6152 . . . . . . . 8 (𝑤 = 𝑦 → (sin‘(𝑤 / 2)) = (sin‘(𝑦 / 2)))
87oveq2d 6620 . . . . . . 7 (𝑤 = 𝑦 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑦 / 2))))
95, 8oveq12d 6622 . . . . . 6 (𝑤 = 𝑦 → ((sin‘((𝑘 + (1 / 2)) · 𝑤)) / ((2 · π) · (sin‘(𝑤 / 2)))) = ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
103, 9ifbieq2d 4083 . . . . 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))))))
1110cbvmptv 4710 . . . 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 6612 . . . . . . . 8 (𝑘 = 𝑚 → (2 · 𝑘) = (2 · 𝑚))
1312oveq1d 6619 . . . . . . 7 (𝑘 = 𝑚 → ((2 · 𝑘) + 1) = ((2 · 𝑚) + 1))
1413oveq1d 6619 . . . . . 6 (𝑘 = 𝑚 → (((2 · 𝑘) + 1) / (2 · π)) = (((2 · 𝑚) + 1) / (2 · π)))
15 oveq1 6611 . . . . . . . . 9 (𝑘 = 𝑚 → (𝑘 + (1 / 2)) = (𝑚 + (1 / 2)))
1615oveq1d 6619 . . . . . . . 8 (𝑘 = 𝑚 → ((𝑘 + (1 / 2)) · 𝑦) = ((𝑚 + (1 / 2)) · 𝑦))
1716fveq2d 6152 . . . . . . 7 (𝑘 = 𝑚 → (sin‘((𝑘 + (1 / 2)) · 𝑦)) = (sin‘((𝑚 + (1 / 2)) · 𝑦)))
1817oveq1d 6619 . . . . . 6 (𝑘 = 𝑚 → ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
1914, 18ifeq12d 4078 . . . . 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))))))
2019mpteq2dv 4705 . . . 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)))))))
2111, 20syl5eq 2667 . . 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)))))))
2221cbvmptv 4710 . 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 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
24 fourierdlem113.m . 2 (𝜑𝑀 ∈ ℕ)
25 fourierdlem113.q . 2 (𝜑𝑄 ∈ (𝑃𝑀))
26 oveq1 6611 . . . . . . . 8 (𝑤 = 𝑦 → (𝑤 + (𝑗 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
2726eleq1d 2683 . . . . . . 7 (𝑤 = 𝑦 → ((𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
2827rexbidv 3045 . . . . . 6 (𝑤 = 𝑦 → (∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
2928cbvrabv 3185 . . . . 5 {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
3029uneq2i 3742 . . . 4 ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
3130fveq2i 6151 . . 3 (#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) = (#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
3231oveq1i 6614 . 2 ((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1) = ((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
33 oveq1 6611 . . . . . . . . . . . 12 (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
3433oveq2d 6620 . . . . . . . . . . 11 (𝑘 = 𝑗 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
3534eleq1d 2683 . . . . . . . . . 10 (𝑘 = 𝑗 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
3635cbvrexv 3160 . . . . . . . . 9 (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄)
3736a1i 11 . . . . . . . 8 (𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
3837rabbiia 3173 . . . . . . 7 {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
3938uneq2i 3742 . . . . . 6 ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
40 isoeq5 6525 . . . . . 6 (({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}) → (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
4139, 40ax-mp 5 . . . . 5 (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
4241a1i 11 . . . 4 (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
4333oveq2d 6620 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (𝑤 + (𝑘 · 𝑇)) = (𝑤 + (𝑗 · 𝑇)))
4443eleq1d 2683 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → ((𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
4544cbvrexv 3160 . . . . . . . . . . . 12 (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄)
4645a1i 11 . . . . . . . . . . 11 (𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) → (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
4746rabbiia 3173 . . . . . . . . . 10 {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}
4847uneq2i 3742 . . . . . . . . 9 ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})
4948fveq2i 6151 . . . . . . . 8 (#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
5049oveq1i 6614 . . . . . . 7 ((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
5150oveq2i 6615 . . . . . 6 (0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)) = (0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1))
52 isoeq4 6524 . . . . . 6 ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)) = (0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)) → (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
5351, 52ax-mp 5 . . . . 5 (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
5453a1i 11 . . . 4 (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
55 isoeq1 6521 . . . 4 (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
5642, 54, 553bitrd 294 . . 3 (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))))
5756cbviotav 5816 . 2 (℩𝑔𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
58 fourierdlem113.x . 2 (𝜑𝑋 ∈ ℝ)
59 pire 24114 . . . . 5 π ∈ ℝ
6059renegcli 10286 . . . 4 -π ∈ ℝ
6160a1i 11 . . 3 (𝜑 → -π ∈ ℝ)
6259a1i 11 . . 3 (𝜑 → π ∈ ℝ)
63 negpilt0 38956 . . . 4 -π < 0
6463a1i 11 . . 3 (𝜑 → -π < 0)
65 pipos 24116 . . . 4 0 < π
6665a1i 11 . . 3 (𝜑 → 0 < π)
67 picn 24115 . . . . 5 π ∈ ℂ
68672timesi 11091 . . . 4 (2 · π) = (π + π)
69 fourierdlem113.t . . . 4 𝑇 = (2 · π)
7067, 67subnegi 10304 . . . 4 (π − -π) = (π + π)
7168, 69, 703eqtr4i 2653 . . 3 𝑇 = (π − -π)
7223fourierdlem2 39633 . . . . . . . 8 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
7324, 72syl 17 . . . . . . 7 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
7425, 73mpbid 222 . . . . . 6 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
7574simpld 475 . . . . 5 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
76 elmapi 7823 . . . . 5 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
7775, 76syl 17 . . . 4 (𝜑𝑄:(0...𝑀)⟶ℝ)
78 fzfid 12712 . . . 4 (𝜑 → (0...𝑀) ∈ Fin)
79 rnffi 38830 . . . 4 ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin)
8077, 78, 79syl2anc 692 . . 3 (𝜑 → ran 𝑄 ∈ Fin)
8123, 24, 25fourierdlem15 39646 . . . 4 (𝜑𝑄:(0...𝑀)⟶(-π[,]π))
82 frn 6010 . . . 4 (𝑄:(0...𝑀)⟶(-π[,]π) → ran 𝑄 ⊆ (-π[,]π))
8381, 82syl 17 . . 3 (𝜑 → ran 𝑄 ⊆ (-π[,]π))
8474simprd 479 . . . . 5 (𝜑 → (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))
8584simplrd 792 . . . 4 (𝜑 → (𝑄𝑀) = π)
86 ffun 6005 . . . . . 6 (𝑄:(0...𝑀)⟶(-π[,]π) → Fun 𝑄)
8781, 86syl 17 . . . . 5 (𝜑 → Fun 𝑄)
8824nnnn0d 11295 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
89 nn0uz 11666 . . . . . . . 8 0 = (ℤ‘0)
9088, 89syl6eleq 2708 . . . . . . 7 (𝜑𝑀 ∈ (ℤ‘0))
91 eluzfz2 12291 . . . . . . 7 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
9290, 91syl 17 . . . . . 6 (𝜑𝑀 ∈ (0...𝑀))
93 fdm 6008 . . . . . . . 8 (𝑄:(0...𝑀)⟶(-π[,]π) → dom 𝑄 = (0...𝑀))
9481, 93syl 17 . . . . . . 7 (𝜑 → dom 𝑄 = (0...𝑀))
9594eqcomd 2627 . . . . . 6 (𝜑 → (0...𝑀) = dom 𝑄)
9692, 95eleqtrd 2700 . . . . 5 (𝜑𝑀 ∈ dom 𝑄)
97 fvelrn 6308 . . . . 5 ((Fun 𝑄𝑀 ∈ dom 𝑄) → (𝑄𝑀) ∈ ran 𝑄)
9887, 96, 97syl2anc 692 . . . 4 (𝜑 → (𝑄𝑀) ∈ ran 𝑄)
9985, 98eqeltrrd 2699 . . 3 (𝜑 → π ∈ ran 𝑄)
100 fourierdlem113.e . . 3 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
101 fourierdlem113.exq . . 3 (𝜑 → (𝐸𝑋) ∈ ran 𝑄)
102 eqid 2621 . . 3 ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
103 isoeq1 6521 . . . . 5 (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
10430, 48, 393eqtr4ri 2654 . . . . . 6 ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
105 isoeq5 6525 . . . . . 6 (({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) → (𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
106104, 105ax-mp 5 . . . . 5 (𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
107103, 106syl6bb 276 . . . 4 (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
108107cbviotav 5816 . . 3 (℩𝑔𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
109 eqid 2621 . . 3 {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
11061, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109fourierdlem51 39681 . 2 (𝜑𝑋 ∈ ran (℩𝑔𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
111 fourierdlem113.per . 2 ((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
112 ax-resscn 9937 . . . 4 ℝ ⊆ ℂ
113112a1i 11 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℂ)
114 ioossre 12177 . . . . . . 7 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
115114a1i 11 . . . . . 6 (𝜑 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
1161, 115fssresd 6028 . . . . 5 (𝜑 → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
117112a1i 11 . . . . 5 (𝜑 → ℝ ⊆ ℂ)
118116, 117fssd 6014 . . . 4 (𝜑 → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
119118adantr 481 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
120114a1i 11 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
1211, 117fssd 6014 . . . . . . 7 (𝜑𝐹:ℝ⟶ℂ)
122121adantr 481 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
123 ssid 3603 . . . . . . 7 ℝ ⊆ ℝ
124123a1i 11 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℝ)
125 eqid 2621 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
126125tgioo2 22514 . . . . . . 7 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
127125, 126dvres 23581 . . . . . 6 (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))))
128113, 122, 124, 120, 127syl22anc 1324 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))))
129128dmeqd 5286 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))))
130 ioontr 39147 . . . . . . 7 ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))
131130reseq2i 5353 . . . . . 6 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
132131dmeqi 5285 . . . . 5 dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
133132a1i 11 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
134 fourierdlem113.dvcn . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
135 cncff 22604 . . . . 5 (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
136 fdm 6008 . . . . 5 (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
137134, 135, 1363syl 18 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → dom ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
138129, 133, 1373eqtrd 2659 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
139 dvcn 23590 . . 3 (((ℝ ⊆ ℂ ∧ (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ) ∧ dom (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
140113, 119, 120, 138, 139syl31anc 1326 . 2 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
141120, 113sstrd 3593 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
14277adantr 481 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
143 fzofzp1 12506 . . . . . . 7 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
144143adantl 482 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
145142, 144ffvelrnd 6316 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
146145rexrd 10033 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
147 elfzofz 12426 . . . . . 6 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
148147adantl 482 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
149142, 148ffvelrnd 6316 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
15074simprrd 796 . . . . 5 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
151150r19.21bi 2927 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
152125, 146, 149, 151lptioo1cn 39282 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ((limPt‘(TopOpen‘ℂfld))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
153116adantr 481 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
154123a1i 11 . . . . . . . 8 (𝜑 → ℝ ⊆ ℝ)
155117, 121, 154dvbss 23571 . . . . . . 7 (𝜑 → dom (ℝ D 𝐹) ⊆ ℝ)
156 dvfre 23620 . . . . . . . 8 ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
1571, 154, 156syl2anc 692 . . . . . . 7 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
158 0re 9984 . . . . . . . . . 10 0 ∈ ℝ
15960, 158, 59lttri 10107 . . . . . . . . 9 ((-π < 0 ∧ 0 < π) → -π < π)
16063, 65, 159mp2an 707 . . . . . . . 8 -π < π
161160a1i 11 . . . . . . 7 (𝜑 → -π < π)
16284simplld 790 . . . . . . 7 (𝜑 → (𝑄‘0) = -π)
163134, 135syl 17 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
164 fourierdlem113.dvlb . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)) ≠ ∅)
165163, 141, 152, 164, 125ellimciota 39250 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖))) ∈ (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
166149rexrd 10033 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
167125, 166, 145, 151lptioo2cn 39281 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((limPt‘(TopOpen‘ℂfld))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
168 fourierdlem113.dvub . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) ≠ ∅)
169163, 141, 167, 168, 125ellimciota 39250 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1)))) ∈ (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
170121adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
171 zre 11325 . . . . . . . . . . . 12 (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
172171adantl 482 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
173 2re 11034 . . . . . . . . . . . . . . 15 2 ∈ ℝ
174173, 59remulcli 9998 . . . . . . . . . . . . . 14 (2 · π) ∈ ℝ
175174a1i 11 . . . . . . . . . . . . 13 (𝜑 → (2 · π) ∈ ℝ)
17669, 175syl5eqel 2702 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ)
177176adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
178172, 177remulcld 10014 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
179170adantr 481 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
180177adantr 481 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℝ)
181 simplr 791 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑘 ∈ ℤ)
182 simpr 477 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
183111ad4ant14 1290 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
184179, 180, 181, 182, 183fperiodmul 38982 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹𝑡))
185 eqid 2621 . . . . . . . . . 10 (ℝ D 𝐹) = (ℝ D 𝐹)
186170, 178, 184, 185fperdvper 39439 . . . . . . . . 9 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ dom (ℝ D 𝐹)) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡)))
187186an32s 845 . . . . . . . 8 (((𝜑𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡)))
188187simpld 475 . . . . . . 7 (((𝜑𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹))
189187simprd 479 . . . . . . 7 (((𝜑𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡))
190 fveq2 6148 . . . . . . . . 9 (𝑗 = 𝑖 → (𝑄𝑗) = (𝑄𝑖))
191 oveq1 6611 . . . . . . . . . 10 (𝑗 = 𝑖 → (𝑗 + 1) = (𝑖 + 1))
192191fveq2d 6152 . . . . . . . . 9 (𝑗 = 𝑖 → (𝑄‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)))
193190, 192oveq12d 6622 . . . . . . . 8 (𝑗 = 𝑖 → ((𝑄𝑗)(,)(𝑄‘(𝑗 + 1))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
194193cbvmptv 4710 . . . . . . 7 (𝑗 ∈ (0..^𝑀) ↦ ((𝑄𝑗)(,)(𝑄‘(𝑗 + 1)))) = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
195 eqid 2621 . . . . . . 7 (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇))) = (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇)))
196155, 157, 61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195fourierdlem71 39701 . . . . . 6 (𝜑 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
197196adantr 481 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
198 nfv 1840 . . . . . . . . 9 𝑡(𝜑𝑖 ∈ (0..^𝑀))
199 nfra1 2936 . . . . . . . . 9 𝑡𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧
200198, 199nfan 1825 . . . . . . . 8 𝑡((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
201128, 131syl6eq 2671 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
202201fveq1d 6150 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡))
203 fvres 6164 . . . . . . . . . . . . 13 (𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
204202, 203sylan9eq 2675 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
205204fveq2d 6152 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡)))
206205adantlr 750 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡)))
207 simplr 791 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
208 ssdmres 5379 . . . . . . . . . . . . . 14 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
209137, 208sylibr 224 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹))
210209ad2antrr 761 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹))
211 simpr 477 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
212210, 211sseldd 3584 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ dom (ℝ D 𝐹))
213 rspa 2925 . . . . . . . . . . 11 ((∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧𝑡 ∈ dom (ℝ D 𝐹)) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
214207, 212, 213syl2anc 692 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
215206, 214eqbrtrd 4635 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
216215ex 450 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) → (𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
217200, 216ralrimi 2951 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) → ∀𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
218217ex 450 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 → ∀𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
219218reximdv 3010 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
220197, 219mpd 15 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
221149, 145, 153, 138, 220ioodvbdlimc1 39454 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)) ≠ ∅)
222119, 141, 152, 221, 125ellimciota 39250 . 2 ((𝜑𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
223149, 145, 153, 138, 220ioodvbdlimc2 39456 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) ≠ ∅)
224119, 141, 167, 223, 125ellimciota 39250 . 2 ((𝜑𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1)))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
225 frel 6007 . . . . . . 7 ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ → Rel (ℝ D 𝐹))
226157, 225syl 17 . . . . . 6 (𝜑 → Rel (ℝ D 𝐹))
227 resindm 5403 . . . . . 6 (Rel (ℝ D 𝐹) → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
228226, 227syl 17 . . . . 5 (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
229 inss2 3812 . . . . . . 7 ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
230229a1i 11 . . . . . 6 (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
231157, 230fssresd 6028 . . . . 5 (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
232228, 231feq1dd 38820 . . . 4 (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
233232, 117fssd 6014 . . 3 (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℂ)
234 ioosscn 39127 . . . . 5 (-∞(,)𝑋) ⊆ ℂ
235 ssinss1 3819 . . . . 5 ((-∞(,)𝑋) ⊆ ℂ → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
236234, 235ax-mp 5 . . . 4 ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ
237236a1i 11 . . 3 (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
238 3simpb 1057 . . . . . . . 8 ((𝜑𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → (𝜑𝑘 ∈ ℤ))
239 simp2 1060 . . . . . . . 8 ((𝜑𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ dom (ℝ D 𝐹))
240170adantr 481 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
241177adantr 481 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
242 simplr 791 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℤ)
243 simpr 477 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
244 eleq1 2686 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 ∈ ℝ ↔ 𝑦 ∈ ℝ))
245244anbi2d 739 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝜑𝑥 ∈ ℝ) ↔ (𝜑𝑦 ∈ ℝ)))
246 oveq1 6611 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
247246fveq2d 6152 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
248 fveq2 6148 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
249247, 248eqeq12d 2636 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)))
250245, 249imbi12d 334 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))))
251250, 111chvarv 2262 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
252251ad4ant14 1290 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
253240, 241, 242, 243, 252fperiodmul 38982 . . . . . . . . 9 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
254170, 178, 253, 185fperdvper 39439 . . . . . . . 8 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥)))
255238, 239, 254syl2anc 692 . . . . . . 7 ((𝜑𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥)))
256255simpld 475 . . . . . 6 ((𝜑𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹))
257 oveq2 6612 . . . . . . . . . 10 (𝑤 = 𝑥 → (π − 𝑤) = (π − 𝑥))
258257oveq1d 6619 . . . . . . . . 9 (𝑤 = 𝑥 → ((π − 𝑤) / 𝑇) = ((π − 𝑥) / 𝑇))
259258fveq2d 6152 . . . . . . . 8 (𝑤 = 𝑥 → (⌊‘((π − 𝑤) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
260259oveq1d 6619 . . . . . . 7 (𝑤 = 𝑥 → ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
261260cbvmptv 4710 . . . . . 6 (𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
262 eqid 2621 . . . . . 6 (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥)))
26361, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209fourierdlem41 39672 . . . . 5 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))))
264263simpld 475 . . . 4 (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)))
265125cnfldtop 22497 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ Top
266265a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (TopOpen‘ℂfld) ∈ Top)
267236a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
268 mnfxr 10040 . . . . . . . . . . . 12 -∞ ∈ ℝ*
269268a1i 11 . . . . . . . . . . 11 (𝑦 ∈ ℝ → -∞ ∈ ℝ*)
270 rexr 10029 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → 𝑦 ∈ ℝ*)
271 mnflt 11901 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → -∞ < 𝑦)
272269, 270, 271xrltled 38950 . . . . . . . . . . 11 (𝑦 ∈ ℝ → -∞ ≤ 𝑦)
273 iooss1 12152 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ -∞ ≤ 𝑦) → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
274269, 272, 273syl2anc 692 . . . . . . . . . 10 (𝑦 ∈ ℝ → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
2752743ad2ant2 1081 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
276 simp3 1061 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))
277275, 276ssind 3815 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)))
278 unicntop 38690 . . . . . . . . 9 ℂ = (TopOpen‘ℂfld)
279278lpss3 20858 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ Top ∧ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ ∧ (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂfld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
280266, 267, 277, 279syl3anc 1323 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → ((limPt‘(TopOpen‘ℂfld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
2812803adant3l 1319 . . . . . 6 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂfld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
2822703ad2ant2 1081 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑦 ∈ ℝ*)
283583ad2ant1 1080 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ℝ)
284 simp3l 1087 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑦 < 𝑋)
285125, 282, 283, 284lptioo2cn 39281 . . . . . 6 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝑦(,)𝑋)))
286281, 285sseldd 3584 . . . . 5 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
287286rexlimdv3a 3026 . . . 4 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)))))
288264, 287mpd 15 . . 3 (𝜑𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
289255simprd 479 . . . 4 ((𝜑𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥))
290 oveq2 6612 . . . . . . . 8 (𝑦 = 𝑥 → (π − 𝑦) = (π − 𝑥))
291290oveq1d 6619 . . . . . . 7 (𝑦 = 𝑥 → ((π − 𝑦) / 𝑇) = ((π − 𝑥) / 𝑇))
292291fveq2d 6152 . . . . . 6 (𝑦 = 𝑥 → (⌊‘((π − 𝑦) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
293292oveq1d 6619 . . . . 5 (𝑦 = 𝑥 → ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
294293cbvmptv 4710 . . . 4 (𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
295 id 22 . . . . . 6 (𝑧 = 𝑥𝑧 = 𝑥)
296 fveq2 6148 . . . . . 6 (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧) = ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥))
297295, 296oveq12d 6622 . . . . 5 (𝑧 = 𝑥 → (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧)) = (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
298297cbvmptv 4710 . . . 4 (𝑧 ∈ ℝ ↦ (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
29961, 62, 161, 23, 71, 24, 25, 155, 157, 256, 289, 134, 169, 58, 294, 298fourierdlem49 39679 . . 3 (𝜑 → (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim 𝑋) ≠ ∅)
300233, 237, 288, 299, 125ellimciota 39250 . 2 (𝜑 → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim 𝑋)) ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim 𝑋))
301 resindm 5403 . . . . . 6 (Rel (ℝ D 𝐹) → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
302226, 301syl 17 . . . . 5 (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
303 inss2 3812 . . . . . . 7 ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
304303a1i 11 . . . . . 6 (𝜑 → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
305157, 304fssresd 6028 . . . . 5 (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
306302, 305feq1dd 38820 . . . 4 (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
307306, 117fssd 6014 . . 3 (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℂ)
308 ioosscn 39127 . . . . 5 (𝑋(,)+∞) ⊆ ℂ
309 ssinss1 3819 . . . . 5 ((𝑋(,)+∞) ⊆ ℂ → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
310308, 309ax-mp 5 . . . 4 ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ
311310a1i 11 . . 3 (𝜑 → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
312263simprd 479 . . . 4 (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)))
313265a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (TopOpen‘ℂfld) ∈ Top)
314310a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
315 pnfxr 10036 . . . . . . . . . . . 12 +∞ ∈ ℝ*
316315a1i 11 . . . . . . . . . . 11 (𝑦 ∈ ℝ → +∞ ∈ ℝ*)
317 ltpnf 11898 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → 𝑦 < +∞)
318270, 316, 317xrltled 38950 . . . . . . . . . . 11 (𝑦 ∈ ℝ → 𝑦 ≤ +∞)
319 iooss2 12153 . . . . . . . . . . 11 ((+∞ ∈ ℝ*𝑦 ≤ +∞) → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
320316, 318, 319syl2anc 692 . . . . . . . . . 10 (𝑦 ∈ ℝ → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
3213203ad2ant2 1081 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
322 simp3 1061 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))
323321, 322ssind 3815 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)))
324278lpss3 20858 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ Top ∧ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ ∧ (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂfld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
325313, 314, 323, 324syl3anc 1323 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → ((limPt‘(TopOpen‘ℂfld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
3263253adant3l 1319 . . . . . 6 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂfld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
3272703ad2ant2 1081 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑦 ∈ ℝ*)
328583ad2ant1 1080 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ℝ)
329 simp3l 1087 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 < 𝑦)
330125, 327, 328, 329lptioo1cn 39282 . . . . . 6 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝑋(,)𝑦)))
331326, 330sseldd 3584 . . . . 5 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
332331rexlimdv3a 3026 . . . 4 (𝜑 → (∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)))))
333312, 332mpd 15 . . 3 (𝜑𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
334 biid 251 . . . 4 (((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑤 ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ ℤ) ∧ 𝑤 = (𝑋 + (𝑘 · 𝑇))) ↔ ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑤 ∈ ((𝑄𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ ℤ) ∧ 𝑤 = (𝑋 + (𝑘 · 𝑇))))
33561, 62, 161, 23, 71, 24, 25, 157, 256, 289, 134, 165, 58, 294, 298, 334fourierdlem48 39678 . . 3 (𝜑 → (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim 𝑋) ≠ ∅)
336307, 311, 333, 335, 125ellimciota 39250 . 2 (𝜑 → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim 𝑋)) ∈ (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim 𝑋))
337 fourierdlem113.l . 2 (𝜑𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
338 fourierdlem113.r . 2 (𝜑𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim 𝑋))
339 fourierdlem113.a . 2 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
340 fourierdlem113.b . 2 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
341 fveq2 6148 . . . . . . . 8 (𝑛 = 𝑘 → (𝐴𝑛) = (𝐴𝑘))
342 oveq1 6611 . . . . . . . . 9 (𝑛 = 𝑘 → (𝑛 · 𝑋) = (𝑘 · 𝑋))
343342fveq2d 6152 . . . . . . . 8 (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑋)) = (cos‘(𝑘 · 𝑋)))
344341, 343oveq12d 6622 . . . . . . 7 (𝑛 = 𝑘 → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) = ((𝐴𝑘) · (cos‘(𝑘 · 𝑋))))
345 fveq2 6148 . . . . . . . 8 (𝑛 = 𝑘 → (𝐵𝑛) = (𝐵𝑘))
346342fveq2d 6152 . . . . . . . 8 (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑋)) = (sin‘(𝑘 · 𝑋)))
347345, 346oveq12d 6622 . . . . . . 7 (𝑛 = 𝑘 → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) = ((𝐵𝑘) · (sin‘(𝑘 · 𝑋))))
348344, 347oveq12d 6622 . . . . . 6 (𝑛 = 𝑘 → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = (((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋)))))
349348cbvsumv 14360 . . . . 5 Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑘 ∈ (1...𝑚)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋))))
350 oveq2 6612 . . . . . . 7 (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
351350eqcomd 2627 . . . . . 6 (𝑗 = 𝑚 → (1...𝑚) = (1...𝑗))
352351sumeq1d 14365 . . . . 5 (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑚)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑘 ∈ (1...𝑗)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋)))))
353349, 352syl5req 2668 . . . 4 (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑗)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))))
354353oveq2d 6620 . . 3 (𝑗 = 𝑚 → (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
355354cbvmptv 4710 . 2 (𝑗 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋)))))) = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
356 fourierdlem113.15 . 2 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))))
357 fdm 6008 . . . . . 6 (𝐹:ℝ⟶ℝ → dom 𝐹 = ℝ)
3581, 357syl 17 . . . . 5 (𝜑 → dom 𝐹 = ℝ)
359358, 154eqsstrd 3618 . . . 4 (𝜑 → dom 𝐹 ⊆ ℝ)
360358feq2d 5988 . . . . 5 (𝜑 → (𝐹:dom 𝐹⟶ℝ ↔ 𝐹:ℝ⟶ℝ))
3611, 360mpbird 247 . . . 4 (𝜑𝐹:dom 𝐹⟶ℝ)
362359sselda 3583 . . . . . . 7 ((𝜑𝑡 ∈ dom 𝐹) → 𝑡 ∈ ℝ)
363362adantr 481 . . . . . 6 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑡 ∈ ℝ)
364171adantl 482 . . . . . . 7 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
365177adantlr 750 . . . . . . 7 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
366364, 365remulcld 10014 . . . . . 6 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
367363, 366readdcld 10013 . . . . 5 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ ℝ)
368358eqcomd 2627 . . . . . 6 (𝜑 → ℝ = dom 𝐹)
369368ad2antrr 761 . . . . 5 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → ℝ = dom 𝐹)
370367, 369eleqtrd 2700 . . . 4 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ dom 𝐹)
371 id 22 . . . . . 6 ((𝜑𝑘 ∈ ℤ) → (𝜑𝑘 ∈ ℤ))
372371adantlr 750 . . . . 5 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝜑𝑘 ∈ ℤ))
373372, 363, 184syl2anc 692 . . . 4 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹𝑡))
374359, 361, 61, 62, 161, 71, 24, 77, 162, 85, 140, 222, 224, 370, 373, 194, 195fourierdlem71 39701 . . 3 (𝜑 → ∃𝑢 ∈ ℝ ∀𝑡 ∈ dom 𝐹(abs‘(𝐹𝑡)) ≤ 𝑢)
375358raleqdv 3133 . . . 4 (𝜑 → (∀𝑡 ∈ dom 𝐹(abs‘(𝐹𝑡)) ≤ 𝑢 ↔ ∀𝑡 ∈ ℝ (abs‘(𝐹𝑡)) ≤ 𝑢))
376375rexbidv 3045 . . 3 (𝜑 → (∃𝑢 ∈ ℝ ∀𝑡 ∈ dom 𝐹(abs‘(𝐹𝑡)) ≤ 𝑢 ↔ ∃𝑢 ∈ ℝ ∀𝑡 ∈ ℝ (abs‘(𝐹𝑡)) ≤ 𝑢))
377374, 376mpbid 222 . 2 (𝜑 → ∃𝑢 ∈ ℝ ∀𝑡 ∈ ℝ (abs‘(𝐹𝑡)) ≤ 𝑢)
3781, 22, 23, 24, 25, 32, 57, 58, 110, 69, 111, 140, 222, 224, 134, 300, 336, 337, 338, 339, 340, 355, 356, 377, 196, 58fourierdlem112 39742 1 (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  cun 3553  cin 3554  wss 3555  c0 3891  ifcif 4058  {cpr 4150   class class class wbr 4613  cmpt 4673  dom cdm 5074  ran crn 5075  cres 5076  Rel wrel 5079  cio 5808  Fun wfun 5841  wf 5843  cfv 5847   Isom wiso 5848  (class class class)co 6604  𝑚 cmap 7802  Fincfn 7899  cc 9878  cr 9879  0cc0 9880  1c1 9881   + caddc 9883   · cmul 9885  +∞cpnf 10015  -∞cmnf 10016  *cxr 10017   < clt 10018  cle 10019  cmin 10210  -cneg 10211   / cdiv 10628  cn 10964  2c2 11014  0cn0 11236  cz 11321  cuz 11631  (,)cioo 12117  (,]cioc 12118  [,)cico 12119  [,]cicc 12120  ...cfz 12268  ..^cfzo 12406  cfl 12531   mod cmo 12608  seqcseq 12741  #chash 13057  abscabs 13908  cli 14149  Σcsu 14350  sincsin 14719  cosccos 14720  πcpi 14722  TopOpenctopn 16003  topGenctg 16019  fldccnfld 19665  Topctop 20617  intcnt 20731  limPtclp 20848  cnccncf 22587  citg 23293   lim climc 23532   D cdv 23533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cc 9201  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959  ax-mulf 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-disj 4584  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-ofr 6851  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-omul 7510  df-er 7687  df-map 7804  df-pm 7805  df-ixp 7853  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-acn 8712  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-xnn0 11308  df-z 11322  df-dec 11438  df-uz 11632  df-q 11733  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-ioo 12121  df-ioc 12122  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-fl 12533  df-mod 12609  df-seq 12742  df-exp 12801  df-fac 13001  df-bc 13030  df-hash 13058  df-shft 13741  df-cj 13773  df-re 13774  df-im 13775  df-sqrt 13909  df-abs 13910  df-limsup 14136  df-clim 14153  df-rlim 14154  df-sum 14351  df-ef 14723  df-sin 14725  df-cos 14726  df-pi 14728  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-mulr 15876  df-starv 15877  df-sca 15878  df-vsca 15879  df-ip 15880  df-tset 15881  df-ple 15882  df-ds 15885  df-unif 15886  df-hom 15887  df-cco 15888  df-rest 16004  df-topn 16005  df-0g 16023  df-gsum 16024  df-topgen 16025  df-pt 16026  df-prds 16029  df-xrs 16083  df-qtop 16088  df-imas 16089  df-xps 16091  df-mre 16167  df-mrc 16168  df-acs 16170  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-mulg 17462  df-cntz 17671  df-cmn 18116  df-psmet 19657  df-xmet 19658  df-met 19659  df-bl 19660  df-mopn 19661  df-fbas 19662  df-fg 19663  df-cnfld 19666  df-top 20621  df-bases 20622  df-topon 20623  df-topsp 20624  df-cld 20733  df-ntr 20734  df-cls 20735  df-nei 20812  df-lp 20850  df-perf 20851  df-cn 20941  df-cnp 20942  df-t1 21028  df-haus 21029  df-cmp 21100  df-tx 21275  df-hmeo 21468  df-fil 21560  df-fm 21652  df-flim 21653  df-flf 21654  df-xms 22035  df-ms 22036  df-tms 22037  df-cncf 22589  df-ovol 23140  df-vol 23141  df-mbf 23294  df-itg1 23295  df-itg2 23296  df-ibl 23297  df-itg 23298  df-0p 23343  df-ditg 23517  df-limc 23536  df-dv 23537
This theorem is referenced by:  fourierdlem114  39744
  Copyright terms: Public domain W3C validator