Theorem dirkerval

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

	Ref	Expression
Hypothesis	dirkerval.1	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
Assertion	dirkerval	⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dirkerval.1	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
2		simpl	⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → 𝑚 = 𝑁 )
3	2	oveq2d	⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( 2 · 𝑚 ) = ( 2 · 𝑁 ) )
4	3	oveq1d	⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( ( 2 · 𝑚 ) + 1 ) = ( ( 2 · 𝑁 ) + 1 ) )
5	4	oveq1d	⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) = ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) )
6	2	oveq1d	⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( 𝑚 + ( 1 / 2 ) ) = ( 𝑁 + ( 1 / 2 ) ) )
7	6	fvoveq1d	⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
8	7	oveq1d	⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
9	5 8	ifeq12d	⊢ ( ( 𝑚 = 𝑁 ∧ 𝑠 ∈ ℝ ) → 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 ) ) ) ) ) )
10	9	mpteq2dva	⊢ ( 𝑚 = 𝑁 → ( 𝑠 ∈ ℝ ↦ 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		simpl	⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → 𝑛 = 𝑚 )
12	11	oveq2d	⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( 2 · 𝑛 ) = ( 2 · 𝑚 ) )
13	12	oveq1d	⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑚 ) + 1 ) )
14	13	oveq1d	⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) = ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) )
15	11	oveq1d	⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( 𝑛 + ( 1 / 2 ) ) = ( 𝑚 + ( 1 / 2 ) ) )
16	15	fvoveq1d	⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) = ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) )
17	16	oveq1d	⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
18	14 17	ifeq12d	⊢ ( ( 𝑛 = 𝑚 ∧ 𝑠 ∈ ℝ ) → 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 ) ) ) ) ) )
19	18	mpteq2dva	⊢ ( 𝑛 = 𝑚 → ( 𝑠 ∈ ℝ ↦ 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 ) ) ) ) ) ) )
20	19	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 ) ) ) ) ) ) )
21	1 20	eqtri	⊢ 𝐷 = ( 𝑚 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑚 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑚 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
22		reex	⊢ ℝ ∈ V
23	22	mptex	⊢ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ∈ V
24	10 21 23	fvmpt	⊢ ( 𝑁 ∈ ℕ → ( 𝐷 ‘ 𝑁 ) = ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )