Metamath Proof Explorer


Theorem dvcos

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

Ref Expression
Assertion dvcos Dcos=xsinx

Proof

Step Hyp Ref Expression
1 dvsincos Dsin=cosDcos=xsinx
2 1 simpri Dcos=xsinx