Metamath Proof Explorer

Theorem dvsin

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

Ref Expression
Assertion dvsin 
|- ( CC _D sin ) = cos

Proof

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