Metamath Proof Explorer

Theorem dvcos

Description: Derivative of the cosine function. (Contributed by Mario Carneiro, 21-May-2016)

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

Proof

Step Hyp Ref Expression
1 dvsincos 
 |-  ( ( CC _D sin ) = cos /\ ( CC _D cos ) = ( x e. CC |-> -u ( sin ` x ) ) )
2 1 simpri 
 |-  ( CC _D cos ) = ( x e. CC |-> -u ( sin ` x ) )