This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvsin

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

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

Step	Hyp	Ref	Expression
1		dvsincos	$⊢ (ℂ D \sin = \cos \land ℂ D \cos = (x \in ℂ ⟼ - \sin x))$
2	1	simpli	$⊢ ℂ D \sin = \cos$