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 29 tgioo2
 |-  ( 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 ) )