Metamath Proof Explorer

Theorem dirkerdenne0

Description: The Dirichlet kernel denominator is never 0 . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion dirkerdenne0 ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 2cnd ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → 2 ∈ ℂ )
2 picn ⊢ π ∈ ℂ
3 2 a1i ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → π ∈ ℂ )
4 1 3 mulcld ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( 2 · π ) ∈ ℂ )
5 recn ⊢ ( 𝑆 ∈ ℝ → 𝑆 ∈ ℂ )
6 5 adantr ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → 𝑆 ∈ ℂ )
7 6 halfcld ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( 𝑆 / 2 ) ∈ ℂ )
8 7 sincld ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( sin ‘ ( 𝑆 / 2 ) ) ∈ ℂ )
9 2ne0 ⊢ 2 ≠ 0
10 9 a1i ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → 2 ≠ 0 )
11 0re ⊢ 0 ∈ ℝ
12 pipos ⊢ 0 < π
13 11 12 gtneii ⊢ π ≠ 0
14 13 a1i ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → π ≠ 0 )
15 1 3 10 14 mulne0d ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( 2 · π ) ≠ 0 )
16 6 1 3 10 14 divdiv1d ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( 𝑆 / 2 ) / π ) = ( 𝑆 / ( 2 · π ) ) )
17 simpr ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ¬ ( 𝑆 mod ( 2 · π ) ) = 0 )
18 2rp ⊢ 2 ∈ ℝ+
19 pirp ⊢ π ∈ ℝ+
20 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ )
21 18 19 20 mp2an ⊢ ( 2 · π ) ∈ ℝ+
22 mod0 ⊢ ( ( 𝑆 ∈ ℝ ∧ ( 2 · π ) ∈ ℝ+ ) → ( ( 𝑆 mod ( 2 · π ) ) = 0 ↔ ( 𝑆 / ( 2 · π ) ) ∈ ℤ ) )
23 21 22 mpan2 ⊢ ( 𝑆 ∈ ℝ → ( ( 𝑆 mod ( 2 · π ) ) = 0 ↔ ( 𝑆 / ( 2 · π ) ) ∈ ℤ ) )
24 23 adantr ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( 𝑆 mod ( 2 · π ) ) = 0 ↔ ( 𝑆 / ( 2 · π ) ) ∈ ℤ ) )
25 17 24 mtbid ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ¬ ( 𝑆 / ( 2 · π ) ) ∈ ℤ )
26 16 25 eqneltrd ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ¬ ( ( 𝑆 / 2 ) / π ) ∈ ℤ )
27 sineq0 ⊢ ( ( 𝑆 / 2 ) ∈ ℂ → ( ( sin ‘ ( 𝑆 / 2 ) ) = 0 ↔ ( ( 𝑆 / 2 ) / π ) ∈ ℤ ) )
28 7 27 syl ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( sin ‘ ( 𝑆 / 2 ) ) = 0 ↔ ( ( 𝑆 / 2 ) / π ) ∈ ℤ ) )
29 26 28 mtbird ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ¬ ( sin ‘ ( 𝑆 / 2 ) ) = 0 )
30 29 neqned ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( sin ‘ ( 𝑆 / 2 ) ) ≠ 0 )
31 4 8 15 30 mulne0d ⊢ ( ( 𝑆 ∈ ℝ ∧ ¬ ( 𝑆 mod ( 2 · π ) ) = 0 ) → ( ( 2 · π ) · ( sin ‘ ( 𝑆 / 2 ) ) ) ≠ 0 )