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 ) ) |