Metamath Proof Explorer

Theorem dirkerval

Description: The N_th Dirichlet Kernel. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis dirkerval.1 ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
Assertion dirkerval ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dirkerval.1 ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
2 simpl ⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → 𝑚 = 𝑁 )
3 2 oveq2d ⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( 2 · 𝑚 ) = ( 2 · 𝑁 ) )
4 3 oveq1d ⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( ( 2 · 𝑚 ) + 1 ) = ( ( 2 · 𝑁 ) + 1 ) )
5 4 oveq1d ⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
6 2 oveq1d ⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( 𝑚 + ( 1 / 2 ) ) = ( 𝑁 + ( 1 / 2 ) ) )
7 6 fvoveq1d ⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
8 7 oveq1d ⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
9 5 8 ifeq12d ⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
10 9 mpteq2dva ⊢ ( 𝑚 = 𝑁 → ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
11 simpl ⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → 𝑛 = 𝑚 )
12 11 oveq2d ⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( 2 · 𝑛 ) = ( 2 · 𝑚 ) )
13 12 oveq1d ⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑚 ) + 1 ) )
14 13 oveq1d ⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) = ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) )
15 11 oveq1d ⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( 𝑛 + ( 1 / 2 ) ) = ( 𝑚 + ( 1 / 2 ) ) )
16 15 fvoveq1d ⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) = ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) )
17 16 oveq1d ⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
18 14 17 ifeq12d ⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
19 18 mpteq2dva ⊢ ( 𝑛 = 𝑚 → ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
20 19 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
21 1 20 eqtri ⊢ 𝐷 = ( 𝑚 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
22 reex ⊢ ℝ ∈ V
23 22 mptex ⊢ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ∈ V
24 10 21 23 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )