This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dirkerf

Description: For any natural number N , the Dirichlet Kernel ( DN ) is a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis dirkerf.1 ⊢ D = n ∈ ℕ ⟼ y ∈ ℝ ⟼ if y mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2
Assertion dirkerf ⊢ N ∈ ℕ → D ⁡ N : ℝ ⟶ ℝ

Proof

Step Hyp Ref Expression
1 dirkerf.1 ⊢ D = n ∈ ℕ ⟼ y ∈ ℝ ⟼ if y mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2
2 1 dirkerval2 ⊢ N ∈ ℕ ∧ y ∈ ℝ → D ⁡ N ⁡ y = if y mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2
3 1 dirkerre ⊢ N ∈ ℕ ∧ y ∈ ℝ → D ⁡ N ⁡ y ∈ ℝ
4 2 3 eqeltrrd ⊢ N ∈ ℕ ∧ y ∈ ℝ → if y mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2 ∈ ℝ
5 4 fmpttd ⊢ N ∈ ℕ → y ∈ ℝ ⟼ if y mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2 : ℝ ⟶ ℝ
6 1 dirkerval ⊢ N ∈ ℕ → D ⁡ N = y ∈ ℝ ⟼ if y mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2
7 6 feq1d ⊢ N ∈ ℕ → D ⁡ N : ℝ ⟶ ℝ ↔ y ∈ ℝ ⟼ if y mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ y 2 ⁢ π ⁢ sin ⁡ y 2 : ℝ ⟶ ℝ
8 5 7 mpbird ⊢ N ∈ ℕ → D ⁡ N : ℝ ⟶ ℝ