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 ) ) ) ) ) )