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 ‘ 𝑥 ) )