Metamath Proof Explorer

Theorem dirkercncf

Description: For any natural number N , the Dirichlet Kernel ( DN ) is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis dirkercncf.d 
|- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
Assertion dirkercncf 
|- ( N e. NN -> ( D ` N ) e. ( RR -cn-> RR ) )

Proof

Step Hyp Ref Expression
1 dirkercncf.d 
 |-  D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
2 1 dirkerf 
 |-  ( N e. NN -> ( D ` N ) : RR --> RR )
3 ax-resscn 
 |-  RR C_ CC
4 3 a1i 
 |-  ( N e. NN -> RR C_ CC )
5 2 4 fssd 
 |-  ( N e. NN -> ( D ` N ) : RR --> CC )
6 5 ad2antrr 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( D ` N ) : RR --> CC )
7 oveq1 
 |-  ( y = w -> ( y mod ( 2 x. _pi ) ) = ( w mod ( 2 x. _pi ) ) )
8 7 eqeq1d 
 |-  ( y = w -> ( ( y mod ( 2 x. _pi ) ) = 0 <-> ( w mod ( 2 x. _pi ) ) = 0 ) )
9 oveq2 
 |-  ( y = w -> ( ( n + ( 1 / 2 ) ) x. y ) = ( ( n + ( 1 / 2 ) ) x. w ) )
10 9 fveq2d 
 |-  ( y = w -> ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) = ( sin ` ( ( n + ( 1 / 2 ) ) x. w ) ) )
11 oveq1 
 |-  ( y = w -> ( y / 2 ) = ( w / 2 ) )
12 11 fveq2d 
 |-  ( y = w -> ( sin ` ( y / 2 ) ) = ( sin ` ( w / 2 ) ) )
13 12 oveq2d 
 |-  ( y = w -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) )
14 10 13 oveq12d 
 |-  ( y = w -> ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( ( sin ` ( ( n + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) )
15 8 14 ifbieq2d 
 |-  ( y = w -> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = if ( ( w mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) ) )
16 15 cbvmptv 
 |-  ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) = ( w e. RR |-> if ( ( w mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) ) )
17 16 mpteq2i 
 |-  ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) ) = ( n e. NN |-> ( w e. RR |-> if ( ( w mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) ) ) )
18 1 17 eqtri 
 |-  D = ( n e. NN |-> ( w e. RR |-> if ( ( w mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) ) ) )
19 eqid 
 |-  ( y - _pi ) = ( y - _pi )
20 eqid 
 |-  ( y + _pi ) = ( y + _pi )
21 eqid 
 |-  ( w e. ( ( y - _pi ) (,) ( y + _pi ) ) |-> ( ( sin ` ( ( n + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) ) = ( w e. ( ( y - _pi ) (,) ( y + _pi ) ) |-> ( ( sin ` ( ( n + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) )
22 eqid 
 |-  ( w e. ( ( y - _pi ) (,) ( y + _pi ) ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) = ( w e. ( ( y - _pi ) (,) ( y + _pi ) ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) )
23 simpll 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> N e. NN )
24 simplr 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> y e. RR )
25 simpr 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( y mod ( 2 x. _pi ) ) = 0 )
26 18 19 20 21 22 23 24 25 dirkercncflem3 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( ( D ` N ) ` y ) e. ( ( D ` N ) limCC y ) )
27 3 jctl 
 |-  ( y e. RR -> ( RR C_ CC /\ y e. RR ) )
28 27 ad2antlr 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( RR C_ CC /\ y e. RR ) )
29 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
30 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
31 29 30 cnplimc 
 |-  ( ( RR C_ CC /\ y e. RR ) -> ( ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( ( D ` N ) : RR --> CC /\ ( ( D ` N ) ` y ) e. ( ( D ` N ) limCC y ) ) ) )
32 28 31 syl 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( ( D ` N ) : RR --> CC /\ ( ( D ` N ) ` y ) e. ( ( D ` N ) limCC y ) ) ) )
33 6 26 32 mpbir2and 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
34 29 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
35 34 a1i 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( TopOpen ` CCfld ) e. Top )
36 2 ad2antrr 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( D ` N ) : RR --> RR )
37 3 a1i 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> RR C_ CC )
38 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
39 38 toponunii 
 |-  RR = U. ( topGen ` ran (,) )
40 29 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
41 40 toponunii 
 |-  CC = U. ( TopOpen ` CCfld )
42 39 41 cnprest2 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( D ` N ) : RR --> RR /\ RR C_ CC ) -> ( ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` y ) ) )
43 35 36 37 42 syl3anc 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` y ) ) )
44 33 43 mpbid 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` y ) )
45 30 eqcomi 
 |-  ( ( TopOpen ` CCfld ) |`t RR ) = ( topGen ` ran (,) )
46 45 a1i 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( ( TopOpen ` CCfld ) |`t RR ) = ( topGen ` ran (,) ) )
47 46 oveq2d 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( ( topGen ` ran (,) ) CnP ( ( TopOpen ` CCfld ) |`t RR ) ) = ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) )
48 47 fveq1d 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( ( ( topGen ` ran (,) ) CnP ( ( TopOpen ` CCfld ) |`t RR ) ) ` y ) = ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` y ) )
49 44 48 eleqtrd 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ ( y mod ( 2 x. _pi ) ) = 0 ) -> ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` y ) )
50 simpll 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ -. ( y mod ( 2 x. _pi ) ) = 0 ) -> N e. NN )
51 simplr 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ -. ( y mod ( 2 x. _pi ) ) = 0 ) -> y e. RR )
52 neqne 
 |-  ( -. ( y mod ( 2 x. _pi ) ) = 0 -> ( y mod ( 2 x. _pi ) ) =/= 0 )
