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 ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
Assertion dirkerf ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 dirkerf.1 ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
2 1 dirkerval2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑦 ) = if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) )
3 1 dirkerre ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑦 ) ∈ ℝ )
4 2 3 eqeltrrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℝ ) → if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ∈ ℝ )
5 4 fmpttd ⊢ ( 𝑁 ∈ ℕ → ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) : ℝ ⟶ ℝ )
6 1 dirkerval ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) = ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
7 6 feq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ ↔ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) : ℝ ⟶ ℝ ) )
8 5 7 mpbird ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ )