Metamath Proof Explorer

Theorem dirkerdenne0

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

Ref Expression
Assertion dirkerdenne0 
|- ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) =/= 0 )

Proof

Step Hyp Ref Expression
1 2cnd 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> 2 e. CC )
2 picn 
 |-  _pi e. CC
3 2 a1i 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> _pi e. CC )
4 1 3 mulcld 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( 2 x. _pi ) e. CC )
5 recn 
 |-  ( S e. RR -> S e. CC )
6 5 adantr 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> S e. CC )
7 6 halfcld 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( S / 2 ) e. CC )
8 7 sincld 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( sin ` ( S / 2 ) ) e. CC )
9 2ne0 
 |-  2 =/= 0
10 9 a1i 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> 2 =/= 0 )
11 0re 
 |-  0 e. RR
12 pipos 
 |-  0 < _pi
13 11 12 gtneii 
 |-  _pi =/= 0
14 13 a1i 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> _pi =/= 0 )
15 1 3 10 14 mulne0d 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( 2 x. _pi ) =/= 0 )
16 6 1 3 10 14 divdiv1d 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( S / 2 ) / _pi ) = ( S / ( 2 x. _pi ) ) )
17 simpr 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> -. ( S mod ( 2 x. _pi ) ) = 0 )
18 2rp 
 |-  2 e. RR+
19 pirp 
 |-  _pi e. RR+
20 rpmulcl 
 |-  ( ( 2 e. RR+ /\ _pi e. RR+ ) -> ( 2 x. _pi ) e. RR+ )
21 18 19 20 mp2an 
 |-  ( 2 x. _pi ) e. RR+
22 mod0 
 |-  ( ( S e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( S mod ( 2 x. _pi ) ) = 0 <-> ( S / ( 2 x. _pi ) ) e. ZZ ) )
23 21 22 mpan2 
 |-  ( S e. RR -> ( ( S mod ( 2 x. _pi ) ) = 0 <-> ( S / ( 2 x. _pi ) ) e. ZZ ) )
24 23 adantr 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( S mod ( 2 x. _pi ) ) = 0 <-> ( S / ( 2 x. _pi ) ) e. ZZ ) )
25 17 24 mtbid 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> -. ( S / ( 2 x. _pi ) ) e. ZZ )
26 16 25 eqneltrd 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> -. ( ( S / 2 ) / _pi ) e. ZZ )
27 sineq0 
 |-  ( ( S / 2 ) e. CC -> ( ( sin ` ( S / 2 ) ) = 0 <-> ( ( S / 2 ) / _pi ) e. ZZ ) )
28 7 27 syl 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( sin ` ( S / 2 ) ) = 0 <-> ( ( S / 2 ) / _pi ) e. ZZ ) )
29 26 28 mtbird 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> -. ( sin ` ( S / 2 ) ) = 0 )
30 29 neqned 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( sin ` ( S / 2 ) ) =/= 0 )
31 4 8 15 30 mulne0d 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) =/= 0 )