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

Proof

Step Hyp Ref Expression
1 dirkerre.1 
 |-  D = ( n e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
2 1 dirkerval2 
 |-  ( ( N e. NN /\ S e. RR ) -> ( ( D ` N ) ` S ) = if ( ( S mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. S ) ) / ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) ) ) )
3 2re 
 |-  2 e. RR
4 3 a1i 
 |-  ( N e. NN -> 2 e. RR )
5 nnre 
 |-  ( N e. NN -> N e. RR )
6 4 5 remulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. RR )
7 1red 
 |-  ( N e. NN -> 1 e. RR )
8 6 7 readdcld 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. RR )
9 pire 
 |-  _pi e. RR
10 9 a1i 
 |-  ( N e. NN -> _pi e. RR )
11 4 10 remulcld 
 |-  ( N e. NN -> ( 2 x. _pi ) e. RR )
12 2cnd 
 |-  ( N e. NN -> 2 e. CC )
13 10 recnd 
 |-  ( N e. NN -> _pi e. CC )
14 2ne0 
 |-  2 =/= 0
15 14 a1i 
 |-  ( N e. NN -> 2 =/= 0 )
16 0re 
 |-  0 e. RR
17 pipos 
 |-  0 < _pi
18 16 17 gtneii 
 |-  _pi =/= 0
19 18 a1i 
 |-  ( N e. NN -> _pi =/= 0 )
20 12 13 15 19 mulne0d 
 |-  ( N e. NN -> ( 2 x. _pi ) =/= 0 )
21 8 11 20 redivcld 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) e. RR )
22 21 ad2antrr 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) e. RR )
23 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 )
24 22 23 ifclda 
 |-  ( ( N e. NN /\ S e. RR ) -> if ( ( S mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. S ) ) / ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) ) ) e. RR )
25 2 24 eqeltrd 
 |-  ( ( N e. NN /\ S e. RR ) -> ( ( D ` N ) ` S ) e. RR )