Step |
Hyp |
Ref |
Expression |
1 |
|
dirkerval.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 |
|
simpl |
|- ( ( m = N /\ s e. RR ) -> m = N ) |
3 |
2
|
oveq2d |
|- ( ( m = N /\ s e. RR ) -> ( 2 x. m ) = ( 2 x. N ) ) |
4 |
3
|
oveq1d |
|- ( ( m = N /\ s e. RR ) -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. N ) + 1 ) ) |
5 |
4
|
oveq1d |
|- ( ( m = N /\ s e. RR ) -> ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) ) |
6 |
2
|
oveq1d |
|- ( ( m = N /\ s e. RR ) -> ( m + ( 1 / 2 ) ) = ( N + ( 1 / 2 ) ) ) |
7 |
6
|
fvoveq1d |
|- ( ( m = N /\ s e. RR ) -> ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) ) |
8 |
7
|
oveq1d |
|- ( ( m = N /\ s e. RR ) -> ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) |
9 |
5 8
|
ifeq12d |
|- ( ( m = N /\ s e. RR ) -> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) = 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 ) ) ) ) ) ) |
10 |
9
|
mpteq2dva |
|- ( m = N -> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) ) |
11 |
|
simpl |
|- ( ( n = m /\ s e. RR ) -> n = m ) |
12 |
11
|
oveq2d |
|- ( ( n = m /\ s e. RR ) -> ( 2 x. n ) = ( 2 x. m ) ) |
13 |
12
|
oveq1d |
|- ( ( n = m /\ s e. RR ) -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. m ) + 1 ) ) |
14 |
13
|
oveq1d |
|- ( ( n = m /\ s e. RR ) -> ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) = ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) ) |
15 |
11
|
oveq1d |
|- ( ( n = m /\ s e. RR ) -> ( n + ( 1 / 2 ) ) = ( m + ( 1 / 2 ) ) ) |
16 |
15
|
fvoveq1d |
|- ( ( n = m /\ s e. RR ) -> ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) = ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) ) |
17 |
16
|
oveq1d |
|- ( ( n = m /\ s e. RR ) -> ( ( sin ` ( ( n + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) = ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) |
18 |
14 17
|
ifeq12d |
|- ( ( n = m /\ 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 ) ) ) ) ) = if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) |
19 |
18
|
mpteq2dva |
|- ( n = m -> ( 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 ) ) ) ) ) ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) ) |
20 |
19
|
cbvmptv |
|- ( 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 ) ) ) ) ) ) ) = ( m e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) ) |
21 |
1 20
|
eqtri |
|- D = ( m e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) ) |
22 |
|
reex |
|- RR e. _V |
23 |
22
|
mptex |
|- ( 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. _V |
24 |
10 21 23
|
fvmpt |
|- ( N e. NN -> ( D ` N ) = ( 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 ) ) ) ) ) ) ) |