Metamath Proof Explorer

Theorem dirkerval2

Description: The N_th Dirichlet Kernel evaluated at a specific point S . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis dirkerval2.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 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dirkerval2.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 dirkerval 
 |-  ( N e. NN -> ( D ` N ) = ( 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 ) ) ) ) ) ) )
3 oveq1 
 |-  ( s = t -> ( s mod ( 2 x. _pi ) ) = ( t mod ( 2 x. _pi ) ) )
4 3 eqeq1d 
 |-  ( s = t -> ( ( s mod ( 2 x. _pi ) ) = 0 <-> ( t mod ( 2 x. _pi ) ) = 0 ) )
5 oveq2 
 |-  ( s = t -> ( ( N + ( 1 / 2 ) ) x. s ) = ( ( N + ( 1 / 2 ) ) x. t ) )
6 5 fveq2d 
 |-  ( s = t -> ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. t ) ) )
7 fvoveq1 
 |-  ( s = t -> ( sin ` ( s / 2 ) ) = ( sin ` ( t / 2 ) ) )
8 7 oveq2d 
 |-  ( s = t -> ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( t / 2 ) ) ) )
9 6 8 oveq12d 
 |-  ( s = t -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. t ) ) / ( ( 2 x. _pi ) x. ( sin ` ( t / 2 ) ) ) ) )
10 4 9 ifbieq2d 
 |-  ( s = t -> 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 ) ) ) ) ) = if ( ( t mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. t ) ) / ( ( 2 x. _pi ) x. ( sin ` ( t / 2 ) ) ) ) ) )
11 10 cbvmptv 
 |-  ( 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 ) ) ) ) ) ) = ( t e. RR |-> if ( ( t mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. t ) ) / ( ( 2 x. _pi ) x. ( sin ` ( t / 2 ) ) ) ) ) )
12 2 11 eqtrdi 
 |-  ( N e. NN -> ( D ` N ) = ( t e. RR |-> if ( ( t mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. t ) ) / ( ( 2 x. _pi ) x. ( sin ` ( t / 2 ) ) ) ) ) ) )
13 12 adantr 
 |-  ( ( N e. NN /\ S e. RR ) -> ( D ` N ) = ( t e. RR |-> if ( ( t mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. t ) ) / ( ( 2 x. _pi ) x. ( sin ` ( t / 2 ) ) ) ) ) ) )
14 simpr 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ t = S ) -> t = S )
15 14 oveq1d 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ t = S ) -> ( t mod ( 2 x. _pi ) ) = ( S mod ( 2 x. _pi ) ) )
16 15 eqeq1d 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ t = S ) -> ( ( t mod ( 2 x. _pi ) ) = 0 <-> ( S mod ( 2 x. _pi ) ) = 0 ) )
17 14 oveq2d 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ t = S ) -> ( ( N + ( 1 / 2 ) ) x. t ) = ( ( N + ( 1 / 2 ) ) x. S ) )
18 17 fveq2d 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ t = S ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. t ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. S ) ) )
19 14 fvoveq1d 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ t = S ) -> ( sin ` ( t / 2 ) ) = ( sin ` ( S / 2 ) ) )
20 19 oveq2d 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ t = S ) -> ( ( 2 x. _pi ) x. ( sin ` ( t / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) )
21 18 20 oveq12d 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ t = S ) -> ( ( sin ` ( ( N + ( 1 / 2 ) ) x. t ) ) / ( ( 2 x. _pi ) x. ( sin ` ( t / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. S ) ) / ( ( 2 x. _pi ) x. ( sin ` ( S / 2 ) ) ) ) )
22 16 21 ifbieq2d 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ t = S ) -> if ( ( t mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. t ) ) / ( ( 2 x. _pi ) x. ( sin ` ( t / 2 ) ) ) ) ) = 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 ) ) ) ) ) )
23 simpr 
 |-  ( ( N e. NN /\ S e. RR ) -> S e. RR )
24 2re 
 |-  2 e. RR
25 24 a1i 
 |-  ( N e. NN -> 2 e. RR )
26 nnre 
 |-  ( N e. NN -> N e. RR )
27 25 26 remulcld 
 |-  ( N e. NN -> ( 2 x. N ) e. RR )
28 1red 
 |-  ( N e. NN -> 1 e. RR )
29 27 28 readdcld 
 |-  ( N e. NN -> ( ( 2 x. N ) + 1 ) e. RR )
30 pire 
 |-  _pi e. RR
31 30 a1i 
 |-  ( N e. NN -> _pi e. RR )
32 25 31 remulcld 
 |-  ( N e. NN -> ( 2 x. _pi ) e. RR )
33 2cnd 
 |-  ( N e. NN -> 2 e. CC )
34 31 recnd 
 |-  ( N e. NN -> _pi e. CC )
35 2pos 
 |-  0 < 2
36 35 a1i 
 |-  ( N e. NN -> 0 < 2 )
37 36 gt0ne0d 
 |-  ( N e. NN -> 2 =/= 0 )
38 pipos 
 |-  0 < _pi
39 38 a1i 
 |-  ( N e. NN -> 0 < _pi )
40 39 gt0ne0d 
 |-  ( N e. NN -> _pi =/= 0 )
41 33 34 37 40 mulne0d 
 |-  ( N e. NN -> ( 2 x. _pi ) =/= 0 )
42 29 32 41 redivcld 
 |-  ( N e. NN -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) e. RR )
43 42 ad2antrr 
 |-  ( ( ( N e. NN /\ S e. RR ) /\ ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) e. RR )
44 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 )
45 43 44 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 )
46 13 22 23 45 fvmptd 
 |-  ( ( 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 ) ) ) ) ) )