Theorem dvsin

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

	Ref	Expression
Assertion	dvsin	$$⊢ℂ\mathrm{D}\sin =\cos$$

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	simpli	$$⊢ℂ\mathrm{D}\sin =\cos$$