Metamath Proof Explorer

Theorem dirkerval

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

Ref Expression
Hypothesis dirkerval.1 ⊢D=n∈ℕ⟼s∈ℝ⟼ifsmod2⁢π=02⁢n+12⁢πsin⁡n+12⁢s2⁢π⁢sin⁡s2
Assertion dirkerval ⊢N∈ℕ→D⁡N=s∈ℝ⟼ifsmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢s2⁢π⁢sin⁡s2

Proof

Step Hyp Ref Expression
1 dirkerval.1 ⊢D=n∈ℕ⟼s∈ℝ⟼ifsmod2⁢π=02⁢n+12⁢πsin⁡n+12⁢s2⁢π⁢sin⁡s2
2 simpl ⊢m=N∧s∈ℝ→m=N
3 2 oveq2d ⊢m=N∧s∈ℝ→2⁢m=2⋅ N
4 3 oveq1d ⊢m=N∧s∈ℝ→2⁢m+1=2⋅ N+1
5 4 oveq1d ⊢m=N∧s∈ℝ→2⁢m+12⁢π=2⋅ N+12⁢π
6 2 oveq1d ⊢m=N∧s∈ℝ→m+12=N+12
7 6 fvoveq1d ⊢m=N∧s∈ℝ→sin⁡m+12⁢s=sin⁡N+12⁢s
8 7 oveq1d ⊢m=N∧s∈ℝ→sin⁡m+12⁢s2⁢π⁢sin⁡s2=sin⁡N+12⁢s2⁢π⁢sin⁡s2
9 5 8 ifeq12d ⊢m=N∧s∈ℝ→ifsmod2⁢π=02⁢m+12⁢πsin⁡m+12⁢s2⁢π⁢sin⁡s2=ifsmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢s2⁢π⁢sin⁡s2
10 9 mpteq2dva ⊢m=N→s∈ℝ⟼ifsmod2⁢π=02⁢m+12⁢πsin⁡m+12⁢s2⁢π⁢sin⁡s2=s∈ℝ⟼ifsmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢s2⁢π⁢sin⁡s2
11 simpl ⊢n=m∧s∈ℝ→n=m
12 11 oveq2d ⊢n=m∧s∈ℝ→2⁢n=2⁢m
13 12 oveq1d ⊢n=m∧s∈ℝ→2⁢n+1=2⁢m+1
14 13 oveq1d ⊢n=m∧s∈ℝ→2⁢n+12⁢π=2⁢m+12⁢π
15 11 oveq1d ⊢n=m∧s∈ℝ→n+12=m+12
16 15 fvoveq1d ⊢n=m∧s∈ℝ→sin⁡n+12⁢s=sin⁡m+12⁢s
17 16 oveq1d ⊢n=m∧s∈ℝ→sin⁡n+12⁢s2⁢π⁢sin⁡s2=sin⁡m+12⁢s2⁢π⁢sin⁡s2
18 14 17 ifeq12d ⊢n=m∧s∈ℝ→ifsmod2⁢π=02⁢n+12⁢πsin⁡n+12⁢s2⁢π⁢sin⁡s2=ifsmod2⁢π=02⁢m+12⁢πsin⁡m+12⁢s2⁢π⁢sin⁡s2
19 18 mpteq2dva ⊢n=m→s∈ℝ⟼ifsmod2⁢π=02⁢n+12⁢πsin⁡n+12⁢s2⁢π⁢sin⁡s2=s∈ℝ⟼ifsmod2⁢π=02⁢m+12⁢πsin⁡m+12⁢s2⁢π⁢sin⁡s2
20 19 cbvmptv ⊢n∈ℕ⟼s∈ℝ⟼ifsmod2⁢π=02⁢n+12⁢πsin⁡n+12⁢s2⁢π⁢sin⁡s2=m∈ℕ⟼s∈ℝ⟼ifsmod2⁢π=02⁢m+12⁢πsin⁡m+12⁢s2⁢π⁢sin⁡s2
21 1 20 eqtri ⊢D=m∈ℕ⟼s∈ℝ⟼ifsmod2⁢π=02⁢m+12⁢πsin⁡m+12⁢s2⁢π⁢sin⁡s2
22 reex ⊢ℝ∈V
23 22 mptex ⊢s∈ℝ⟼ifsmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢s2⁢π⁢sin⁡s2∈V
24 10 21 23 fvmpt ⊢N∈ℕ→D⁡N=s∈ℝ⟼ifsmod2⁢π=02⋅ N+12⁢πsin⁡N+12⁢s2⁢π⁢sin⁡s2