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 )