Metamath Proof Explorer

Theorem dvcosre

Description: The real derivative of the cosine. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Assertion dvcosre 
|- ( RR _D ( x e. RR |-> ( cos ` x ) ) ) = ( x e. RR |-> -u ( sin ` x ) )

Proof

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