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

Metamath Proof Explorer

Theorem dvcos

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

Ref Expression
Assertion dvcos ⊢ ℂ D cos = x ∈ ℂ ⟼ − sin ⁡ x

Proof

Step Hyp Ref Expression
1 dvsincos ⊢ ℂ D sin = cos ∧ ℂ D cos = x ∈ ℂ ⟼ − sin ⁡ x
2 1 simpri ⊢ ℂ D cos = x ∈ ℂ ⟼ − sin ⁡ x