Metamath Proof Explorer

Theorem dvcosre

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

Ref Expression
Assertion dvcosre ⊢ dx ∈ ℝ cos ⁡ x d ℝ x = x ∈ ℝ ⟼ − sin ⁡ x

Proof

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