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

Metamath Proof Explorer

Theorem dvcosre

Description: The real derivative of the cosine. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Assertion dvcosre ( ℝ D ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ - ( sin ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
2 cosf ⊢ cos : ℂ ⟶ ℂ
3 ssid ⊢ ℂ ⊆ ℂ
4 nfcv ⊢ Ⅎ 𝑥 ℝ
5 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V }
6 4 5 dfssf ⊢ ( ℝ ⊆ { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } ↔ ∀ 𝑥 ( 𝑥 ∈ ℝ → 𝑥 ∈ { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } ) )
7 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
8 7 sincld ⊢ ( 𝑥 ∈ ℝ → ( sin ‘ 𝑥 ) ∈ ℂ )
9 8 negcld ⊢ ( 𝑥 ∈ ℝ → - ( sin ‘ 𝑥 ) ∈ ℂ )
10 elex ⊢ ( - ( sin ‘ 𝑥 ) ∈ ℂ → - ( sin ‘ 𝑥 ) ∈ V )
11 9 10 syl ⊢ ( 𝑥 ∈ ℝ → - ( sin ‘ 𝑥 ) ∈ V )
12 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } ↔ ( 𝑥 ∈ ℂ ∧ - ( sin ‘ 𝑥 ) ∈ V ) )
13 7 11 12 sylanbrc ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V } )
14 6 13 mpgbir ⊢ ℝ ⊆ { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V }
15 dvcos ⊢ ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) )
16 15 dmmpt ⊢ dom ( ℂ D cos ) = { 𝑥 ∈ ℂ ∣ - ( sin ‘ 𝑥 ) ∈ V }
17 14 16 sseqtrri ⊢ ℝ ⊆ dom ( ℂ D cos )
18 dvres3 ⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ cos : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D cos ) ) ) → ( ℝ D ( cos ↾ ℝ ) ) = ( ( ℂ D cos ) ↾ ℝ ) )
19 1 2 3 17 18 mp4an ⊢ ( ℝ D ( cos ↾ ℝ ) ) = ( ( ℂ D cos ) ↾ ℝ )
20 ffn ⊢ ( cos : ℂ ⟶ ℂ → cos Fn ℂ )
21 2 20 ax-mp ⊢ cos Fn ℂ
22 dffn5 ⊢ ( cos Fn ℂ ↔ cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
23 21 22 mpbi ⊢ cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) )
24 23 reseq1i ⊢ ( cos ↾ ℝ ) = ( ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ↾ ℝ )
25 ax-resscn ⊢ ℝ ⊆ ℂ
26 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) ) )
27 25 26 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) )
28 24 27 eqtri ⊢ ( cos ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) )
29 28 oveq2i ⊢ ( ℝ D ( cos ↾ ℝ ) ) = ( ℝ D ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) ) )
30 15 reseq1i ⊢ ( ( ℂ D cos ) ↾ ℝ ) = ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) ↾ ℝ )
31 resmpt ⊢ ( ℝ ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ - ( sin ‘ 𝑥 ) ) )
32 25 31 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ - ( sin ‘ 𝑥 ) )
33 30 32 eqtri ⊢ ( ( ℂ D cos ) ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ - ( sin ‘ 𝑥 ) )
34 19 29 33 3eqtr3i ⊢ ( ℝ D ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ - ( sin ‘ 𝑥 ) )