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 dfss2f ( ℝ ⊆ { 𝑥 ∈ ℂ ∣ - ( 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 ‘ 𝑥 ) )