Metamath Proof Explorer

Theorem dirkercncflem3

Description: The Dirichlet Kernel is continuous at Y points that are multiples of ( 2 x. _pi ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dirkercncflem3.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 ) ) ) ) ) ) )
dirkercncflem3.a 
|- A = ( Y - _pi )
dirkercncflem3.b 
|- B = ( Y + _pi )
dirkercncflem3.f 
|- F = ( y e. ( A (,) B ) |-> ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
dirkercncflem3.g 
|- G = ( y e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
dirkercncflem3.n 
|- ( ph -> N e. NN )
dirkercncflem3.yr 
|- ( ph -> Y e. RR )
dirkercncflem3.yod 
|- ( ph -> ( Y mod ( 2 x. _pi ) ) = 0 )
Assertion dirkercncflem3 
|- ( ph -> ( ( D ` N ) ` Y ) e. ( ( D ` N ) limCC Y ) )

Proof

Step Hyp Ref Expression
1 dirkercncflem3.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 dirkercncflem3.a 
 |-  A = ( Y - _pi )
3 dirkercncflem3.b 
 |-  B = ( Y + _pi )
4 dirkercncflem3.f 
 |-  F = ( y e. ( A (,) B ) |-> ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
5 dirkercncflem3.g 
 |-  G = ( y e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
6 dirkercncflem3.n 
 |-  ( ph -> N e. NN )
7 dirkercncflem3.yr 
 |-  ( ph -> Y e. RR )
8 dirkercncflem3.yod 
 |-  ( ph -> ( Y mod ( 2 x. _pi ) ) = 0 )
9 oveq2 
 |-  ( w = y -> ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. y ) )
10 9 fveq2d 
 |-  ( w = y -> ( sin ` ( ( N + ( 1 / 2 ) ) x. w ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
11 10 cbvmptv 
 |-  ( w e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
12 fvoveq1 
 |-  ( w = y -> ( sin ` ( w / 2 ) ) = ( sin ` ( y / 2 ) ) )
13 12 oveq2d 
 |-  ( w = y -> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
14 13 cbvmptv 
 |-  ( w e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
15 2 3 7 8 dirkercncflem1 
 |-  ( ph -> ( Y e. ( A (,) B ) /\ A. y e. ( ( A (,) B ) \ { Y } ) ( ( sin ` ( y / 2 ) ) =/= 0 /\ ( cos ` ( y / 2 ) ) =/= 0 ) ) )
16 15 simprd 
 |-  ( ph -> A. y e. ( ( A (,) B ) \ { Y } ) ( ( sin ` ( y / 2 ) ) =/= 0 /\ ( cos ` ( y / 2 ) ) =/= 0 ) )
17 r19.26 
 |-  ( A. y e. ( ( A (,) B ) \ { Y } ) ( ( sin ` ( y / 2 ) ) =/= 0 /\ ( cos ` ( y / 2 ) ) =/= 0 ) <-> ( A. y e. ( ( A (,) B ) \ { Y } ) ( sin ` ( y / 2 ) ) =/= 0 /\ A. y e. ( ( A (,) B ) \ { Y } ) ( cos ` ( y / 2 ) ) =/= 0 ) )
18 16 17 sylib 
 |-  ( ph -> ( A. y e. ( ( A (,) B ) \ { Y } ) ( sin ` ( y / 2 ) ) =/= 0 /\ A. y e. ( ( A (,) B ) \ { Y } ) ( cos ` ( y / 2 ) ) =/= 0 ) )
19 18 simpld 
 |-  ( ph -> A. y e. ( ( A (,) B ) \ { Y } ) ( sin ` ( y / 2 ) ) =/= 0 )
20 19 r19.21bi 
 |-  ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( y / 2 ) ) =/= 0 )
21 9 fveq2d 
 |-  ( w = y -> ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) = ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
22 21 oveq2d 
 |-  ( w = y -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) = ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
23 22 cbvmptv 
 |-  ( w e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
24 fvoveq1 
 |-  ( w = y -> ( cos ` ( w / 2 ) ) = ( cos ` ( y / 2 ) ) )
25 24 oveq2d 
 |-  ( w = y -> ( _pi x. ( cos ` ( w / 2 ) ) ) = ( _pi x. ( cos ` ( y / 2 ) ) ) )
26 25 cbvmptv 
 |-  ( w e. ( ( A (,) B ) \ { Y } ) |-> ( _pi x. ( cos ` ( w / 2 ) ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( _pi x. ( cos ` ( y / 2 ) ) ) )
27 eqid 
 |-  ( z e. ( A (,) B ) |-> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. z ) ) ) / ( _pi x. ( cos ` ( z / 2 ) ) ) ) ) = ( z e. ( A (,) B ) |-> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. z ) ) ) / ( _pi x. ( cos ` ( z / 2 ) ) ) ) )
28 15 simpld 
 |-  ( ph -> Y e. ( A (,) B ) )
29 18 simprd 
 |-  ( ph -> A. y e. ( ( A (,) B ) \ { Y } ) ( cos ` ( y / 2 ) ) =/= 0 )
30 29 r19.21bi 
 |-  ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( cos ` ( y / 2 ) ) =/= 0 )
31 1 11 14 20 23 26 27 6 28 8 30 dirkercncflem2 
 |-  ( ph -> ( ( D ` N ) ` Y ) e. ( ( ( D ` N ) |` ( ( A (,) B ) \ { Y } ) ) limCC Y ) )
32 1 dirkerf 
 |-  ( N e. NN -> ( D ` N ) : RR --> RR )
33 6 32 syl 
 |-  ( ph -> ( D ` N ) : RR --> RR )
34 ax-resscn 
 |-  RR C_ CC
35 34 a1i 
 |-  ( ph -> RR C_ CC )
36 33 35 fssd 
 |-  ( ph -> ( D ` N ) : RR --> CC )
37 ioossre 
 |-  ( A (,) B ) C_ RR
38 37 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
39 38 ssdifssd 
 |-  ( ph -> ( ( A (,) B ) \ { Y } ) C_ RR )
40 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
41 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( RR u. { Y } ) ) = ( ( TopOpen ` CCfld ) |`t ( RR u. { Y } ) )
42 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
43 retop 
 |-  ( topGen ` ran (,) ) e. Top
44 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
45 44 isopn3 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,) B ) C_ RR ) -> ( ( A (,) B ) e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) ) )
46 43 38 45 sylancr 
 |-  ( ph -> ( ( A (,) B ) e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) ) )
47 42 46 mpbii 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) )
48 28 47 eleqtrrd 
 |-  ( ph -> Y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
49 40 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
50 49 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) )
51 50 fveq2d 
 |-  ( ph -> ( int ` ( topGen ` ran (,) ) ) = ( int ` ( ( TopOpen ` CCfld ) |`t RR ) ) )
52 51 fveq1d 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t RR ) ) ` ( A (,) B ) ) )
53 48 52 eleqtrd 
 |-  ( ph -> Y e. ( ( int ` ( ( TopOpen ` CCfld ) |`t RR ) ) ` ( A (,) B ) ) )
54 7 snssd 
 |-  ( ph -> { Y } C_ RR )
55 ssequn2 
 |-  ( { Y } C_ RR <-> ( RR u. { Y } ) = RR )
56 54 55 sylib 
 |-  ( ph -> ( RR u. { Y } ) = RR )
57 56 oveq2d 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( RR u. { Y } ) ) = ( ( TopOpen ` CCfld ) |`t RR ) )
58 57 fveq2d 
 |-  ( ph -> ( int ` ( ( TopOpen ` CCfld ) |`t ( RR u. { Y } ) ) ) = ( int ` ( ( TopOpen ` CCfld ) |`t RR ) ) )
59 uncom 
 |-  ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( { Y } u. ( ( A (,) B ) \ { Y } ) )
60 28 snssd 
 |-  ( ph -> { Y } C_ ( A (,) B ) )
61 undif 
 |-  ( { Y } C_ ( A (,) B ) <-> ( { Y } u. ( ( A (,) B ) \ { Y } ) ) = ( A (,) B ) )
62 60 61 sylib 
 |-  ( ph -> ( { Y } u. ( ( A (,) B ) \ { Y } ) ) = ( A (,) B ) )
63 59 62 syl5eq 
 |-  ( ph -> ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( A (,) B ) )
64 58 63 fveq12d 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t ( RR u. { Y } ) ) ) ` ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t RR ) ) ` ( A (,) B ) ) )
65 53 64 eleqtrrd 
 |-  ( ph -> Y e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( RR u. { Y } ) ) ) ` ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) )
66 36 39 35 40 41 65 limcres 
 |-  ( ph -> ( ( ( D ` N ) |` ( ( A (,) B ) \ { Y } ) ) limCC Y ) = ( ( D ` N ) limCC Y ) )
67 31 66 eleqtrd 
 |-  ( ph -> ( ( D ` N ) ` Y ) e. ( ( D ` N ) limCC Y ) )