This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
Assertion dirkerval2 ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑆 ) = if ( ( 𝑆 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dirkerval2.1 ⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
2 1 dirkerval ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
3 oveq1 ⊢ ( 𝑠 = 𝑡 → ( 𝑠 mod ( 2 · π ) ) = ( 𝑡 mod ( 2 · π ) ) )
4 3 eqeq1d ⊢ ( 𝑠 = 𝑡 → ( ( 𝑠 mod ( 2 · π ) ) = 0 ↔ ( 𝑡 mod ( 2 · π ) ) = 0 ) )
5 oveq2 ⊢ ( 𝑠 = 𝑡 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑡 ) )
6 5 fveq2d ⊢ ( 𝑠 = 𝑡 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑡 ) ) )
7 fvoveq1 ⊢ ( 𝑠 = 𝑡 → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( 𝑡 / 2 ) ) )
8 7 oveq2d ⊢ ( 𝑠 = 𝑡 → ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑡 / 2 ) ) ) )
9 6 8 oveq12d ⊢ ( 𝑠 = 𝑡 → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑡 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑡 / 2 ) ) ) ) )
10 4 9 ifbieq2d ⊢ ( 𝑠 = 𝑡 → 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 10 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 ) ) ) ) ) )
12 2 11 eqtrdi ⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) = ( 𝑡 ∈ ℝ ↦ if ( ( 𝑡 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑡 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) )
13 12 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) → ( 𝐷 ‘ 𝑁 ) = ( 𝑡 ∈ ℝ ↦ if ( ( 𝑡 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑡 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑡 / 2 ) ) ) ) ) ) )
14 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ 𝑡 = 𝑆 ) → 𝑡 = 𝑆 )
15 14 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ 𝑡 = 𝑆 ) → ( 𝑡 mod ( 2 · π ) ) = ( 𝑆 mod ( 2 · π ) ) )
16 15 eqeq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ 𝑡 = 𝑆 ) → ( ( 𝑡 mod ( 2 · π ) ) = 0 ↔ ( 𝑆 mod ( 2 · π ) ) = 0 ) )
17 14 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ 𝑡 = 𝑆 ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑡 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) )
18 17 fveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ 𝑡 = 𝑆 ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑡 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) )
19 14 fvoveq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ 𝑡 = 𝑆 ) → ( sin ‘ ( 𝑡 / 2 ) ) = ( sin ‘ ( 𝑆 / 2 ) ) )
20 19 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ 𝑡 = 𝑆 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑡 / 2 ) ) ) = ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) )
21 18 20 oveq12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ 𝑡 = 𝑆 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑡 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑡 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ) )
22 16 21 ifbieq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ 𝑡 = 𝑆 ) → 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 ) ) ) ) ) )
23 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) → 𝑆 ∈ ℝ )
24 2re ⊢ 2 ∈ ℝ
25 24 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
26 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
27 25 26 remulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ )
28 1red ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
29 27 28 readdcld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
30 pire ⊢ π ∈ ℝ
31 30 a1i ⊢ ( 𝑁 ∈ ℕ → π ∈ ℝ )
32 25 31 remulcld ⊢ ( 𝑁 ∈ ℕ → ( 2 · π ) ∈ ℝ )
33 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
34 31 recnd ⊢ ( 𝑁 ∈ ℕ → π ∈ ℂ )
35 2pos ⊢ 0 < 2
36 35 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < 2 )
37 36 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
38 pipos ⊢ 0 < π
39 38 a1i ⊢ ( 𝑁 ∈ ℕ → 0 < π )
40 39 gt0ne0d ⊢ ( 𝑁 ∈ ℕ → π ≠ 0 )
41 33 34 37 40 mulne0d ⊢ ( 𝑁 ∈ ℕ → ( 2 · π ) ≠ 0 )
42 29 32 41 redivcld ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) ∈ ℝ )
43 42 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) ∈ ℝ )
44 dirker2re ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ) ∈ ℝ )
45 43 44 ifclda ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) → if ( ( 𝑆 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ) ) ∈ ℝ )
46 13 22 23 45 fvmptd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑆 ) = if ( ( 𝑆 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ) ) )