53 52 adantl 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ -. ( y mod ( 2 x. _pi ) ) = 0 ) -> ( y mod ( 2 x. _pi ) ) =/= 0 )
54 eqid 
 |-  ( |_ ` ( y / ( 2 x. _pi ) ) ) = ( |_ ` ( y / ( 2 x. _pi ) ) )
55 eqid 
 |-  ( ( |_ ` ( y / ( 2 x. _pi ) ) ) + 1 ) = ( ( |_ ` ( y / ( 2 x. _pi ) ) ) + 1 )
56 eqid 
 |-  ( ( |_ ` ( y / ( 2 x. _pi ) ) ) x. ( 2 x. _pi ) ) = ( ( |_ ` ( y / ( 2 x. _pi ) ) ) x. ( 2 x. _pi ) )
57 eqid 
 |-  ( ( ( |_ ` ( y / ( 2 x. _pi ) ) ) + 1 ) x. ( 2 x. _pi ) ) = ( ( ( |_ ` ( y / ( 2 x. _pi ) ) ) + 1 ) x. ( 2 x. _pi ) )
58 18 50 51 53 54 55 56 57 dirkercncflem4 
 |-  ( ( ( N e. NN /\ y e. RR ) /\ -. ( y mod ( 2 x. _pi ) ) = 0 ) -> ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` y ) )
59 49 58 pm2.61dan 
 |-  ( ( N e. NN /\ y e. RR ) -> ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` y ) )
60 59 ralrimiva 
 |-  ( N e. NN -> A. y e. RR ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` y ) )
61 cncnp 
 |-  ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( topGen ` ran (,) ) e. ( TopOn ` RR ) ) -> ( ( D ` N ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) <-> ( ( D ` N ) : RR --> RR /\ A. y e. RR ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` y ) ) ) )
62 38 38 61 mp2an 
 |-  ( ( D ` N ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) <-> ( ( D ` N ) : RR --> RR /\ A. y e. RR ( D ` N ) e. ( ( ( topGen ` ran (,) ) CnP ( topGen ` ran (,) ) ) ` y ) ) )
63 2 60 62 sylanbrc 
 |-  ( N e. NN -> ( D ` N ) e. ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
64 29 30 30 cncfcn 
 |-  ( ( RR C_ CC /\ RR C_ CC ) -> ( RR -cn-> RR ) = ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) ) )
65 3 3 64 mp2an 
 |-  ( RR -cn-> RR ) = ( ( topGen ` ran (,) ) Cn ( topGen ` ran (,) ) )
66 63 65 eleqtrrdi 
 |-  ( N e. NN -> ( D ` N ) e. ( RR -cn-> RR ) )