Theorem dvcosre

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

	Ref	Expression
Assertion	dvcosre	$$⊢\frac{d\left(x\in ℝ⟼\cos x\right)}{d_{ℝ}x}=\left(x\in ℝ⟼-\sin x\right)$$

Proof

Step	Hyp	Ref	Expression
1		reelprrecn	$$⊢ℝ\in \left\{ℝ,ℂ\right\}$$
2		cosf	$$⊢\cos :ℂ⟶ℂ$$
3		ssid	$$⊢ℂ\subseteq ℂ$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xℝ$$
5		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in ℂ|-\sin x\in \mathrm{V}\right\}$$
6	4 5	dfss2f	$$⊢ℝ\subseteq \left\{x\in ℂ|-\sin x\in \mathrm{V}\right\}\leftrightarrow \forall x\left(x\in ℝ\to x\in \left\{x\in ℂ|-\sin x\in \mathrm{V}\right\}\right)$$
7		recn	$$⊢x\in ℝ\to x\in ℂ$$
8	7	sincld	$$⊢x\in ℝ\to \sin x\in ℂ$$
9	8	negcld	$$⊢x\in ℝ\to -\sin x\in ℂ$$
10		elex	$$⊢-\sin x\in ℂ\to -\sin x\in \mathrm{V}$$
11	9 10	syl	$$⊢x\in ℝ\to -\sin x\in \mathrm{V}$$
12		rabid	$$⊢x\in \left\{x\in ℂ|-\sin x\in \mathrm{V}\right\}\leftrightarrow \left(x\in ℂ\wedge -\sin x\in \mathrm{V}\right)$$
13	7 11 12	sylanbrc	$$⊢x\in ℝ\to x\in \left\{x\in ℂ|-\sin x\in \mathrm{V}\right\}$$
14	6 13	mpgbir	$$⊢ℝ\subseteq \left\{x\in ℂ|-\sin x\in \mathrm{V}\right\}$$
15		dvcos	$$⊢ℂ\mathrm{D}\cos =\left(x\in ℂ⟼-\sin x\right)$$
16	15	dmmpt	$$⊢\mathrm{dom}{\cos }_{ℂ}^{\prime }=\left\{x\in ℂ|-\sin x\in \mathrm{V}\right\}$$
17	14 16	sseqtrri	$$⊢ℝ\subseteq \mathrm{dom}{\cos }_{ℂ}^{\prime }$$
18		dvres3	$$⊢\left(\left(ℝ\in \left\{ℝ,ℂ\right\}\wedge \cos :ℂ⟶ℂ\right)\wedge \left(ℂ\subseteq ℂ\wedge ℝ\subseteq \mathrm{dom}{\cos }_{ℂ}^{\prime }\right)\right)\to ℝ\mathrm{D}\left({\cos \upharpoonright }_{ℝ}\right)={{\cos }_{ℂ}^{\prime }\upharpoonright }_{ℝ}$$
19	1 2 3 17 18	mp4an	$$⊢ℝ\mathrm{D}\left({\cos \upharpoonright }_{ℝ}\right)={{\cos }_{ℂ}^{\prime }\upharpoonright }_{ℝ}$$
20		ffn	$$⊢\cos :ℂ⟶ℂ\to \cos Fnℂ$$
21	2 20	ax-mp	$$⊢\cos Fnℂ$$
22		dffn5	$$⊢\cos Fnℂ\leftrightarrow \cos =\left(x\in ℂ⟼\cos x\right)$$
23	21 22	mpbi	$$⊢\cos =\left(x\in ℂ⟼\cos x\right)$$
24	23	reseq1i	$$⊢{\cos \upharpoonright }_{ℝ}={\left(x\in ℂ⟼\cos x\right)\upharpoonright }_{ℝ}$$
25		ax-resscn	$$⊢ℝ\subseteq ℂ$$
26		resmpt	$$⊢ℝ\subseteq ℂ\to {\left(x\in ℂ⟼\cos x\right)\upharpoonright }_{ℝ}=\left(x\in ℝ⟼\cos x\right)$$
27	25 26	ax-mp	$$⊢{\left(x\in ℂ⟼\cos x\right)\upharpoonright }_{ℝ}=\left(x\in ℝ⟼\cos x\right)$$
28	24 27	eqtri	$$⊢{\cos \upharpoonright }_{ℝ}=\left(x\in ℝ⟼\cos x\right)$$
29	28	oveq2i	$$⊢ℝ\mathrm{D}\left({\cos \upharpoonright }_{ℝ}\right)=\frac{d\left(x\in ℝ⟼\cos x\right)}{d_{ℝ}x}$$
30	15	reseq1i	$$⊢{{\cos }_{ℂ}^{\prime }\upharpoonright }_{ℝ}={\left(x\in ℂ⟼-\sin x\right)\upharpoonright }_{ℝ}$$
31		resmpt	$$⊢ℝ\subseteq ℂ\to {\left(x\in ℂ⟼-\sin x\right)\upharpoonright }_{ℝ}=\left(x\in ℝ⟼-\sin x\right)$$
32	25 31	ax-mp	$$⊢{\left(x\in ℂ⟼-\sin x\right)\upharpoonright }_{ℝ}=\left(x\in ℝ⟼-\sin x\right)$$
33	30 32	eqtri	$$⊢{{\cos }_{ℂ}^{\prime }\upharpoonright }_{ℝ}=\left(x\in ℝ⟼-\sin x\right)$$
34	19 29 33	3eqtr3i	$$⊢\frac{d\left(x\in ℝ⟼\cos x\right)}{d_{ℝ}x}=\left(x\in ℝ⟼-\sin x\right)$$