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