Theorem dvcos

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

	Ref	Expression
Assertion	dvcos	$$⊢ℂ\mathrm{D}\cos =\left(x\in ℂ⟼-\sin x\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvsincos	$$⊢\left(ℂ\mathrm{D}\sin =\cos \wedge ℂ\mathrm{D}\cos =\left(x\in ℂ⟼-\sin x\right)\right)$$
2	1	simpri	$$⊢ℂ\mathrm{D}\cos =\left(x\in ℂ⟼-\sin x\right)$$