Step |
Hyp |
Ref |
Expression |
1 |
|
dirkerre.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
|
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 ) ) ) ) ) ) |
3 |
|
2re |
|- 2 e. RR |
4 |
3
|
a1i |
|- ( N e. NN -> 2 e. RR ) |
5 |
|
nnre |
|- ( N e. NN -> N e. RR ) |
6 |
4 5
|
remulcld |
|- ( N e. NN -> ( 2 x. N ) e. RR ) |
7 |
|
1red |
|- ( N e. NN -> 1 e. RR ) |
8 |
6 7
|
readdcld |
|- ( N e. NN -> ( ( 2 x. N ) + 1 ) e. RR ) |
9 |
|
pire |
|- _pi e. RR |
10 |
9
|
a1i |
|- ( N e. NN -> _pi e. RR ) |
11 |
4 10
|
remulcld |
|- ( N e. NN -> ( 2 x. _pi ) e. RR ) |
12 |
|
2cnd |
|- ( N e. NN -> 2 e. CC ) |
13 |
10
|
recnd |
|- ( N e. NN -> _pi e. CC ) |
14 |
|
2ne0 |
|- 2 =/= 0 |
15 |
14
|
a1i |
|- ( N e. NN -> 2 =/= 0 ) |
16 |
|
0re |
|- 0 e. RR |
17 |
|
pipos |
|- 0 < _pi |
18 |
16 17
|
gtneii |
|- _pi =/= 0 |
19 |
18
|
a1i |
|- ( N e. NN -> _pi =/= 0 ) |
20 |
12 13 15 19
|
mulne0d |
|- ( N e. NN -> ( 2 x. _pi ) =/= 0 ) |
21 |
8 11 20
|
redivcld |
|- ( N e. NN -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) e. RR ) |
22 |
21
|
ad2antrr |
|- ( ( ( N e. NN /\ S e. RR ) /\ ( S mod ( 2 x. _pi ) ) = 0 ) -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) e. RR ) |
23 |
|
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 ) |
24 |
22 23
|
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 ) |
25 |
2 24
|
eqeltrd |
|- ( ( N e. NN /\ S e. RR ) -> ( ( D ` N ) ` S ) e. RR ) |