Theorem dirkerre

Description: The Dirichlet kernel at any point evaluates to a real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dirkerre.1	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑠 ∈ ℝ ↦ if ( ( 𝑠 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑠 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
2	1	dirkerval2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑆 ) = if ( ( 𝑆 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ) ) )
3		2re	⊢ 2 ∈ ℝ
4	3	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
5		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
6	4 5	remulcld	⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ )
7		1red	⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
8	6 7	readdcld	⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℝ )
9		pire	⊢ π ∈ ℝ
10	9	a1i	⊢ ( 𝑁 ∈ ℕ → π ∈ ℝ )
11	4 10	remulcld	⊢ ( 𝑁 ∈ ℕ → ( 2 · π ) ∈ ℝ )
12		2cnd	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
13	10	recnd	⊢ ( 𝑁 ∈ ℕ → π ∈ ℂ )
14		2ne0	⊢ 2 ≠ 0
15	14	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
16		0re	⊢ 0 ∈ ℝ
17		pipos	⊢ 0 < π
18	16 17	gtneii	⊢ π ≠ 0
19	18	a1i	⊢ ( 𝑁 ∈ ℕ → π ≠ 0 )
20	12 13 15 19	mulne0d	⊢ ( 𝑁 ∈ ℕ → ( 2 · π ) ≠ 0 )
21	8 11 20	redivcld	⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) ∈ ℝ )
22	21	ad2antrr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) ∈ ℝ )
23		dirker2re	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ) ∈ ℝ )
24	22 23	ifclda	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) → if ( ( 𝑆 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑁 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ) ) ∈ ℝ )
25	2 24	eqeltrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑆 ) ∈ ℝ )