P. 462 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46101-46200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	stirlinglem13 46101*	𝐵 is decreasing and has a lower bound, then it converges. Since 𝐵 is log𝐴, in another theorem it is proven that 𝐴 converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))    ⇒   ⊢ ∃𝑑 ∈ ℝ 𝐵 ⇝ 𝑑
Theorem	stirlinglem14 46102*	The sequence 𝐴 converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (log‘(𝐴‘𝑛)))    ⇒   ⊢ ∃𝑐 ∈ ℝ+ 𝐴 ⇝ 𝑐
Theorem	stirlinglem15 46103*	The Stirling's formula is proven using a number of local definitions. The main theorem stirling 46104 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ Ⅎ𝑛𝜑    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ ((√‘((2 · π) · 𝑛)) · ((𝑛 / e)↑𝑛)))    &   ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ ((!‘𝑛) / ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛))))    &   ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝐴‘(2 · 𝑛)))    &   ⊢ 𝐸 = (𝑛 ∈ ℕ ↦ ((√‘(2 · 𝑛)) · ((𝑛 / e)↑𝑛)))    &   ⊢ 𝑉 = (𝑛 ∈ ℕ ↦ ((((2↑(4 · 𝑛)) · ((!‘𝑛)↑4)) / ((!‘(2 · 𝑛))↑2)) / ((2 · 𝑛) + 1)))    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛)↑4) / ((𝐷‘𝑛)↑2)))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 ⇝ 𝐶)    ⇒   ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((!‘𝑛) / (𝑆‘𝑛))) ⇝ 1)
Theorem	stirling 46104	Stirling's approximation formula for 𝑛 factorial. The proof follows two major steps: first it is proven that 𝑆 and 𝑛 factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for π it is proven that the unknown constant is the square root of π and then the exact Stirling's formula is established. This is Metamath 100 proof #90. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ ((√‘((2 · π) · 𝑛)) · ((𝑛 / e)↑𝑛)))    ⇒   ⊢ (𝑛 ∈ ℕ ↦ ((!‘𝑛) / (𝑆‘𝑛))) ⇝ 1
Theorem	stirlingr 46105	Stirling's approximation formula for 𝑛 factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 46104 is proven for convergence in the topology of complex numbers. The variable 𝑅 is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ ((√‘((2 · π) · 𝑛)) · ((𝑛 / e)↑𝑛)))    &   ⊢ 𝑅 = (⇝𝑡‘(topGen‘ran (,)))    ⇒   ⊢ (𝑛 ∈ ℕ ↦ ((!‘𝑛) / (𝑆‘𝑛)))𝑅1
21.43.15  Dirichlet kernel
Theorem	dirkerval 46106*	The Nth Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ 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)))))))
Theorem	dirker2re 46107	The Dirichlet Kernel value is a real if the argument is not a multiple of π . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ) ∧ ¬ (𝑆 mod (2 · π)) = 0) → ((sin‘((𝑁 + (1 / 2)) · 𝑆)) / ((2 · π) · (sin‘(𝑆 / 2)))) ∈ ℝ)
Theorem	dirkerdenne0 46108	The Dirichlet Kernel denominator is never 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝑆 ∈ ℝ ∧ ¬ (𝑆 mod (2 · π)) = 0) → ((2 · π) · (sin‘(𝑆 / 2))) ≠ 0)
Theorem	dirkerval2 46109*	The Nth Dirichlet Kernel evaluated at a specific point 𝑆. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ 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))))))
Theorem	dirkerre 46110*	The Dirichlet Kernel at any point evaluates to a real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ) → ((𝐷‘𝑁)‘𝑆) ∈ ℝ)
Theorem	dirkerper 46111*	the Dirichlet Kernel has period 2π. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    &   ⊢ 𝑇 = (2 · π)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℝ) → ((𝐷‘𝑁)‘(𝑥 + 𝑇)) = ((𝐷‘𝑁)‘𝑥))
Theorem	dirkerf 46112*	For any natural number 𝑁, the Dirichlet Kernel (𝐷‘𝑁) is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
Theorem	dirkertrigeqlem1 46113*	Sum of an even number of alternating cos values. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐾 ∈ ℕ → Σ𝑛 ∈ (1...(2 · 𝐾))(cos‘(𝑛 · π)) = 0)
Theorem	dirkertrigeqlem2 46114*	Trigonomic equality lemma for the Dirichlet Kernel trigonomic equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → (sin‘𝐴) ≠ 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
Theorem	dirkertrigeqlem3 46115*	Trigonometric equality lemma for the Dirichlet Kernel trigonometric equality. Here we handle the case for an angle that's an odd multiple of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ 𝐴 = (((2 · 𝐾) + 1) · π)    ⇒   ⊢ (𝜑 → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝐴))) / π) = ((sin‘((𝑁 + (1 / 2)) · 𝐴)) / ((2 · π) · (sin‘(𝐴 / 2)))))
Theorem	dirkertrigeq 46116*	Trigonometric equality for the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐹 = (𝐷‘𝑁)    &   ⊢ 𝐻 = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑘 ∈ (1...𝑁)(cos‘(𝑘 · 𝑠))) / π))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐻)
Theorem	dirkeritg 46117*	The definite integral of the Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if((𝑥 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑥)) / ((2 · π) · (sin‘(𝑥 / 2)))))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐹 = (𝐷‘𝑁)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 / 2) + Σ𝑘 ∈ (1...𝑁)((sin‘(𝑘 · 𝑥)) / 𝑘)) / π))    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)(𝐹‘𝑥) d𝑥 = ((𝐺‘𝐵) − (𝐺‘𝐴)))
Theorem	dirkercncflem1 46118*	If 𝑌 is a multiple of π then it belongs to an open inerval (𝐴(,)𝐵) such that for any other point 𝑦 in the interval, cos y/2 and sin y/2 are nonzero. Such an interval is needed to apply De L'Hopital theorem. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐴 = (𝑌 − π)    &   ⊢ 𝐵 = (𝑌 + π)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝐴(,)𝐵) ∧ ∀𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})((sin‘(𝑦 / 2)) ≠ 0 ∧ (cos‘(𝑦 / 2)) ≠ 0)))
Theorem	dirkercncflem2 46119*	Lemma used to prove that the Dirichlet Kernel is continuous at 𝑌 points that are multiples of (2 · π). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    &   ⊢ 𝐹 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑦)))    &   ⊢ 𝐺 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((2 · π) · (sin‘(𝑦 / 2))))    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (sin‘(𝑦 / 2)) ≠ 0)    &   ⊢ 𝐻 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ ((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑦))))    &   ⊢ 𝐼 = (𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌}) ↦ (π · (cos‘(𝑦 / 2))))    &   ⊢ 𝐿 = (𝑤 ∈ (𝐴(,)𝐵) ↦ (((𝑁 + (1 / 2)) · (cos‘((𝑁 + (1 / 2)) · 𝑤))) / (π · (cos‘(𝑤 / 2)))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝐴(,)𝐵) ∖ {𝑌})) → (cos‘(𝑦 / 2)) ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ (((𝐷‘𝑁) ↾ ((𝐴(,)𝐵) ∖ {𝑌})) limℂ 𝑌))
Theorem	dirkercncflem3 46120*	The Dirichlet Kernel is continuous at 𝑌 points that are multiples of (2 · π). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    &   ⊢ 𝐴 = (𝑌 − π)    &   ⊢ 𝐵 = (𝑌 + π)    &   ⊢ 𝐹 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))    &   ⊢ 𝐺 = (𝑦 ∈ (𝐴(,)𝐵) ↦ ((2 · π) · (sin‘(𝑦 / 2))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → (𝑌 mod (2 · π)) = 0)    ⇒   ⊢ (𝜑 → ((𝐷‘𝑁)‘𝑌) ∈ ((𝐷‘𝑁) limℂ 𝑌))
Theorem	dirkercncflem4 46121*	The Dirichlet Kernel is continuos at points that are not multiple of 2 π . This is the easier condition, for the proof of the continuity of the Dirichlet kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → (𝑌 mod (2 · π)) ≠ 0)    &   ⊢ 𝐴 = (⌊‘(𝑌 / (2 · π)))    &   ⊢ 𝐵 = (𝐴 + 1)    &   ⊢ 𝐶 = (𝐴 · (2 · π))    &   ⊢ 𝐸 = (𝐵 · (2 · π))    ⇒   ⊢ (𝜑 → (𝐷‘𝑁) ∈ (((topGen‘ran (,)) CnP (topGen‘ran (,)))‘𝑌))
Theorem	dirkercncf 46122*	For any natural number 𝑁, the Dirichlet Kernel (𝐷‘𝑁) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if((𝑦 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑦)) / ((2 · π) · (sin‘(𝑦 / 2)))))))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
21.43.16  Fourier Series
Theorem	fourierdlem1 46123	A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))    &   ⊢ (𝜑 → 𝑋 ∈ ((𝑄‘𝐼)[,](𝑄‘(𝐼 + 1))))    ⇒   ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))
Theorem	fourierdlem2 46124*	Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    ⇒   ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
Theorem	fourierdlem3 46125*	Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ ((-π[,]π) ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    ⇒   ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ ((-π[,]π) ↑m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
Theorem	fourierdlem4 46126*	𝐸 is a function that maps any point to a periodic corresponding point in (𝐴, 𝐵]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    ⇒   ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
Theorem	fourierdlem5 46127*	𝑆 is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑆 = (𝑥 ∈ (-π[,]π) ↦ (sin‘((𝑋 + (1 / 2)) · 𝑥)))    ⇒   ⊢ (𝑋 ∈ ℝ → 𝑆:(-π[,]π)⟶ℝ)
Theorem	fourierdlem6 46128	𝑋 is in the periodic partition, when the considered interval is centered at 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝐼 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝐼 < 𝐽)    &   ⊢ (𝜑 → (𝑋 + (𝐼 · 𝑇)) ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (𝑋 + (𝐽 · 𝑇)) ∈ (𝐴[,]𝐵))    ⇒   ⊢ (𝜑 → 𝐽 = (𝐼 + 1))
Theorem	fourierdlem7 46129*	The difference between the periodic sawtooth function and the identity function is decreasing. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ≤ 𝑌)    ⇒   ⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ≤ ((𝐸‘𝑋) − 𝑋))
Theorem	fourierdlem8 46130	A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐼)[,](𝑄‘(𝐼 + 1))) ⊆ (𝐴[,]𝐵))
Theorem	fourierdlem9 46131*	𝐻 is a complex function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ)    &   ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))    ⇒   ⊢ (𝜑 → 𝐻:(-π[,]π)⟶ℝ)
Theorem	fourierdlem10 46132	Condition on the bounds of a nonempty subinterval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    &   ⊢ (𝜑 → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵))
Theorem	fourierdlem11 46133*	If there is a partition, than the lower bound is strictly less than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    ⇒   ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
Theorem	fourierdlem12 46134*	A point of a partition is not an element of any open interval determined by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑄)    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
Theorem	fourierdlem13 46135*	Value of 𝑉 in terms of value of 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑋) ∧ (𝑝‘𝑚) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))    &   ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐼) = ((𝑉‘𝐼) − 𝑋) ∧ (𝑉‘𝐼) = (𝑋 + (𝑄‘𝐼))))
Theorem	fourierdlem14 46136*	Given the partition 𝑉, 𝑄 is the partition shifted to the left by 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑋) ∧ (𝑝‘𝑚) = (𝐵 + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))    &   ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))    ⇒   ⊢ (𝜑 → 𝑄 ∈ (𝑂‘𝑀))
Theorem	fourierdlem15 46137*	The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    ⇒   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
Theorem	fourierdlem16 46138*	The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ 𝐶 = (-π(,)π)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ 𝐿1)    &   ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (((𝐴‘𝑁) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿1) ∧ ∫𝐶((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 ∈ ℝ))
Theorem	fourierdlem17 46139*	The defined 𝐿 is actually a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝐿 = (𝑥 ∈ (𝐴(,]𝐵) ↦ if(𝑥 = 𝐵, 𝐴, 𝑥))    ⇒   ⊢ (𝜑 → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
Theorem	fourierdlem18 46140*	The function 𝑆 is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠)))    ⇒   ⊢ (𝜑 → 𝑆 ∈ ((-π[,]π)–cn→ℝ))
Theorem	fourierdlem19 46141*	If two elements of 𝐷 have the same periodic image in (𝐴(,]𝐵) then they are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝐷 = {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    &   ⊢ (𝜑 → 𝑊 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐷)    &   ⊢ (𝜑 → (𝐸‘𝑍) = (𝐸‘𝑊))    ⇒   ⊢ (𝜑 → ¬ 𝑊 < 𝑍)
Theorem	fourierdlem20 46142*	Every interval in the partition 𝑆 is included in an interval of the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)    &   ⊢ (𝜑 → (𝑄‘0) ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ≤ (𝑄‘𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))    &   ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))    &   ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))    &   ⊢ 𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < )    ⇒   ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
Theorem	fourierdlem21 46143*	The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ 𝐶 = (-π(,)π)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ 𝐿1)    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (((𝐵‘𝑁) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1) ∧ ∫𝐶((𝐹‘𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 ∈ ℝ))
Theorem	fourierdlem22 46144*	The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ 𝐶 = (-π(,)π)    &   ⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ 𝐿1)    &   ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))    &   ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))    ⇒   ⊢ (𝜑 → ((𝑛 ∈ ℕ0 → (𝐴‘𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵‘𝑛) ∈ ℝ)))
Theorem	fourierdlem23 46145*	If 𝐹 is continuous and 𝑋 is constant, then (𝐹‘(𝑋 + 𝑠)) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ))    &   ⊢ (𝜑 → 𝐵 ⊆ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑋 + 𝑠) ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑠 ∈ 𝐵 ↦ (𝐹‘(𝑋 + 𝑠))) ∈ (𝐵–cn→ℂ))
Theorem	fourierdlem24 46146	A sufficient condition for module being nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ((-π[,]π) ∖ {0}) → (𝐴 mod (2 · π)) ≠ 0)
Theorem	fourierdlem25 46147*	If 𝐶 is not in the range of the partition, then it is in an open interval induced by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ((𝑄‘0)[,](𝑄‘𝑀)))    &   ⊢ (𝜑 → ¬ 𝐶 ∈ ran 𝑄)    &   ⊢ 𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < )    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ (0..^𝑀)𝐶 ∈ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))))
Theorem	fourierdlem26 46148*	Periodic image of a point 𝑌 that's in the period that begins with the point 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → (𝐸‘𝑋) = 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋(,](𝑋 + 𝑇)))    ⇒   ⊢ (𝜑 → (𝐸‘𝑌) = (𝐴 + (𝑌 − 𝑋)))
Theorem	fourierdlem27 46149	A partition open interval is a subset of the partitioned open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))    ⇒   ⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (𝐴(,)𝐵))
Theorem	fourierdlem28 46150*	Derivative of (𝐹‘(𝑋 + 𝑠)). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ 𝐷 = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))    &   ⊢ (𝜑 → 𝐷:((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)    ⇒   ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐷‘(𝑋 + 𝑠))))
Theorem	fourierdlem29 46151*	Explicit function value for 𝐾 applied to 𝐴. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))    ⇒   ⊢ (𝐴 ∈ (-π[,]π) → (𝐾‘𝐴) = if(𝐴 = 0, 1, (𝐴 / (2 · (sin‘(𝐴 / 2))))))
Theorem	fourierdlem30 46152*	Sum of three small pieces is less than ε. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝐹 · -𝐺)) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ 𝑋 = (abs‘𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝑌 = (abs‘𝐶)    &   ⊢ 𝑍 = (abs‘∫𝐼(𝐹 · -𝐺) d𝑥)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1) ≤ 𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝐵) ≤ 1)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘𝐷) ≤ 1)    ⇒   ⊢ (𝜑 → (abs‘(((𝐴 · -(𝐵 / 𝑅)) − (𝐶 · -(𝐷 / 𝑅))) − ∫𝐼(𝐹 · -(𝐺 / 𝑅)) d𝑥)) < 𝐸)
Theorem	fourierdlem31 46153*	If 𝐴 is finite and for any element in 𝐴 there is a number 𝑚 such that a property holds for all numbers larger than 𝑚, then there is a number 𝑛 such that the property holds for all numbers larger than 𝑛 and for all elements in 𝐴. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.)
⊢ Ⅎ𝑖𝜑    &   ⊢ Ⅎ𝑟𝜑    &   ⊢ Ⅎ𝑖𝑉    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)    &   ⊢ 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}    &   ⊢ 𝑉 = (𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < ))    &   ⊢ 𝑁 = sup(ran 𝑉, ℝ, < )    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒)
Theorem	fourierdlem32 46154	Limit of a continuous function on an open subinterval. Lower bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝑅 ∈ (𝐹 limℂ 𝐴))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    &   ⊢ (𝜑 → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))    &   ⊢ 𝑌 = if(𝐶 = 𝐴, 𝑅, (𝐹‘𝐶))    &   ⊢ 𝐽 = ((TopOpen‘ℂfld) ↾t (𝐴[,)𝐵))    ⇒   ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐶))
Theorem	fourierdlem33 46155	Limit of a continuous function on an open subinterval. Upper bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → 𝐿 ∈ (𝐹 limℂ 𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    &   ⊢ (𝜑 → (𝐶(,)𝐷) ⊆ (𝐴(,)𝐵))    &   ⊢ 𝑌 = if(𝐷 = 𝐵, 𝐿, (𝐹‘𝐷))    &   ⊢ 𝐽 = ((TopOpen‘ℂfld) ↾t ((𝐴(,)𝐵) ∪ {𝐵}))    ⇒   ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝐶(,)𝐷)) limℂ 𝐷))
Theorem	fourierdlem34 46156*	A partition is one to one. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    ⇒   ⊢ (𝜑 → 𝑄:(0...𝑀)–1-1→ℝ)
Theorem	fourierdlem35 46157	There is a single point in (𝐴(,]𝐵) that's distant from 𝑋 a multiple integer of 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝐼 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → (𝑋 + (𝐼 · 𝑇)) ∈ (𝐴(,]𝐵))    &   ⊢ (𝜑 → (𝑋 + (𝐽 · 𝑇)) ∈ (𝐴(,]𝐵))    ⇒   ⊢ (𝜑 → 𝐼 = 𝐽)
Theorem	fourierdlem36 46158*	𝐹 is an isomorphism. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝐹 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐴))    &   ⊢ 𝑁 = ((♯‘𝐴) − 1)    ⇒   ⊢ (𝜑 → 𝐹 Isom < , < ((0...𝑁), 𝐴))
Theorem	fourierdlem37 46159*	𝐼 is a function that maps any real point to the point that in the partition that immediately precedes the corresponding periodic point in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    &   ⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))    &   ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ))    ⇒   ⊢ (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})))
Theorem	fourierdlem38 46160*	The function 𝐹 is continuous on every interval induced by the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 ∈ (dom 𝐹–cn→ℂ))    &   ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ 𝐻 = (𝐴 ∪ ((-π[,]π) ∖ dom 𝐹))    &   ⊢ (𝜑 → ran 𝑄 = 𝐻)    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
Theorem	fourierdlem39 46161*	Integration by parts of ∫(𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))    &   ⊢ 𝐺 = (ℝ D 𝐹)    &   ⊢ (𝜑 → 𝐺 ∈ ((𝐴(,)𝐵)–cn→ℂ))    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ (𝐴(,)𝐵)(abs‘(𝐺‘𝑥)) ≤ 𝑦)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑅 · 𝑥))) d𝑥 = ((((𝐹‘𝐵) · -((cos‘(𝑅 · 𝐵)) / 𝑅)) − ((𝐹‘𝐴) · -((cos‘(𝑅 · 𝐴)) / 𝑅))) − ∫(𝐴(,)𝐵)((𝐺‘𝑥) · -((cos‘(𝑅 · 𝑥)) / 𝑅)) d𝑥))
Theorem	fourierdlem40 46162*	𝐻 is a continuous function on any partition interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (-π[,]π))    &   ⊢ (𝜑 → 𝐵 ∈ (-π[,]π))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐵 + 𝑋))–cn→ℂ))    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ)    &   ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))    ⇒   ⊢ (𝜑 → (𝐻 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
Theorem	fourierdlem41 46163*	Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥)))    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ 𝐷)    ⇒   ⊢ (𝜑 → (∃𝑦 ∈ ℝ (𝑦 < 𝑋 ∧ (𝑦(,)𝑋) ⊆ 𝐷) ∧ ∃𝑦 ∈ ℝ (𝑋 < 𝑦 ∧ (𝑋(,)𝑦) ⊆ 𝐷)))
Theorem	fourierdlem42 46164*	The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    &   ⊢ 𝑇 = (𝐶 − 𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ 𝐷 = (abs ∘ − )    &   ⊢ 𝐼 = ((𝐴 × 𝐴) ∖ I )    &   ⊢ 𝑅 = ran (𝐷 ↾ 𝐼)    &   ⊢ 𝐸 = inf(𝑅, ℝ, < )    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐾 = (𝐽 ↾t (𝑋[,]𝑌))    &   ⊢ 𝐻 = {𝑥 ∈ (𝑋[,]𝑌) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ 𝐴}    &   ⊢ (𝜓 ↔ ((𝜑 ∧ (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑎 < 𝑏)) ∧ ∃𝑗 ∈ ℤ ∃𝑘 ∈ ℤ ((𝑎 + (𝑗 · 𝑇)) ∈ 𝐴 ∧ (𝑏 + (𝑘 · 𝑇)) ∈ 𝐴)))    ⇒   ⊢ (𝜑 → 𝐻 ∈ Fin)
Theorem	fourierdlem43 46165	𝐾 is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))    ⇒   ⊢ 𝐾:(-π[,]π)⟶ℝ
Theorem	fourierdlem44 46166	A condition for having (sin‘(𝐴 / 2)) nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ (-π[,]π) ∧ 𝐴 ≠ 0) → (sin‘(𝐴 / 2)) ≠ 0)
Theorem	fourierdlem46 46167*	The function 𝐹 has a limit at the bounds of every interval induced by the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 ∈ (dom 𝐹–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅)    &   ⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻))    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻)    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))    &   ⊢ (𝜑 → (𝑄‘𝐼) < (𝑄‘(𝐼 + 1)))    &   ⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-π(,)π))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ 𝐻 = ({-π, π, 𝐶} ∪ ((-π[,]π) ∖ dom 𝐹))    &   ⊢ (𝜑 → ran 𝑄 = 𝐻)    ⇒   ⊢ (𝜑 → (((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅ ∧ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅))
Theorem	fourierdlem47 46168*	For 𝑟 large enough, the final expression is less than the given positive 𝐸. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐹) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (𝑥 ∈ 𝐼 ↦ (𝐹 · -𝐺)) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ ℂ)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℂ) → 𝐺 ∈ ℂ)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑟 ∈ ℝ) → (abs‘𝐺) ≤ 1)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ 𝑋 = (abs‘𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ 𝑌 = (abs‘𝐶)    &   ⊢ 𝑍 = ∫𝐼(abs‘𝐹) d𝑥    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (abs‘𝐵) ≤ 1)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → 𝐷 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → (abs‘𝐷) ≤ 1)    &   ⊢ 𝑀 = ((⌊‘((((𝑋 + 𝑌) + 𝑍) / 𝐸) + 1)) + 1)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)(abs‘(((𝐴 · -(𝐵 / 𝑟)) − (𝐶 · -(𝐷 / 𝑟))) − ∫𝐼(𝐹 · -(𝐺 / 𝑟)) d𝑥)) < 𝐸)
Theorem	fourierdlem48 46169*	The given periodic function 𝐹 has a right limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥)))    &   ⊢ (𝜒 ↔ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑦 ∈ ((𝑄‘𝑖)[,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ ℤ) ∧ 𝑦 = (𝑋 + (𝑘 · 𝑇))))    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋) ≠ ∅)
Theorem	fourierdlem49 46170*	The given periodic function 𝐹 has a left limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑍 = (𝑥 ∈ ℝ ↦ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + (𝑍‘𝑥)))    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋) ≠ ∅)
Theorem	fourierdlem50 46171*	Continuity of 𝑂 and its limits with respect to the 𝑆 partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))    &   ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))    &   ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))    &   ⊢ 𝑁 = ((♯‘𝑇) − 1)    &   ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))    &   ⊢ 𝑈 = (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))    &   ⊢ (𝜒 ↔ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))))    ⇒   ⊢ (𝜑 → (𝑈 ∈ (0..^𝑀) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1)))))
Theorem	fourierdlem51 46172*	𝑋 is in the periodic partition, when the considered interval is centered at 𝑋. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    &   ⊢ (𝜑 → 0 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐶)    &   ⊢ 𝐷 = ({(𝐴 + 𝑋), (𝐵 + 𝑋)} ∪ {𝑦 ∈ ((𝐴 + 𝑋)[,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶})    &   ⊢ 𝐹 = (℩𝑓𝑓 Isom < , < ((0...((♯‘𝐷) − 1)), 𝐷))    &   ⊢ 𝐻 = {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶}    ⇒   ⊢ (𝜑 → 𝑋 ∈ ran 𝐹)
Theorem	fourierdlem52 46173*	d16:d17,d18:jca |- ( ph -> ( ( S 0) ≤ 𝐴 ∧ 𝐴 ≤ (𝑆 0 ) ) ) . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑇 ∈ Fin)    &   ⊢ 𝑁 = ((♯‘𝑇) − 1)    &   ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑇)    ⇒   ⊢ (𝜑 → ((𝑆:(0...𝑁)⟶(𝐴[,]𝐵) ∧ (𝑆‘0) = 𝐴) ∧ (𝑆‘𝑁) = 𝐵))
Theorem	fourierdlem53 46174*	The limit of 𝐹(𝑠) at (𝑋 + 𝐷) is the limit of 𝐹(𝑋 + 𝑠) at 𝐷. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝐺 = (𝑠 ∈ 𝐴 ↦ (𝐹‘(𝑋 + 𝑠)))    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑋 + 𝑠) ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ≠ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝑋 + 𝐷)))    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → 𝐶 ∈ (𝐺 limℂ 𝐷))
Theorem	fourierdlem54 46175*	Given a partition 𝑄 and an arbitrary interval [𝐶, 𝐷], a partition 𝑆 on [𝐶, 𝐷] is built such that it preserves any periodic function piecewise continuous on 𝑄 will be piecewise continuous on 𝑆, with the same limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    &   ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})    &   ⊢ 𝑁 = ((♯‘𝐻) − 1)    &   ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))    ⇒   ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
Theorem	fourierdlem55 46176*	𝑈 is a real function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ)    &   ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))    &   ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))    &   ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠)))    ⇒   ⊢ (𝜑 → 𝑈:(-π[,]π)⟶ℝ)
Theorem	fourierdlem56 46177*	Derivative of the 𝐾 function on an interval not containing ' 0 '. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ((-π[,]π) ∖ {0}))    &   ⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0)    ⇒   ⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐾‘𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((((sin‘(𝑠 / 2)) − (((cos‘(𝑠 / 2)) / 2) · 𝑠)) / ((sin‘(𝑠 / 2))↑2)) / 2)))
Theorem	fourierdlem57 46178*	The derivative of 𝑂. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))    &   ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))    ⇒   ⊢ ((𝜑 → ((ℝ D 𝑂):(𝐴(,)𝐵)⟶ℝ ∧ (ℝ D 𝑂) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)) · (2 · (sin‘(𝑠 / 2)))) − ((cos‘(𝑠 / 2)) · ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) / ((2 · (sin‘(𝑠 / 2)))↑2))))) ∧ (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (cos‘(𝑠 / 2))))
Theorem	fourierdlem58 46179*	The derivative of 𝐾 is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐾 = (𝑠 ∈ 𝐴 ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))    &   ⊢ (𝜑 → 𝐴 ⊆ (-π[,]π))    &   ⊢ (𝜑 → ¬ 0 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ (topGen‘ran (,)))    ⇒   ⊢ (𝜑 → (ℝ D 𝐾) ∈ (𝐴–cn→ℝ))
Theorem	fourierdlem59 46180*	The derivative of 𝐻 is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℝ))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ 𝐻 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))    ⇒   ⊢ (𝜑 → (ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℝ))
Theorem	fourierdlem60 46181*	Given a differentiable function 𝐹, with finite limit of the derivative at 𝐴 the derived function 𝐻 has a limit at 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐵))    &   ⊢ 𝐺 = (ℝ D 𝐹)    &   ⊢ (𝜑 → dom 𝐺 = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐺 limℂ 𝐵))    &   ⊢ 𝐻 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ (((𝐹‘(𝐵 + 𝑠)) − 𝑌) / 𝑠))    &   ⊢ 𝑁 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ ((𝐹‘(𝐵 + 𝑠)) − 𝑌))    &   ⊢ 𝐷 = (𝑠 ∈ ((𝐴 − 𝐵)(,)0) ↦ 𝑠)    ⇒   ⊢ (𝜑 → 𝐸 ∈ (𝐻 limℂ 0))
Theorem	fourierdlem61 46182*	Given a differentiable function 𝐹, with finite limit of the derivative at 𝐴 the derived function 𝐻 has a limit at 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐹 limℂ 𝐴))    &   ⊢ 𝐺 = (ℝ D 𝐹)    &   ⊢ (𝜑 → dom 𝐺 = (𝐴(,)𝐵))    &   ⊢ (𝜑 → 𝐸 ∈ (𝐺 limℂ 𝐴))    &   ⊢ 𝐻 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ (((𝐹‘(𝐴 + 𝑠)) − 𝑌) / 𝑠))    &   ⊢ 𝑁 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ ((𝐹‘(𝐴 + 𝑠)) − 𝑌))    &   ⊢ 𝐷 = (𝑠 ∈ (0(,)(𝐵 − 𝐴)) ↦ 𝑠)    ⇒   ⊢ (𝜑 → 𝐸 ∈ (𝐻 limℂ 0))
Theorem	fourierdlem62 46183	The function 𝐾 is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐾 = (𝑦 ∈ (-π[,]π) ↦ if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2))))))    ⇒   ⊢ 𝐾 ∈ ((-π[,]π)–cn→ℝ)
Theorem	fourierdlem63 46184*	The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    &   ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})    &   ⊢ 𝑁 = ((♯‘𝐻) − 1)    &   ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    &   ⊢ (𝜑 → 𝐾 ∈ (0...𝑀))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))    &   ⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))))    &   ⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾))    &   ⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))    ⇒   ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾))
Theorem	fourierdlem64 46185*	The partition 𝑉 is finer than 𝑄, when 𝑄 is moved on the same interval where 𝑉 lies. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    &   ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})    &   ⊢ 𝑁 = ((♯‘𝐻) − 1)    &   ⊢ 𝑉 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))    &   ⊢ 𝐿 = sup({𝑘 ∈ ℤ ∣ ((𝑄‘0) + (𝑘 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )    &   ⊢ 𝐼 = sup({𝑗 ∈ (0..^𝑀) ∣ ((𝑄‘𝑗) + (𝐿 · 𝑇)) ≤ (𝑉‘𝐽)}, ℝ, < )    ⇒   ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐿 ∈ ℤ) ∧ ∃𝑖 ∈ (0..^𝑀)∃𝑙 ∈ ℤ ((𝑉‘𝐽)(,)(𝑉‘(𝐽 + 1))) ⊆ (((𝑄‘𝑖) + (𝑙 · 𝑇))(,)((𝑄‘(𝑖 + 1)) + (𝑙 · 𝑇)))))
Theorem	fourierdlem65 46186*	The distance of two adjacent points in the moved partition is preserved in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))    &   ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)    &   ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    &   ⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))    &   ⊢ 𝑍 = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))    ⇒   ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝐿‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
Theorem	fourierdlem66 46187*	Value of the 𝐺 function when the argument is not zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ)    &   ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))    &   ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))    &   ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))    &   ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠)))    &   ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑛 + (1 / 2)) · 𝑠)))    &   ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠)))    &   ⊢ 𝐴 = ((-π[,]π) ∖ {0})    ⇒   ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑠 ∈ 𝐴) → (𝐺‘𝑠) = (π · (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) · ((𝐷‘𝑛)‘𝑠))))
Theorem	fourierdlem67 46188*	𝐺 is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ)    &   ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))    &   ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))    &   ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠)))    &   ⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠)))    &   ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠)))    ⇒   ⊢ (𝜑 → 𝐺:(-π[,]π)⟶ℝ)
Theorem	fourierdlem68 46189*	The derivative of 𝑂 is bounded on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))    &   ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘(𝐹‘𝑡)) ≤ 𝐷)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) → (abs‘((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘𝑡)) ≤ 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / (2 · (sin‘(𝑠 / 2)))))    ⇒   ⊢ (𝜑 → (dom (ℝ D 𝑂) = (𝐴(,)𝐵) ∧ ∃𝑏 ∈ ℝ ∀𝑠 ∈ dom (ℝ D 𝑂)(abs‘((ℝ D 𝑂)‘𝑠)) ≤ 𝑏))
Theorem	fourierdlem69 46190*	A piecewise continuous function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))    ⇒   ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
Theorem	fourierdlem70 46191*	A piecewise continuous function is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)    &   ⊢ (𝜑 → (𝑄‘0) = 𝐴)    &   ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))    &   ⊢ 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑠 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑠)) ≤ 𝑥)
Theorem	fourierdlem71 46192*	A periodic piecewise continuous function, possibly undefined on a finite set in each periodic interval, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → dom 𝐹 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)    &   ⊢ (𝜑 → (𝑄‘0) = 𝐴)    &   ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))    &   ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝑥 + (𝑘 · 𝑇)) ∈ dom 𝐹)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑘 ∈ ℤ) → (𝐹‘(𝑥 + (𝑘 · 𝑇))) = (𝐹‘𝑥))    &   ⊢ 𝐼 = (𝑖 ∈ (0..^𝑀) ↦ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐹(abs‘(𝐹‘𝑥)) ≤ 𝑦)
Theorem	fourierdlem72 46193*	The derivative of 𝑂 is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℝ))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (-π[,]π))    &   ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))    &   ⊢ (𝜑 → 𝑈 ∈ (0..^𝑀))    &   ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1))))    &   ⊢ 𝐻 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))    &   ⊢ 𝐾 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))    &   ⊢ 𝑂 = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠)))    ⇒   ⊢ (𝜑 → (ℝ D 𝑂) ∈ ((𝐴(,)𝐵)–cn→ℂ))
Theorem	fourierdlem73 46194*	A version of the Riemann Lebesgue lemma: as 𝑟 increases, the integral in 𝑆 goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))    &   ⊢ (𝜑 → (𝑄‘0) = 𝐴)    &   ⊢ (𝜑 → (𝑄‘𝑀) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)))    &   ⊢ 𝐺 = (ℝ D 𝐹)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ dom 𝐺(abs‘(𝐺‘𝑥)) ≤ 𝑦)    &   ⊢ 𝑆 = (𝑟 ∈ ℝ+ ↦ ∫(𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑟 · 𝑥))) d𝑥)    &   ⊢ 𝐷 = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))))    ⇒   ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)(abs‘∫(𝐴(,)𝐵)((𝐹‘𝑥) · (sin‘(𝑟 · 𝑥))) d𝑥) < 𝑒)
Theorem	fourierdlem74 46195*	Given a piecewise smooth function 𝐹, the derived function 𝐻 has a limit at the upper bound of each interval of the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋))    &   ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1))))    &   ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))    &   ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝐺 = (ℝ D 𝐹)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)    &   ⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) limℂ 𝑋))    &   ⊢ 𝐴 = if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))
Theorem	fourierdlem75 46196*	Given a piecewise smooth function 𝐹, the derived function 𝐻 has a limit at the lower bound of each interval of the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋))    &   ⊢ (𝜑 → 𝑊 ∈ ℝ)    &   ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖)))    &   ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))    &   ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝐺 = (ℝ D 𝐹)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ ((𝐺 ↾ (𝑋(,)+∞)) limℂ 𝑋))    &   ⊢ 𝐴 = if((𝑉‘𝑖) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘𝑖) < 𝑋, 𝑊, 𝑌)) / (𝑄‘𝑖)))    ⇒   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)))
Theorem	fourierdlem76 46197*	Continuity of 𝑂 and its limits with respect to the 𝑆 partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘𝑖)))    &   ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) limℂ (𝑉‘(𝑖 + 1))))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))    &   ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))    &   ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))    &   ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))    &   ⊢ 𝑁 = ((♯‘𝑇) − 1)    &   ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))    &   ⊢ 𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))))    &   ⊢ 𝐸 = (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))))    &   ⊢ (𝜒 ↔ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))    ⇒   ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) limℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))
Theorem	fourierdlem77 46198*	If 𝐻 is bounded, then 𝑈 is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ)    &   ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))    &   ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))    &   ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠)))    &   ⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑠 ∈ (-π[,]π)(abs‘(𝐻‘𝑠)) ≤ 𝑎)    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ ℝ+ ∀𝑠 ∈ (-π[,]π)(abs‘(𝑈‘𝑠)) ≤ 𝑏)
Theorem	fourierdlem78 46199*	𝐺 is continuous when restricted on an interval not containing 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (-π[,]π))    &   ⊢ (𝜑 → 𝐵 ∈ (-π[,]π))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵))    &   ⊢ (𝜑 → (𝐹 ↾ ((𝐴 + 𝑋)(,)(𝐵 + 𝑋))) ∈ (((𝐴 + 𝑋)(,)(𝐵 + 𝑋))–cn→ℂ))    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝑊 ∈ ℝ)    &   ⊢ 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))    &   ⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))    &   ⊢ 𝑈 = (𝑠 ∈ (-π[,]π) ↦ ((𝐻‘𝑠) · (𝐾‘𝑠)))    &   ⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ 𝑆 = (𝑠 ∈ (-π[,]π) ↦ (sin‘((𝑁 + (1 / 2)) · 𝑠)))    &   ⊢ 𝐺 = (𝑠 ∈ (-π[,]π) ↦ ((𝑈‘𝑠) · (𝑆‘𝑠)))    ⇒   ⊢ (𝜑 → (𝐺 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℝ))
Theorem	fourierdlem79 46200*	𝐸 projects every interval of the partition induced by 𝑆 on 𝐻 into a corresponding interval of the partition induced by 𝑄 on [𝐴, 𝐵]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝑇 = (𝐵 − 𝐴)    &   ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 < 𝐷)    &   ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})    &   ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})    &   ⊢ 𝑁 = ((♯‘𝐻) − 1)    &   ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))    &   ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))    &   ⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))    &   ⊢ 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))    &   ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ))    ⇒   ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))