Metamath Proof Explorer

Theorem dirker2re

Description: The Dirchlet Kernel value is a real if the argument is not a multiple of π . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion dirker2re ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
2 1 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → 𝑁 ∈ ℝ )
3 1red ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → 1 ∈ ℝ )
4 3 rehalfcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( 1 / 2 ) ∈ ℝ )
5 2 4 readdcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ )
6 simplr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → 𝑆 ∈ ℝ )
7 5 6 remulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ∈ ℝ )
8 7 resincld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) ∈ ℝ )
9 2re ⊢ 2 ∈ ℝ
10 9 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → 2 ∈ ℝ )
11 pire ⊢ π ∈ ℝ
12 11 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → π ∈ ℝ )
13 10 12 remulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( 2 · π ) ∈ ℝ )
14 6 rehalfcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( 𝑆 / 2 ) ∈ ℝ )
15 14 resincld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( sin ‘ ( 𝑆 / 2 ) ) ∈ ℝ )
16 13 15 remulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ∈ ℝ )
17 2cnd ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → 2 ∈ ℂ )
18 picn ⊢ π ∈ ℂ
19 18 a1i ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → π ∈ ℂ )
20 17 19 mulcld ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( 2 · π ) ∈ ℂ )
21 recn ⊢ ( 𝑆 ∈ ℝ → 𝑆 ∈ ℂ )
22 21 adantr ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → 𝑆 ∈ ℂ )
23 22 halfcld ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( 𝑆 / 2 ) ∈ ℂ )
24 23 sincld ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( sin ‘ ( 𝑆 / 2 ) ) ∈ ℂ )
25 2ne0 ⊢ 2 ≠ 0
26 25 a1i ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → 2 ≠ 0 )
27 0re ⊢ 0 ∈ ℝ
28 pipos ⊢ 0 < π
29 27 28 gtneii ⊢ π ≠ 0
30 29 a1i ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → π ≠ 0 )
31 17 19 26 30 mulne0d ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( 2 · π ) ≠ 0 )
32 22 17 19 26 30 divdiv1d ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( 𝑆 / 2 ) / π ) = ( 𝑆 / ( 2 · π ) ) )
33 simpr ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ¬ ( 𝑆 mod ( 2 · π ) ) = 0 )
34 2rp ⊢ 2 ∈ ℝ+
35 pirp ⊢ π ∈ ℝ+
36 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ )
37 34 35 36 mp2an ⊢ ( 2 · π ) ∈ ℝ+
38 mod0 ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ) → ( ( 𝑆 mod ( 2 · π ) ) = 0 ↔ ( 𝑆 / ( 2 · π ) ) ∈ ℤ ) )
39 37 38 mpan2 ⊢ ( 𝑆 ∈ ℝ → ( ( 𝑆 mod ( 2 · π ) ) = 0 ↔ ( 𝑆 / ( 2 · π ) ) ∈ ℤ ) )
40 39 adantr ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( 𝑆 mod ( 2 · π ) ) = 0 ↔ ( 𝑆 / ( 2 · π ) ) ∈ ℤ ) )
41 33 40 mtbid ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ¬ ( 𝑆 / ( 2 · π ) ) ∈ ℤ )
42 32 41 eqneltrd ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ¬ ( ( 𝑆 / 2 ) / π ) ∈ ℤ )
43 sineq0 ⊢ ( ( 𝑆 / 2 ) ∈ ℂ → ( ( sin ‘ ( 𝑆 / 2 ) ) = 0 ↔ ( ( 𝑆 / 2 ) / π ) ∈ ℤ ) )
44 23 43 syl ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( sin ‘ ( 𝑆 / 2 ) ) = 0 ↔ ( ( 𝑆 / 2 ) / π ) ∈ ℤ ) )
45 42 44 mtbird ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ¬ ( sin ‘ ( 𝑆 / 2 ) ) = 0 )
46 45 neqned ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( sin ‘ ( 𝑆 / 2 ) ) ≠ 0 )
47 20 24 31 46 mulne0d ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ≠ 0 )
48 47 adantll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ≠ 0 )
49 8 16 48 redivcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ℝ ) ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑆 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ) ∈ ℝ )