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 |
⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) : ℝ ⟶ ℝ ) |