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 ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 dvsincos ⊢ ( ( ℂ D sin ) = cos ∧ ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) )
2 1 simpri ⊢ ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) )