fourierdlem106

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem106.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem106.t	⊢ 𝑇 = ( 2 · π )
	fourierdlem106.per	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
	fourierdlem106.g	⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
	fourierdlem106.dmdv	⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
	fourierdlem106.dvcn	⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
	fourierdlem106.rlim	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) lim_ℂ 𝑥 ) ≠ ∅ )
	fourierdlem106.llim	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) lim_ℂ 𝑥 ) ≠ ∅ )
	fourierdlem106.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
Assertion	fourierdlem106	⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim_ℂ 𝑋 ) ≠ ∅ ∧ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim_ℂ 𝑋 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem106.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierdlem106.t	⊢ 𝑇 = ( 2 · π )
3		fourierdlem106.per	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
4		fourierdlem106.g	⊢ 𝐺 = ( ( ℝ D 𝐹 ) ↾ ( - π (,) π ) )
5		fourierdlem106.dmdv	⊢ ( 𝜑 → ( ( - π (,) π ) ∖ dom 𝐺 ) ∈ Fin )
6		fourierdlem106.dvcn	⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝐺 –cn→ ℂ ) )
7		fourierdlem106.rlim	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π [,) π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( 𝑥 (,) +∞ ) ) lim_ℂ 𝑥 ) ≠ ∅ )
8		fourierdlem106.llim	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( - π (,] π ) ∖ dom 𝐺 ) ) → ( ( 𝐺 ↾ ( -∞ (,) 𝑥 ) ) lim_ℂ 𝑥 ) ≠ ∅ )
9		fourierdlem106.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
10		eqid	⊢ ( 𝑘 ∈ ℕ ↦ { 𝑤 ∈ ( ℝ ↑_m ( 0 ... 𝑘 ) ) ∣ ( ( ( 𝑤 ‘ 0 ) = - π ∧ ( 𝑤 ‘ 𝑘 ) = π ) ∧ ∀ 𝑧 ∈ ( 0 ..^ 𝑘 ) ( 𝑤 ‘ 𝑧 ) < ( 𝑤 ‘ ( 𝑧 + 1 ) ) ) } ) = ( 𝑘 ∈ ℕ ↦ { 𝑤 ∈ ( ℝ ↑_m ( 0 ... 𝑘 ) ) ∣ ( ( ( 𝑤 ‘ 0 ) = - π ∧ ( 𝑤 ‘ 𝑘 ) = π ) ∧ ∀ 𝑧 ∈ ( 0 ..^ 𝑘 ) ( 𝑤 ‘ 𝑧 ) < ( 𝑤 ‘ ( 𝑧 + 1 ) ) ) } )
11		id	⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
12		oveq2	⊢ ( 𝑦 = 𝑥 → ( π − 𝑦 ) = ( π − 𝑥 ) )
13	12	oveq1d	⊢ ( 𝑦 = 𝑥 → ( ( π − 𝑦 ) / 𝑇 ) = ( ( π − 𝑥 ) / 𝑇 ) )
14	13	fveq2d	⊢ ( 𝑦 = 𝑥 → ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) )
15	14	oveq1d	⊢ ( 𝑦 = 𝑥 → ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
16	11 15	oveq12d	⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
17	16	cbvmptv	⊢ ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
18		eqid	⊢ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) = ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) )
19		eqid	⊢ ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 ) = ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 )
20		isoeq1	⊢ ( 𝑔 = 𝑓 → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 ) ) , ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) ↔ 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 ) ) , ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) ) )
21	20	cbviotavw	⊢ ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 ) ) , ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) − 1 ) ) , ( { - π , π , ( ( 𝑦 ∈ ℝ ↦ ( 𝑦 + ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑋 ) } ∪ ( ( - π [,] π ) ∖ dom 𝐺 ) ) ) )
22	1 2 3 4 5 6 7 8 9 10 17 18 19 21	fourierdlem102	⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) lim_ℂ 𝑋 ) ≠ ∅ ∧ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) lim_ℂ 𝑋 ) ≠ ∅ ) )

Metamath Proof Explorer

Theorem fourierdlem106

Proof