Metamath Proof Explorer

Theorem dirkerval2

Description: The N_th Dirichlet Kernel evaluated at a specific point S . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis dirkerval2.1 ⊢ D = n ∈ ℕ ⟼ s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
Assertion dirkerval2 ⊢ N ∈ ℕ ∧ S ∈ ℝ → 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 dirkerval2.1 ⊢ D = n ∈ ℕ ⟼ s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
2 1 dirkerval ⊢ N ∈ ℕ → D ⁡ N = s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
3 oveq1 ⊢ s = t → s mod 2 ⁢ π = t mod 2 ⁢ π
4 3 eqeq1d ⊢ s = t → s mod 2 ⁢ π = 0 ↔ t mod 2 ⁢ π = 0
5 oveq2 ⊢ s = t → N + 1 2 ⁢ s = N + 1 2 ⁢ t
6 5 fveq2d ⊢ s = t → sin ⁡ N + 1 2 ⁢ s = sin ⁡ N + 1 2 ⁢ t
7 fvoveq1 ⊢ s = t → sin ⁡ s 2 = sin ⁡ t 2
8 7 oveq2d ⊢ s = t → 2 ⁢ π ⁢ sin ⁡ s 2 = 2 ⁢ π ⁢ sin ⁡ t 2
9 6 8 oveq12d ⊢ s = t → sin ⁡ N + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 = sin ⁡ N + 1 2 ⁢ t 2 ⁢ π ⁢ sin ⁡ t 2
10 4 9 ifbieq2d ⊢ s = t → if s mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 = if t mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ t 2 ⁢ π ⁢ sin ⁡ t 2
11 10 cbvmptv ⊢ s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2 = t ∈ ℝ ⟼ if t mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ t 2 ⁢ π ⁢ sin ⁡ t 2
12 2 11 eqtrdi ⊢ N ∈ ℕ → D ⁡ N = t ∈ ℝ ⟼ if t mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ t 2 ⁢ π ⁢ sin ⁡ t 2
13 12 adantr ⊢ N ∈ ℕ ∧ S ∈ ℝ → D ⁡ N = t ∈ ℝ ⟼ if t mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ t 2 ⁢ π ⁢ sin ⁡ t 2
14 simpr ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ t = S → t = S
15 14 oveq1d ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ t = S → t mod 2 ⁢ π = S mod 2 ⁢ π
16 15 eqeq1d ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ t = S → t mod 2 ⁢ π = 0 ↔ S mod 2 ⁢ π = 0
17 14 oveq2d ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ t = S → N + 1 2 ⁢ t = N + 1 2 ⁢ S
18 17 fveq2d ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ t = S → sin ⁡ N + 1 2 ⁢ t = sin ⁡ N + 1 2 ⁢ S
19 14 fvoveq1d ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ t = S → sin ⁡ t 2 = sin ⁡ S 2
20 19 oveq2d ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ t = S → 2 ⁢ π ⁢ sin ⁡ t 2 = 2 ⁢ π ⁢ sin ⁡ S 2
21 18 20 oveq12d ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ t = S → sin ⁡ N + 1 2 ⁢ t 2 ⁢ π ⁢ sin ⁡ t 2 = sin ⁡ N + 1 2 ⁢ S 2 ⁢ π ⁢ sin ⁡ S 2
22 16 21 ifbieq2d ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ t = S → if t mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ t 2 ⁢ π ⁢ sin ⁡ t 2 = if S mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ S 2 ⁢ π ⁢ sin ⁡ S 2
23 simpr ⊢ N ∈ ℕ ∧ S ∈ ℝ → S ∈ ℝ
24 2re ⊢ 2 ∈ ℝ
25 24 a1i ⊢ N ∈ ℕ → 2 ∈ ℝ
26 nnre ⊢ N ∈ ℕ → N ∈ ℝ
27 25 26 remulcld ⊢ N ∈ ℕ → 2 ⋅ N ∈ ℝ
28 1red ⊢ N ∈ ℕ → 1 ∈ ℝ
29 27 28 readdcld ⊢ N ∈ ℕ → 2 ⋅ N + 1 ∈ ℝ
30 pire ⊢ π ∈ ℝ
31 30 a1i ⊢ N ∈ ℕ → π ∈ ℝ
32 25 31 remulcld ⊢ N ∈ ℕ → 2 ⁢ π ∈ ℝ
33 2cnd ⊢ N ∈ ℕ → 2 ∈ ℂ
34 31 recnd ⊢ N ∈ ℕ → π ∈ ℂ
35 2pos ⊢ 0 < 2
36 35 a1i ⊢ N ∈ ℕ → 0 < 2
37 36 gt0ne0d ⊢ N ∈ ℕ → 2 ≠ 0
38 pipos ⊢ 0 < π
39 38 a1i ⊢ N ∈ ℕ → 0 < π
40 39 gt0ne0d ⊢ N ∈ ℕ → π ≠ 0
41 33 34 37 40 mulne0d ⊢ N ∈ ℕ → 2 ⁢ π ≠ 0
42 29 32 41 redivcld ⊢ N ∈ ℕ → 2 ⋅ N + 1 2 ⁢ π ∈ ℝ
43 42 ad2antrr ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ S mod 2 ⁢ π = 0 → 2 ⋅ N + 1 2 ⁢ π ∈ ℝ
44 dirker2re ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ ¬ S mod 2 ⁢ π = 0 → sin ⁡ N + 1 2 ⁢ S 2 ⁢ π ⁢ sin ⁡ S 2 ∈ ℝ
45 43 44 ifclda ⊢ N ∈ ℕ ∧ S ∈ ℝ → if S mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ S 2 ⁢ π ⁢ sin ⁡ S 2 ∈ ℝ
46 13 22 23 45 fvmptd ⊢ N ∈ ℕ ∧ S ∈ ℝ → D ⁡ N ⁡ S = if S mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ S 2 ⁢ π ⁢ sin ⁡ S 2