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 \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
	Assertion	dirkerf	$⊢ N \in ℕ \to D (N) : ℝ ⟶ ℝ$

Step	Hyp	Ref	Expression
1		dirkerf.1	$⊢ D = (n \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
2	1	dirkerval2	$⊢ (N \in ℕ \land y \in ℝ) \to D (N) (y) = if (y \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})$
3	1	dirkerre	$⊢ (N \in ℕ \land y \in ℝ) \to D (N) (y) \in ℝ$
4	2 3	eqeltrrd	$⊢ (N \in ℕ \land y \in ℝ) \to if (y \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}) \in ℝ$
5	4	fmpttd	$⊢ N \in ℕ \to (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})) : ℝ ⟶ ℝ$
6	1	dirkerval	$⊢ N \in ℕ \to D (N) = (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}))$
7	6	feq1d	$⊢ N \in ℕ \to (D (N) : ℝ ⟶ ℝ \leftrightarrow (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 \cdot N + 1}{2 π}, \frac{\sin (N + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})) : ℝ ⟶ ℝ)$
8	5 7	mpbird	$⊢ N \in ℕ \to D (N) : ℝ ⟶ ℝ$

Metamath Proof Explorer