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 
|- ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. S ) ) / ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) ) e. RR )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( N e. NN -> N e. RR )
2 1 ad2antrr 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> N e. RR )
3 1red 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> 1 e. RR )
4 3 rehalfcld 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( 1 / 2 ) e. RR )
5 2 4 readdcld 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( N + ( 1 / 2 ) ) e. RR )
6 simplr 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> S e. RR )
7 5 6 remulcld 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( N + ( 1 / 2 ) ) x. S ) e. RR )
8 7 resincld 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. S ) ) e. RR )
9 2re 
 |-  2 e. RR
10 9 a1i 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> 2 e. RR )
11 pire 
 |-  _pi e. RR
12 11 a1i 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> _pi e. RR )
13 10 12 remulcld 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( 2 x. _pi ) e. RR )
14 6 rehalfcld 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( S / 2 ) e. RR )
15 14 resincld 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( sin ` ( S / 2 ) ) e. RR )
16 13 15 remulcld 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) e. RR )
17 2cnd 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> 2 e. CC )
18 picn 
 |-  _pi e. CC
19 18 a1i 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> _pi e. CC )
20 17 19 mulcld 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( 2 x. _pi ) e. CC )
21 recn 
 |-  ( S e. RR -> S e. CC )
22 21 adantr 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> S e. CC )
23 22 halfcld 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( S / 2 ) e. CC )
24 23 sincld 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( sin ` ( S / 2 ) ) e. CC )
25 2ne0 
 |-  2 =/= 0
26 25 a1i 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> 2 =/= 0 )
27 0re 
 |-  0 e. RR
28 pipos 
 |-  0 < _pi
29 27 28 gtneii 
 |-  _pi =/= 0
30 29 a1i 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> _pi =/= 0 )
31 17 19 26 30 mulne0d 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( 2 x. _pi ) =/= 0 )
32 22 17 19 26 30 divdiv1d 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( S / 2 ) / _pi ) = ( S / ( 2 x. _pi ) ) )
33 simpr 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> -. ( S mod ( 2 x. _pi ) ) = 0 )
34 2rp 
 |-  2 e. RR+
35 pirp 
 |-  _pi e. RR+
36 rpmulcl 
 |-  ( ( 2 e. RR+ /\ _pi e. RR+ ) -> ( 2 x. _pi ) e. RR+ )
37 34 35 36 mp2an 
 |-  ( 2 x. _pi ) e. RR+
38 mod0 
 |-  ( ( S e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( S mod ( 2 x. _pi ) ) = 0 <-> ( S / ( 2 x. _pi ) ) e. ZZ ) )
39 37 38 mpan2 
 |-  ( S e. RR -> ( ( S mod ( 2 x. _pi ) ) = 0 <-> ( S / ( 2 x. _pi ) ) e. ZZ ) )
40 39 adantr 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( S mod ( 2 x. _pi ) ) = 0 <-> ( S / ( 2 x. _pi ) ) e. ZZ ) )
41 33 40 mtbid 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> -. ( S / ( 2 x. _pi ) ) e. ZZ )
42 32 41 eqneltrd 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> -. ( ( S / 2 ) / _pi ) e. ZZ )
43 sineq0 
 |-  ( ( S / 2 ) e. CC -> ( ( sin ` ( S / 2 ) ) = 0 <-> ( ( S / 2 ) / _pi ) e. ZZ ) )
44 23 43 syl 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( sin ` ( S / 2 ) ) = 0 <-> ( ( S / 2 ) / _pi ) e. ZZ ) )
45 42 44 mtbird 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> -. ( sin ` ( S / 2 ) ) = 0 )
46 45 neqned 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( sin ` ( S / 2 ) ) =/= 0 )
47 20 24 31 46 mulne0d 
 |-  ( ( S e. RR /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) =/= 0 )
48 47 adantll 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) =/= 0 )
49 8 16 48 redivcld 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ -. ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. S ) ) / ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) ) e. RR )