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 ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
Assertion dirkerval ⊢ N ∈ ℕ → D ⁡ N = s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2

Proof

Step Hyp Ref Expression
1 dirkerval.1 ⊢ D = n ∈ ℕ ⟼ s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
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 + 1 2 ⁢ π = 2 ⋅ N + 1 2 ⁢ π
6 2 oveq1d ⊢ m = N ∧ s ∈ ℝ → m + 1 2 = N + 1 2
7 6 fvoveq1d ⊢ m = N ∧ s ∈ ℝ → sin ⁡ m + 1 2 ⁢ s = sin ⁡ N + 1 2 ⁢ s
8 7 oveq1d ⊢ m = N ∧ s ∈ ℝ → sin ⁡ m + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 = sin ⁡ N + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
9 5 8 ifeq12d ⊢ m = N ∧ s ∈ ℝ → if s mod 2 ⁢ π = 0 2 ⁢ m + 1 2 ⁢ π sin ⁡ m + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 = if s mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
10 9 mpteq2dva ⊢ m = N → s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ m + 1 2 ⁢ π sin ⁡ m + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 = s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
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 + 1 2 ⁢ π = 2 ⁢ m + 1 2 ⁢ π
15 11 oveq1d ⊢ n = m ∧ s ∈ ℝ → n + 1 2 = m + 1 2
16 15 fvoveq1d ⊢ n = m ∧ s ∈ ℝ → sin ⁡ n + 1 2 ⁢ s = sin ⁡ m + 1 2 ⁢ s
17 16 oveq1d ⊢ n = m ∧ s ∈ ℝ → sin ⁡ n + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 = sin ⁡ m + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
18 14 17 ifeq12d ⊢ n = m ∧ s ∈ ℝ → if s mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 = if s mod 2 ⁢ π = 0 2 ⁢ m + 1 2 ⁢ π sin ⁡ m + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
19 18 mpteq2dva ⊢ n = m → s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 = s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ m + 1 2 ⁢ π sin ⁡ m + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
20 19 cbvmptv ⊢ n ∈ ℕ ⟼ s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 = m ∈ ℕ ⟼ s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ m + 1 2 ⁢ π sin ⁡ m + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
21 1 20 eqtri ⊢ D = m ∈ ℕ ⟼ s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ m + 1 2 ⁢ π sin ⁡ m + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
22 reex ⊢ ℝ ∈ V
23 22 mptex ⊢ s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 ∈ V
24 10 21 23 fvmpt ⊢ N ∈ ℕ → D ⁡ N = s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2