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

Theorem fourierdlem113 40754
 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 6697 . . . . . . 7 (𝑤 = 𝑦 → (𝑤 mod (2 · π)) = (𝑦 mod (2 · π)))
32eqeq1d 2653 . . . . . 6 (𝑤 = 𝑦 → ((𝑤 mod (2 · π)) = 0 ↔ (𝑦 mod (2 · π)) = 0))
4 oveq2 6698 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑘 + (1 / 2)) · 𝑤) = ((𝑘 + (1 / 2)) · 𝑦))
54fveq2d 6233 . . . . . . 7 (𝑤 = 𝑦 → (sin‘((𝑘 + (1 / 2)) · 𝑤)) = (sin‘((𝑘 + (1 / 2)) · 𝑦)))
6 oveq1 6697 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑤 / 2) = (𝑦 / 2))
76fveq2d 6233 . . . . . . . 8 (𝑤 = 𝑦 → (sin‘(𝑤 / 2)) = (sin‘(𝑦 / 2)))
87oveq2d 6706 . . . . . . 7 (𝑤 = 𝑦 → ((2 · π) · (sin‘(𝑤 / 2))) = ((2 · π) · (sin‘(𝑦 / 2))))
95, 8oveq12d 6708 . . . . . 6 (𝑤 = 𝑦 → ((sin‘((𝑘 + (1 / 2)) · 𝑤)) / ((2 · π) · (sin‘(𝑤 / 2)))) = ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
103, 9ifbieq2d 4144 . . . . 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 4783 . . . 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 6698 . . . . . . . 8 (𝑘 = 𝑚 → (2 · 𝑘) = (2 · 𝑚))
1312oveq1d 6705 . . . . . . 7 (𝑘 = 𝑚 → ((2 · 𝑘) + 1) = ((2 · 𝑚) + 1))
1413oveq1d 6705 . . . . . 6 (𝑘 = 𝑚 → (((2 · 𝑘) + 1) / (2 · π)) = (((2 · 𝑚) + 1) / (2 · π)))
15 oveq1 6697 . . . . . . . . 9 (𝑘 = 𝑚 → (𝑘 + (1 / 2)) = (𝑚 + (1 / 2)))
1615oveq1d 6705 . . . . . . . 8 (𝑘 = 𝑚 → ((𝑘 + (1 / 2)) · 𝑦) = ((𝑚 + (1 / 2)) · 𝑦))
1716fveq2d 6233 . . . . . . 7 (𝑘 = 𝑚 → (sin‘((𝑘 + (1 / 2)) · 𝑦)) = (sin‘((𝑚 + (1 / 2)) · 𝑦)))
1817oveq1d 6705 . . . . . 6 (𝑘 = 𝑚 → ((sin‘((𝑘 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))) = ((sin‘((𝑚 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))
1914, 18ifeq12d 4139 . . . . 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 4778 . . . 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 2697 . . 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 4783 . 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 6697 . . . . . . . 8 (𝑤 = 𝑦 → (𝑤 + (𝑗 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
2726eleq1d 2715 . . . . . . 7 (𝑤 = 𝑦 → ((𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
2827rexbidv 3081 . . . . . 6 (𝑤 = 𝑦 → (∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
2928cbvrabv 3230 . . . . 5 {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
3029uneq2i 3797 . . . 4 ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
3130fveq2i 6232 . . 3 (#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) = (#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
3231oveq1i 6700 . 2 ((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1) = ((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
33 oveq1 6697 . . . . . . . . . . . 12 (𝑘 = 𝑗 → (𝑘 · 𝑇) = (𝑗 · 𝑇))
3433oveq2d 6706 . . . . . . . . . . 11 (𝑘 = 𝑗 → (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑗 · 𝑇)))
3534eleq1d 2715 . . . . . . . . . 10 (𝑘 = 𝑗 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
3635cbvrexv 3202 . . . . . . . . 9 (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄)
3736a1i 11 . . . . . . . 8 (𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄))
3837rabbiia 3215 . . . . . . 7 {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄}
3938uneq2i 3797 . . . . . 6 ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})
40 isoeq5 6611 . . . . . 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 6706 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (𝑤 + (𝑘 · 𝑇)) = (𝑤 + (𝑗 · 𝑇)))
4443eleq1d 2715 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → ((𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
4544cbvrexv 3202 . . . . . . . . . . . 12 (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄)
4645a1i 11 . . . . . . . . . . 11 (𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) → (∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄))
4746rabbiia 3215 . . . . . . . . . 10 {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}
4847uneq2i 3797 . . . . . . . . 9 ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})
4948fveq2i 6232 . . . . . . . 8 (#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄}))
5049oveq1i 6700 . . . . . . 7 ((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)
5150oveq2i 6701 . . . . . 6 (0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)) = (0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1))
52 isoeq4 6610 . . . . . 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 6607 . . . 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 5895 . 2 (℩𝑔𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑤 + (𝑗 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑗 ∈ ℤ (𝑦 + (𝑗 · 𝑇)) ∈ ran 𝑄})))
58 fourierdlem113.x . 2 (𝜑𝑋 ∈ ℝ)
59 pire 24255 . . . . 5 π ∈ ℝ
6059renegcli 10380 . . . 4 -π ∈ ℝ
6160a1i 11 . . 3 (𝜑 → -π ∈ ℝ)
6259a1i 11 . . 3 (𝜑 → π ∈ ℝ)
63 negpilt0 39806 . . . 4 -π < 0
6463a1i 11 . . 3 (𝜑 → -π < 0)
65 pipos 24257 . . . 4 0 < π
6665a1i 11 . . 3 (𝜑 → 0 < π)
67 picn 24256 . . . . 5 π ∈ ℂ
68672timesi 11185 . . . 4 (2 · π) = (π + π)
69 fourierdlem113.t . . . 4 𝑇 = (2 · π)
7067, 67subnegi 10398 . . . 4 (π − -π) = (π + π)
7168, 69, 703eqtr4i 2683 . . 3 𝑇 = (π − -π)
7223fourierdlem2 40644 . . . . . . . 8 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
7324, 72syl 17 . . . . . . 7 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
7425, 73mpbid 222 . . . . . 6 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
7574simpld 474 . . . . 5 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
76 elmapi 7921 . . . . 5 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
7775, 76syl 17 . . . 4 (𝜑𝑄:(0...𝑀)⟶ℝ)
78 fzfid 12812 . . . 4 (𝜑 → (0...𝑀) ∈ Fin)
79 rnffi 39670 . . . 4 ((𝑄:(0...𝑀)⟶ℝ ∧ (0...𝑀) ∈ Fin) → ran 𝑄 ∈ Fin)
8077, 78, 79syl2anc 694 . . 3 (𝜑 → ran 𝑄 ∈ Fin)
8123, 24, 25fourierdlem15 40657 . . . 4 (𝜑𝑄:(0...𝑀)⟶(-π[,]π))
82 frn 6091 . . . 4 (𝑄:(0...𝑀)⟶(-π[,]π) → ran 𝑄 ⊆ (-π[,]π))
8381, 82syl 17 . . 3 (𝜑 → ran 𝑄 ⊆ (-π[,]π))
8474simprd 478 . . . . 5 (𝜑 → (((𝑄‘0) = -π ∧ (𝑄𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))
8584simplrd 808 . . . 4 (𝜑 → (𝑄𝑀) = π)
86 ffun 6086 . . . . . 6 (𝑄:(0...𝑀)⟶(-π[,]π) → Fun 𝑄)
8781, 86syl 17 . . . . 5 (𝜑 → Fun 𝑄)
8824nnnn0d 11389 . . . . . . . 8 (𝜑𝑀 ∈ ℕ0)
89 nn0uz 11760 . . . . . . . 8 0 = (ℤ‘0)
9088, 89syl6eleq 2740 . . . . . . 7 (𝜑𝑀 ∈ (ℤ‘0))
91 eluzfz2 12387 . . . . . . 7 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
9290, 91syl 17 . . . . . 6 (𝜑𝑀 ∈ (0...𝑀))
93 fdm 6089 . . . . . . . 8 (𝑄:(0...𝑀)⟶(-π[,]π) → dom 𝑄 = (0...𝑀))
9481, 93syl 17 . . . . . . 7 (𝜑 → dom 𝑄 = (0...𝑀))
9594eqcomd 2657 . . . . . 6 (𝜑 → (0...𝑀) = dom 𝑄)
9692, 95eleqtrd 2732 . . . . 5 (𝜑𝑀 ∈ dom 𝑄)
97 fvelrn 6392 . . . . 5 ((Fun 𝑄𝑀 ∈ dom 𝑄) → (𝑄𝑀) ∈ ran 𝑄)
9887, 96, 97syl2anc 694 . . . 4 (𝜑 → (𝑄𝑀) ∈ ran 𝑄)
9985, 98eqeltrrd 2731 . . 3 (𝜑 → π ∈ ran 𝑄)
100 fourierdlem113.e . . 3 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
101 fourierdlem113.exq . . 3 (𝜑 → (𝐸𝑋) ∈ ran 𝑄)
102 eqid 2651 . . 3 ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
103 isoeq1 6607 . . . . 5 (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
10430, 48, 393eqtr4ri 2684 . . . . . 6 ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})
105 isoeq5 6611 . . . . . 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 5895 . . 3 (℩𝑔𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
109 eqid 2651 . . 3 {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑤 ∈ ((-π + 𝑋)(,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄}
11061, 62, 64, 66, 71, 80, 83, 99, 100, 58, 101, 102, 108, 109fourierdlem51 40692 . 2 (𝜑𝑋 ∈ ran (℩𝑔𝑔 Isom < , < ((0...((#‘({(-π + 𝑋), (π + 𝑋)} ∪ {𝑤 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑤 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)), ({(-π + 𝑋), (π + 𝑋)} ∪ {𝑦 ∈ ((-π + 𝑋)[,](π + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
111 fourierdlem113.per . 2 ((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
112 ax-resscn 10031 . . . 4 ℝ ⊆ ℂ
113112a1i 11 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℂ)
114 ioossre 12273 . . . . . . 7 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
115114a1i 11 . . . . . 6 (𝜑 → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
1161, 115fssresd 6109 . . . . 5 (𝜑 → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
117112a1i 11 . . . . 5 (𝜑 → ℝ ⊆ ℂ)
118116, 117fssd 6095 . . . 4 (𝜑 → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
119118adantr 480 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
120114a1i 11 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
1211, 117fssd 6095 . . . . . . 7 (𝜑𝐹:ℝ⟶ℂ)
122121adantr 480 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
123 ssid 3657 . . . . . . 7 ℝ ⊆ ℝ
124123a1i 11 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ℝ ⊆ ℝ)
125 eqid 2651 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
126125tgioo2 22653 . . . . . . 7 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
127125, 126dvres 23720 . . . . . 6 (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))))
128113, 122, 124, 120, 127syl22anc 1367 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))))
129128dmeqd 5358 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = dom ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))))
130 ioontr 40054 . . . . . . 7 ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))
131130reseq2i 5425 . . . . . 6 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
132131dmeqi 5357 . . . . 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 22743 . . . . 5 (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) → ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
136 fdm 6089 . . . . 5 (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ → dom ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
137134, 135, 1363syl 18 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → dom ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
138129, 133, 1373eqtrd 2689 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → dom (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
139 dvcn 23729 . . 3 (((ℝ ⊆ ℂ ∧ (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ) ∧ dom (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
140113, 119, 120, 138, 139syl31anc 1369 . 2 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
141120, 113sstrd 3646 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
14277adantr 480 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
143 fzofzp1 12605 . . . . . . 7 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
144143adantl 481 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
145142, 144ffvelrnd 6400 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
146145rexrd 10127 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
147 elfzofz 12524 . . . . . 6 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
148147adantl 481 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
149142, 148ffvelrnd 6400 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
15074simprrd 812 . . . . 5 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
151150r19.21bi 2961 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
152125, 146, 149, 151lptioo1cn 40196 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ((limPt‘(TopOpen‘ℂfld))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
153116adantr 480 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℝ)
154123a1i 11 . . . . . . . 8 (𝜑 → ℝ ⊆ ℝ)
155117, 121, 154dvbss 23710 . . . . . . 7 (𝜑 → dom (ℝ D 𝐹) ⊆ ℝ)
156 dvfre 23759 . . . . . . . 8 ((𝐹:ℝ⟶ℝ ∧ ℝ ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
1571, 154, 156syl2anc 694 . . . . . . 7 (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ)
158 0re 10078 . . . . . . . . . 10 0 ∈ ℝ
15960, 158, 59lttri 10201 . . . . . . . . 9 ((-π < 0 ∧ 0 < π) → -π < π)
16063, 65, 159mp2an 708 . . . . . . . 8 -π < π
161160a1i 11 . . . . . . 7 (𝜑 → -π < π)
16284simplld 806 . . . . . . 7 (𝜑 → (𝑄‘0) = -π)
163134, 135syl 17 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
164 fourierdlem113.dvlb . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)) ≠ ∅)
165163, 141, 152, 164, 125ellimciota 40164 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖))) ∈ (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
166149rexrd 10127 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
167125, 166, 145, 151lptioo2cn 40195 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((limPt‘(TopOpen‘ℂfld))‘((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
168 fourierdlem113.dvub . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) ≠ ∅)
169163, 141, 167, 168, 125ellimciota 40164 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1)))) ∈ (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
170121adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℤ) → 𝐹:ℝ⟶ℂ)
171 zre 11419 . . . . . . . . . . . 12 (𝑘 ∈ ℤ → 𝑘 ∈ ℝ)
172171adantl 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
173 2re 11128 . . . . . . . . . . . . . . 15 2 ∈ ℝ
174173, 59remulcli 10092 . . . . . . . . . . . . . 14 (2 · π) ∈ ℝ
175174a1i 11 . . . . . . . . . . . . 13 (𝜑 → (2 · π) ∈ ℝ)
17669, 175syl5eqel 2734 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ)
177176adantr 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
178172, 177remulcld 10108 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
179170adantr 480 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
180177adantr 480 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑇 ∈ ℝ)
181 simplr 807 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑘 ∈ ℤ)
182 simpr 476 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
183111ad4ant14 1317 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
184179, 180, 181, 182, 183fperiodmul 39832 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ ℝ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹𝑡))
185 eqid 2651 . . . . . . . . . 10 (ℝ D 𝐹) = (ℝ D 𝐹)
186170, 178, 184, 185fperdvper 40451 . . . . . . . . 9 (((𝜑𝑘 ∈ ℤ) ∧ 𝑡 ∈ dom (ℝ D 𝐹)) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡)))
187186an32s 863 . . . . . . . 8 (((𝜑𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → ((𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡)))
188187simpld 474 . . . . . . 7 (((𝜑𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹))
189187simprd 478 . . . . . . 7 (((𝜑𝑡 ∈ dom (ℝ D 𝐹)) ∧ 𝑘 ∈ ℤ) → ((ℝ D 𝐹)‘(𝑡 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑡))
190 fveq2 6229 . . . . . . . . 9 (𝑗 = 𝑖 → (𝑄𝑗) = (𝑄𝑖))
191 oveq1 6697 . . . . . . . . . 10 (𝑗 = 𝑖 → (𝑗 + 1) = (𝑖 + 1))
192191fveq2d 6233 . . . . . . . . 9 (𝑗 = 𝑖 → (𝑄‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)))
193190, 192oveq12d 6708 . . . . . . . 8 (𝑗 = 𝑖 → ((𝑄𝑗)(,)(𝑄‘(𝑗 + 1))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
194193cbvmptv 4783 . . . . . . 7 (𝑗 ∈ (0..^𝑀) ↦ ((𝑄𝑗)(,)(𝑄‘(𝑗 + 1)))) = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
195 eqid 2651 . . . . . . 7 (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇))) = (𝑡 ∈ ℝ ↦ (𝑡 + ((⌊‘((π − 𝑡) / 𝑇)) · 𝑇)))
196155, 157, 61, 62, 161, 71, 24, 77, 162, 85, 134, 165, 169, 188, 189, 194, 195fourierdlem71 40712 . . . . . 6 (𝜑 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
197196adantr 480 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
198 nfv 1883 . . . . . . . . 9 𝑡(𝜑𝑖 ∈ (0..^𝑀))
199 nfra1 2970 . . . . . . . . 9 𝑡𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧
200198, 199nfan 1868 . . . . . . . 8 𝑡((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
201128, 131syl6eq 2701 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))) = ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
202201fveq1d 6231 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡))
203 fvres 6245 . . . . . . . . . . . . 13 (𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
204202, 203sylan9eq 2705 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
205204fveq2d 6233 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡)))
206205adantlr 751 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) = (abs‘((ℝ D 𝐹)‘𝑡)))
207 simplr 807 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
208 ssdmres 5455 . . . . . . . . . . . . . 14 (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
209137, 208sylibr 224 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹))
210209ad2antrr 762 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom (ℝ D 𝐹))
211 simpr 476 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
212210, 211sseldd 3637 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑡 ∈ dom (ℝ D 𝐹))
213 rspa 2959 . . . . . . . . . . 11 ((∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧𝑡 ∈ dom (ℝ D 𝐹)) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
214207, 212, 213syl2anc 694 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧)
215206, 214eqbrtrd 4707 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) ∧ 𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
216215ex 449 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) → (𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
217200, 216ralrimi 2986 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧) → ∀𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
218217ex 449 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 → ∀𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
219218reximdv 3045 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (∃𝑧 ∈ ℝ ∀𝑡 ∈ dom (ℝ D 𝐹)(abs‘((ℝ D 𝐹)‘𝑡)) ≤ 𝑧 → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧))
220197, 219mpd 15 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → ∃𝑧 ∈ ℝ ∀𝑡 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))(abs‘((ℝ D (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))‘𝑡)) ≤ 𝑧)
221149, 145, 153, 138, 220ioodvbdlimc1 40466 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)) ≠ ∅)
222119, 141, 152, 221, 125ellimciota 40164 . 2 ((𝜑𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
223149, 145, 153, 138, 220ioodvbdlimc2 40468 . . 3 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) ≠ ∅)
224119, 141, 167, 223, 125ellimciota 40164 . 2 ((𝜑𝑖 ∈ (0..^𝑀)) → (℩𝑦𝑦 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1)))) ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
225 frel 6088 . . . . . . 7 ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ → Rel (ℝ D 𝐹))
226157, 225syl 17 . . . . . 6 (𝜑 → Rel (ℝ D 𝐹))
227 resindm 5479 . . . . . 6 (Rel (ℝ D 𝐹) → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
228226, 227syl 17 . . . . 5 (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (-∞(,)𝑋)))
229 inss2 3867 . . . . . . 7 ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
230229a1i 11 . . . . . 6 (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
231157, 230fssresd 6109 . . . . 5 (𝜑 → ((ℝ D 𝐹) ↾ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
232228, 231feq1dd 39661 . . . 4 (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℝ)
233232, 117fssd 6095 . . 3 (𝜑 → ((ℝ D 𝐹) ↾ (-∞(,)𝑋)):((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))⟶ℂ)
234 ioosscn 40034 . . . . 5 (-∞(,)𝑋) ⊆ ℂ
235 ssinss1 3874 . . . . 5 ((-∞(,)𝑋) ⊆ ℂ → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
236234, 235ax-mp 5 . . . 4 ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ
237236a1i 11 . . 3 (𝜑 → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
238 3simpb 1079 . . . . . . . 8 ((𝜑𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → (𝜑𝑘 ∈ ℤ))
239 simp2 1082 . . . . . . . 8 ((𝜑𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑥 ∈ dom (ℝ D 𝐹))
240170adantr 480 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
241177adantr 480 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
242 simplr 807 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℤ)
243 simpr 476 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
244 eleq1 2718 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 ∈ ℝ ↔ 𝑦 ∈ ℝ))
245244anbi2d 740 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝜑𝑥 ∈ ℝ) ↔ (𝜑𝑦 ∈ ℝ)))
246 oveq1 6697 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
247246fveq2d 6233 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
248 fveq2 6229 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
249247, 248eqeq12d 2666 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)))
250245, 249imbi12d 333 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝜑𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))))
251250, 111chvarv 2299 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
252251ad4ant14 1317 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
253240, 241, 242, 243, 252fperiodmul 39832 . . . . . . . . 9 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹𝑥))
254170, 178, 253, 185fperdvper 40451 . . . . . . . 8 (((𝜑𝑘 ∈ ℤ) ∧ 𝑥 ∈ dom (ℝ D 𝐹)) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥)))
255238, 239, 254syl2anc 694 . . . . . . 7 ((𝜑𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → ((𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹) ∧ ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥)))
256255simpld 474 . . . . . 6 ((𝜑𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom (ℝ D 𝐹))
257 oveq2 6698 . . . . . . . . . 10 (𝑤 = 𝑥 → (π − 𝑤) = (π − 𝑥))
258257oveq1d 6705 . . . . . . . . 9 (𝑤 = 𝑥 → ((π − 𝑤) / 𝑇) = ((π − 𝑥) / 𝑇))
259258fveq2d 6233 . . . . . . . 8 (𝑤 = 𝑥 → (⌊‘((π − 𝑤) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
260259oveq1d 6705 . . . . . . 7 (𝑤 = 𝑥 → ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
261260cbvmptv 4783 . . . . . 6 (𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
262 eqid 2651 . . . . . 6 (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑤 ∈ ℝ ↦ ((⌊‘((π − 𝑤) / 𝑇)) · 𝑇))‘𝑥)))
26361, 62, 161, 71, 256, 58, 261, 262, 23, 24, 25, 209fourierdlem41 40683 . . . . 5 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))))
264263simpld 474 . . . 4 (𝜑 → ∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)))
265125cnfldtop 22634 . . . . . . . . 9 (TopOpen‘ℂfld) ∈ Top
266265a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (TopOpen‘ℂfld) ∈ Top)
267236a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
268 mnfxr 10134 . . . . . . . . . . . 12 -∞ ∈ ℝ*
269268a1i 11 . . . . . . . . . . 11 (𝑦 ∈ ℝ → -∞ ∈ ℝ*)
270 rexr 10123 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → 𝑦 ∈ ℝ*)
271 mnflt 11995 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → -∞ < 𝑦)
272269, 270, 271xrltled 39800 . . . . . . . . . . 11 (𝑦 ∈ ℝ → -∞ ≤ 𝑦)
273 iooss1 12248 . . . . . . . . . . 11 ((-∞ ∈ ℝ* ∧ -∞ ≤ 𝑦) → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
274269, 272, 273syl2anc 694 . . . . . . . . . 10 (𝑦 ∈ ℝ → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
2752743ad2ant2 1103 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ (-∞(,)𝑋))
276 simp3 1083 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))
277275, 276ssind 3870 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)))
278 unicntop 22636 . . . . . . . . 9 ℂ = (TopOpen‘ℂfld)
279278lpss3 20996 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ Top ∧ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)) ⊆ ℂ ∧ (𝑦(,)𝑋) ⊆ ((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂfld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
280266, 267, 277, 279syl3anc 1366 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → ((limPt‘(TopOpen‘ℂfld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
2812803adant3l 1362 . . . . . 6 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂfld))‘(𝑦(,)𝑋)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
2822703ad2ant2 1103 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑦 ∈ ℝ*)
283583ad2ant1 1102 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ℝ)
284 simp3l 1109 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑦 < 𝑋)
285125, 282, 283, 284lptioo2cn 40195 . . . . . 6 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝑦(,)𝑋)))
286281, 285sseldd 3637 . . . . 5 ((𝜑𝑦 ∈ ℝ ∧ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
287286rexlimdv3a 3062 . . . 4 (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ dom (ℝ D 𝐹)) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹)))))
288264, 287mpd 15 . . 3 (𝜑𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘((-∞(,)𝑋) ∩ dom (ℝ D 𝐹))))
289255simprd 478 . . . 4 ((𝜑𝑥 ∈ dom (ℝ D 𝐹) ∧ 𝑘 ∈ ℤ) → ((ℝ D 𝐹)‘(𝑥 + (𝑘 · 𝑇))) = ((ℝ D 𝐹)‘𝑥))
290 oveq2 6698 . . . . . . . 8 (𝑦 = 𝑥 → (π − 𝑦) = (π − 𝑥))
291290oveq1d 6705 . . . . . . 7 (𝑦 = 𝑥 → ((π − 𝑦) / 𝑇) = ((π − 𝑥) / 𝑇))
292291fveq2d 6233 . . . . . 6 (𝑦 = 𝑥 → (⌊‘((π − 𝑦) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
293292oveq1d 6705 . . . . 5 (𝑦 = 𝑥 → ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
294293cbvmptv 4783 . . . 4 (𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)) = (𝑥 ∈ ℝ ↦ ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
295 id 22 . . . . . 6 (𝑧 = 𝑥𝑧 = 𝑥)
296 fveq2 6229 . . . . . 6 (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧) = ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥))
297295, 296oveq12d 6708 . . . . 5 (𝑧 = 𝑥 → (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧)) = (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
298297cbvmptv 4783 . . . 4 (𝑧 ∈ ℝ ↦ (𝑧 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑧))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((𝑦 ∈ ℝ ↦ ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))‘𝑥)))
29961, 62, 161, 23, 71, 24, 25, 155, 157, 256, 289, 134, 169, 58, 294, 298fourierdlem49 40690 . . 3 (𝜑 → (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim 𝑋) ≠ ∅)
300233, 237, 288, 299, 125ellimciota 40164 . 2 (𝜑 → (℩𝑥𝑥 ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim 𝑋)) ∈ (((ℝ D 𝐹) ↾ (-∞(,)𝑋)) lim 𝑋))
301 resindm 5479 . . . . . 6 (Rel (ℝ D 𝐹) → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
302226, 301syl 17 . . . . 5 (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) = ((ℝ D 𝐹) ↾ (𝑋(,)+∞)))
303 inss2 3867 . . . . . . 7 ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹)
304303a1i 11 . . . . . 6 (𝜑 → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ dom (ℝ D 𝐹))
305157, 304fssresd 6109 . . . . 5 (𝜑 → ((ℝ D 𝐹) ↾ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
306302, 305feq1dd 39661 . . . 4 (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℝ)
307306, 117fssd 6095 . . 3 (𝜑 → ((ℝ D 𝐹) ↾ (𝑋(,)+∞)):((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))⟶ℂ)
308 ioosscn 40034 . . . . 5 (𝑋(,)+∞) ⊆ ℂ
309 ssinss1 3874 . . . . 5 ((𝑋(,)+∞) ⊆ ℂ → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
310308, 309ax-mp 5 . . . 4 ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ
311310a1i 11 . . 3 (𝜑 → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
312263simprd 478 . . . 4 (𝜑 → ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)))
313265a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (TopOpen‘ℂfld) ∈ Top)
314310a1i 11 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ)
315 pnfxr 10130 . . . . . . . . . . . 12 +∞ ∈ ℝ*
316315a1i 11 . . . . . . . . . . 11 (𝑦 ∈ ℝ → +∞ ∈ ℝ*)
317 ltpnf 11992 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → 𝑦 < +∞)
318270, 316, 317xrltled 39800 . . . . . . . . . . 11 (𝑦 ∈ ℝ → 𝑦 ≤ +∞)
319 iooss2 12249 . . . . . . . . . . 11 ((+∞ ∈ ℝ*𝑦 ≤ +∞) → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
320316, 318, 319syl2anc 694 . . . . . . . . . 10 (𝑦 ∈ ℝ → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
3213203ad2ant2 1103 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ (𝑋(,)+∞))
322 simp3 1083 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))
323321, 322ssind 3870 . . . . . . . 8 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)))
324278lpss3 20996 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ Top ∧ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹)) ⊆ ℂ ∧ (𝑋(,)𝑦) ⊆ ((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂfld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
325313, 314, 323, 324syl3anc 1366 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹)) → ((limPt‘(TopOpen‘ℂfld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
3263253adant3l 1362 . . . . . 6 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → ((limPt‘(TopOpen‘ℂfld))‘(𝑋(,)𝑦)) ⊆ ((limPt‘(TopOpen‘ℂfld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
3272703ad2ant2 1103 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑦 ∈ ℝ*)
328583ad2ant1 1102 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ℝ)
329 simp3l 1109 . . . . . . 7 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 < 𝑦)
330125, 327, 328, 329lptioo1cn 40196 . . . . . 6 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘(𝑋(,)𝑦)))
331326, 330sseldd 3637 . . . . 5 ((𝜑𝑦 ∈ ℝ ∧ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ dom (ℝ D 𝐹))) → 𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘((𝑋(,)+∞) ∩ dom (ℝ D 𝐹))))
332331rexlimdv3a 3062 . . . 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 40689 . . 3 (𝜑 → (((ℝ D 𝐹) ↾ (𝑋(,)+∞)) lim 𝑋) ≠ ∅)
336307, 311, 333, 335, 125ellimciota 40164 . 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 6229 . . . . . . . 8 (𝑛 = 𝑘 → (𝐴𝑛) = (𝐴𝑘))
342 oveq1 6697 . . . . . . . . 9 (𝑛 = 𝑘 → (𝑛 · 𝑋) = (𝑘 · 𝑋))
343342fveq2d 6233 . . . . . . . 8 (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑋)) = (cos‘(𝑘 · 𝑋)))
344341, 343oveq12d 6708 . . . . . . 7 (𝑛 = 𝑘 → ((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) = ((𝐴𝑘) · (cos‘(𝑘 · 𝑋))))
345 fveq2 6229 . . . . . . . 8 (𝑛 = 𝑘 → (𝐵𝑛) = (𝐵𝑘))
346342fveq2d 6233 . . . . . . . 8 (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑋)) = (sin‘(𝑘 · 𝑋)))
347345, 346oveq12d 6708 . . . . . . 7 (𝑛 = 𝑘 → ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))) = ((𝐵𝑘) · (sin‘(𝑘 · 𝑋))))
348344, 347oveq12d 6708 . . . . . 6 (𝑛 = 𝑘 → (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = (((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋)))))
349348cbvsumv 14470 . . . . 5 Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑘 ∈ (1...𝑚)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋))))
350 oveq2 6698 . . . . . . 7 (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
351350eqcomd 2657 . . . . . 6 (𝑗 = 𝑚 → (1...𝑚) = (1...𝑗))
352351sumeq1d 14475 . . . . 5 (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑚)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑘 ∈ (1...𝑗)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋)))))
353349, 352syl5req 2698 . . . 4 (𝑗 = 𝑚 → Σ𝑘 ∈ (1...𝑗)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋)))) = Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))))
354353oveq2d 6706 . . 3 (𝑗 = 𝑚 → (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
355354cbvmptv 4783 . 2 (𝑗 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑘 ∈ (1...𝑗)(((𝐴𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵𝑘) · (sin‘(𝑘 · 𝑋)))))) = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))))
356 fourierdlem113.15 . 2 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋)))))
357 fdm 6089 . . . . . 6 (𝐹:ℝ⟶ℝ → dom 𝐹 = ℝ)
3581, 357syl 17 . . . . 5 (𝜑 → dom 𝐹 = ℝ)
359358, 154eqsstrd 3672 . . . 4 (𝜑 → dom 𝐹 ⊆ ℝ)
360358feq2d 6069 . . . . 5 (𝜑 → (𝐹:dom 𝐹⟶ℝ ↔ 𝐹:ℝ⟶ℝ))
3611, 360mpbird 247 . . . 4 (𝜑𝐹:dom 𝐹⟶ℝ)
362359sselda 3636 . . . . . . 7 ((𝜑𝑡 ∈ dom 𝐹) → 𝑡 ∈ ℝ)
363362adantr 480 . . . . . 6 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑡 ∈ ℝ)
364171adantl 481 . . . . . . 7 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℝ)
365177adantlr 751 . . . . . . 7 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → 𝑇 ∈ ℝ)
366364, 365remulcld 10108 . . . . . 6 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑘 · 𝑇) ∈ ℝ)
367363, 366readdcld 10107 . . . . 5 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ ℝ)
368358eqcomd 2657 . . . . . 6 (𝜑 → ℝ = dom 𝐹)
369368ad2antrr 762 . . . . 5 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → ℝ = dom 𝐹)
370367, 369eleqtrd 2732 . . . 4 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑡 + (𝑘 · 𝑇)) ∈ dom 𝐹)
371 id 22 . . . . . 6 ((𝜑𝑘 ∈ ℤ) → (𝜑𝑘 ∈ ℤ))
372371adantlr 751 . . . . 5 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝜑𝑘 ∈ ℤ))
373372, 363, 184syl2anc 694 . . . 4 (((𝜑𝑡 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑡 + (𝑘 · 𝑇))) = (𝐹𝑡))
374359, 361, 61, 62, 161, 71, 24, 77, 162, 85, 140, 222, 224, 370, 373, 194, 195fourierdlem71 40712 . . 3 (𝜑 → ∃𝑢 ∈ ℝ ∀𝑡 ∈ dom 𝐹(abs‘(𝐹𝑡)) ≤ 𝑢)
375358raleqdv 3174 . . . 4 (𝜑 → (∀𝑡 ∈ dom 𝐹(abs‘(𝐹𝑡)) ≤ 𝑢 ↔ ∀𝑡 ∈ ℝ (abs‘(𝐹𝑡)) ≤ 𝑢))
376375rexbidv 3081 . . 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 40753 1 (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119  {cpr 4212   class class class wbr 4685   ↦ cmpt 4762  dom cdm 5143  ran crn 5144   ↾ cres 5145  Rel wrel 5148  ℩cio 5887  Fun wfun 5920  ⟶wf 5922  ‘cfv 5926   Isom wiso 5927  (class class class)co 6690   ↑𝑚 cmap 7899  Fincfn 7997  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  +∞cpnf 10109  -∞cmnf 10110  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305   / cdiv 10722  ℕcn 11058  2c2 11108  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  (,)cioo 12213  (,]cioc 12214  [,)cico 12215  [,]cicc 12216  ...cfz 12364  ..^cfzo 12504  ⌊cfl 12631   mod cmo 12708  seqcseq 12841  #chash 13157  abscabs 14018   ⇝ cli 14259  Σcsu 14460  sincsin 14838  cosccos 14839  πcpi 14841  TopOpenctopn 16129  topGenctg 16145  ℂfldccnfld 19794  Topctop 20746  intcnt 20869  limPtclp 20986  –cn→ccncf 22726  ∫citg 23432   limℂ climc 23671   D cdv 23672 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cc 9295  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-ofr 6940  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-omul 7610  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-acn 8806  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-xnn0 11402  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-t1 21166  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-ovol 23279  df-vol 23280  df-mbf 23433  df-itg1 23434  df-itg2 23435  df-ibl 23436  df-itg 23437  df-0p 23482  df-ditg 23656  df-limc 23675  df-dv 23676 This theorem is referenced by:  fourierdlem114  40755
 Copyright terms: Public domain W3C validator