Metamath Proof Explorer

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 ⊢ D = n ∈ ℕ ⟼ s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
Assertion dirkerre ⊢ N ∈ ℕ ∧ S ∈ ℝ → D ⁡ N ⁡ S ∈ ℝ

Proof

Step Hyp Ref Expression
1 dirkerre.1 ⊢ D = n ∈ ℕ ⟼ s ∈ ℝ ⟼ if s mod 2 ⁢ π = 0 2 ⁢ n + 1 2 ⁢ π sin ⁡ n + 1 2 ⁢ s 2 ⁢ π ⁢ sin ⁡ s 2
2 1 dirkerval2 ⊢ N ∈ ℕ ∧ S ∈ ℝ → D ⁡ N ⁡ S = if S mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ S 2 ⁢ π ⁢ sin ⁡ S 2
3 2re ⊢ 2 ∈ ℝ
4 3 a1i ⊢ N ∈ ℕ → 2 ∈ ℝ
5 nnre ⊢ N ∈ ℕ → N ∈ ℝ
6 4 5 remulcld ⊢ N ∈ ℕ → 2 ⋅ N ∈ ℝ
7 1red ⊢ N ∈ ℕ → 1 ∈ ℝ
8 6 7 readdcld ⊢ N ∈ ℕ → 2 ⋅ N + 1 ∈ ℝ
9 pire ⊢ π ∈ ℝ
10 9 a1i ⊢ N ∈ ℕ → π ∈ ℝ
11 4 10 remulcld ⊢ N ∈ ℕ → 2 ⁢ π ∈ ℝ
12 2cnd ⊢ N ∈ ℕ → 2 ∈ ℂ
13 10 recnd ⊢ N ∈ ℕ → π ∈ ℂ
14 2ne0 ⊢ 2 ≠ 0
15 14 a1i ⊢ N ∈ ℕ → 2 ≠ 0
16 0re ⊢ 0 ∈ ℝ
17 pipos ⊢ 0 < π
18 16 17 gtneii ⊢ π ≠ 0
19 18 a1i ⊢ N ∈ ℕ → π ≠ 0
20 12 13 15 19 mulne0d ⊢ N ∈ ℕ → 2 ⁢ π ≠ 0
21 8 11 20 redivcld ⊢ N ∈ ℕ → 2 ⋅ N + 1 2 ⁢ π ∈ ℝ
22 21 ad2antrr ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ S mod 2 ⁢ π = 0 → 2 ⋅ N + 1 2 ⁢ π ∈ ℝ
23 dirker2re ⊢ N ∈ ℕ ∧ S ∈ ℝ ∧ ¬ S mod 2 ⁢ π = 0 → sin ⁡ N + 1 2 ⁢ S 2 ⁢ π ⁢ sin ⁡ S 2 ∈ ℝ
24 22 23 ifclda ⊢ N ∈ ℕ ∧ S ∈ ℝ → if S mod 2 ⁢ π = 0 2 ⋅ N + 1 2 ⁢ π sin ⁡ N + 1 2 ⁢ S 2 ⁢ π ⁢ sin ⁡ S 2 ∈ ℝ
25 2 24 eqeltrd ⊢ N ∈ ℕ ∧ S ∈ ℝ → D ⁡ N ⁡ S ∈ ℝ