Step |
Hyp |
Ref |
Expression |
1 |
|
reelprrecn |
|- RR e. { RR , CC } |
2 |
|
cosf |
|- cos : CC --> CC |
3 |
|
ssid |
|- CC C_ CC |
4 |
|
nfcv |
|- F/_ x RR |
5 |
|
nfrab1 |
|- F/_ x { x e. CC | -u ( sin ` x ) e. _V } |
6 |
4 5
|
dfss2f |
|- ( RR C_ { x e. CC | -u ( sin ` x ) e. _V } <-> A. x ( x e. RR -> x e. { x e. CC | -u ( sin ` x ) e. _V } ) ) |
7 |
|
recn |
|- ( x e. RR -> x e. CC ) |
8 |
7
|
sincld |
|- ( x e. RR -> ( sin ` x ) e. CC ) |
9 |
8
|
negcld |
|- ( x e. RR -> -u ( sin ` x ) e. CC ) |
10 |
|
elex |
|- ( -u ( sin ` x ) e. CC -> -u ( sin ` x ) e. _V ) |
11 |
9 10
|
syl |
|- ( x e. RR -> -u ( sin ` x ) e. _V ) |
12 |
|
rabid |
|- ( x e. { x e. CC | -u ( sin ` x ) e. _V } <-> ( x e. CC /\ -u ( sin ` x ) e. _V ) ) |
13 |
7 11 12
|
sylanbrc |
|- ( x e. RR -> x e. { x e. CC | -u ( sin ` x ) e. _V } ) |
14 |
6 13
|
mpgbir |
|- RR C_ { x e. CC | -u ( sin ` x ) e. _V } |
15 |
|
dvcos |
|- ( CC _D cos ) = ( x e. CC |-> -u ( sin ` x ) ) |
16 |
15
|
dmmpt |
|- dom ( CC _D cos ) = { x e. CC | -u ( sin ` x ) e. _V } |
17 |
14 16
|
sseqtrri |
|- RR C_ dom ( CC _D cos ) |
18 |
|
dvres3 |
|- ( ( ( RR e. { RR , CC } /\ cos : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D cos ) ) ) -> ( RR _D ( cos |` RR ) ) = ( ( CC _D cos ) |` RR ) ) |
19 |
1 2 3 17 18
|
mp4an |
|- ( RR _D ( cos |` RR ) ) = ( ( CC _D cos ) |` RR ) |
20 |
|
ffn |
|- ( cos : CC --> CC -> cos Fn CC ) |
21 |
2 20
|
ax-mp |
|- cos Fn CC |
22 |
|
dffn5 |
|- ( cos Fn CC <-> cos = ( x e. CC |-> ( cos ` x ) ) ) |
23 |
21 22
|
mpbi |
|- cos = ( x e. CC |-> ( cos ` x ) ) |
24 |
23
|
reseq1i |
|- ( cos |` RR ) = ( ( x e. CC |-> ( cos ` x ) ) |` RR ) |
25 |
|
ax-resscn |
|- RR C_ CC |
26 |
|
resmpt |
|- ( RR C_ CC -> ( ( x e. CC |-> ( cos ` x ) ) |` RR ) = ( x e. RR |-> ( cos ` x ) ) ) |
27 |
25 26
|
ax-mp |
|- ( ( x e. CC |-> ( cos ` x ) ) |` RR ) = ( x e. RR |-> ( cos ` x ) ) |
28 |
24 27
|
eqtri |
|- ( cos |` RR ) = ( x e. RR |-> ( cos ` x ) ) |
29 |
28
|
oveq2i |
|- ( RR _D ( cos |` RR ) ) = ( RR _D ( x e. RR |-> ( cos ` x ) ) ) |
30 |
15
|
reseq1i |
|- ( ( CC _D cos ) |` RR ) = ( ( x e. CC |-> -u ( sin ` x ) ) |` RR ) |
31 |
|
resmpt |
|- ( RR C_ CC -> ( ( x e. CC |-> -u ( sin ` x ) ) |` RR ) = ( x e. RR |-> -u ( sin ` x ) ) ) |
32 |
25 31
|
ax-mp |
|- ( ( x e. CC |-> -u ( sin ` x ) ) |` RR ) = ( x e. RR |-> -u ( sin ` x ) ) |
33 |
30 32
|
eqtri |
|- ( ( CC _D cos ) |` RR ) = ( x e. RR |-> -u ( sin ` x ) ) |
34 |
19 29 33
|
3eqtr3i |
|- ( RR _D ( x e. RR |-> ( cos ` x ) ) ) = ( x e. RR |-> -u ( sin ` x ) ) |