Theorem dvcot

Description: Derivative of the cotangent function. (Contributed by Jon Pennant, 28-Aug-2026)

	Ref	Expression
Assertion	dvcot	$$⊢ℂ\mathrm{D}\cot =\left(x\in \mathrm{dom}\cot ⟼-{\csc \left(x\right)}^2\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-cot	$$⊢\cot =\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\cos x}{\sin x}\right)$$
2	1	oveq2i	$$⊢ℂ\mathrm{D}\cot =\frac{d\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\cos x}{\sin x}\right)}{d_{ℂ}x}$$
3		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
4	3	a1i	$$⊢\top \to ℂ\in \left\{ℝ,ℂ\right\}$$
5		elrabi	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to x\in ℂ$$
6		coscl	$$⊢x\in ℂ\to \cos x\in ℂ$$
7	5 6	syl	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \cos x\in ℂ$$
8	7	adantl	$$⊢\left(\top \wedge x\in \left\{y\in ℂ|\sin y\ne 0\right\}\right)\to \cos x\in ℂ$$
9		sincl	$$⊢x\in ℂ\to \sin x\in ℂ$$
10	5 9	syl	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \sin x\in ℂ$$
11	10	negcld	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\sin x\in ℂ$$
12	11	adantl	$$⊢\left(\top \wedge x\in \left\{y\in ℂ|\sin y\ne 0\right\}\right)\to -\sin x\in ℂ$$
13	6	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to \cos x\in ℂ$$
14	9	negcld	$$⊢x\in ℂ\to -\sin x\in ℂ$$
15	14	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to -\sin x\in ℂ$$
16		cosf	$$⊢\cos :ℂ⟶ℂ$$
17	16	a1i	$$⊢\top \to \cos :ℂ⟶ℂ$$
18	17	feqmptd	$$⊢\top \to \cos =\left(x\in ℂ⟼\cos x\right)$$
19	18	mptru	$$⊢\cos =\left(x\in ℂ⟼\cos x\right)$$
20	19	oveq2i	$$⊢ℂ\mathrm{D}\cos =\frac{d\left(x\in ℂ⟼\cos x\right)}{d_{ℂ}x}$$
21		dvcos	$$⊢ℂ\mathrm{D}\cos =\left(x\in ℂ⟼-\sin x\right)$$
22	20 21	eqtr3i	$$⊢\frac{d\left(x\in ℂ⟼\cos x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼-\sin x\right)$$
23	22	a1i	$$⊢\top \to \frac{d\left(x\in ℂ⟼\cos x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼-\sin x\right)$$
24		ssrab2	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}\subseteq ℂ$$
25	24	a1i	$$⊢\top \to \left\{y\in ℂ|\sin y\ne 0\right\}\subseteq ℂ$$
26		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
27	26	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
28	27	toponrestid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
29		sincn	$$⊢\sin :ℂ\underset{cn}{⟶}ℂ$$
30		ssid	$$⊢ℂ\subseteq ℂ$$
31	26 28 28	cncfcn	$$⊢\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
32	30 30 31	mp2an	$$⊢ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
33	29 32	eleqtri	$$⊢\sin \in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
34		cnn0opn	$$⊢ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
35		cnima	$$⊢\left(\sin \in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {\sin }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
36	33 34 35	mp2an	$$⊢{\sin }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
37		sincl	$$⊢y\in ℂ\to \sin y\in ℂ$$
38		eldifsn	$$⊢\sin y\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(\sin y\in ℂ\wedge \sin y\ne 0\right)$$
39	38	baib	$$⊢\sin y\in ℂ\to \left(\sin y\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \sin y\ne 0\right)$$
40	37 39	syl	$$⊢y\in ℂ\to \left(\sin y\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \sin y\ne 0\right)$$
41	40	bicomd	$$⊢y\in ℂ\to \left(\sin y\ne 0\leftrightarrow \sin y\in \left(ℂ\setminus \left\{0\right\}\right)\right)$$
42	41	rabbiia	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}=\left\{y\in ℂ|\sin y\in \left(ℂ\setminus \left\{0\right\}\right)\right\}$$
43		sinf	$$⊢\sin :ℂ⟶ℂ$$
44	43	a1i	$$⊢\top \to \sin :ℂ⟶ℂ$$
45	44	feqmptd	$$⊢\top \to \sin =\left(y\in ℂ⟼\sin y\right)$$
46	45	mptru	$$⊢\sin =\left(y\in ℂ⟼\sin y\right)$$
47	46	mptpreima	$$⊢{\sin }^{-1}\left[ℂ\setminus \left\{0\right\}\right]=\left\{y\in ℂ|\sin y\in \left(ℂ\setminus \left\{0\right\}\right)\right\}$$
48	42 47	eqtr4i	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}={\sin }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
49	48	eleq1i	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\leftrightarrow {\sin }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
50	36 49	mpbir	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
51	50	a1i	$$⊢\top \to \left\{y\in ℂ|\sin y\ne 0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
52	4 13 15 23 25 28 26 51	dvmptres	$$⊢\top \to \frac{d\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\cos x\right)}{d_{ℂ}x}=\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼-\sin x\right)$$
53		fveq2	$$⊢y=x\to \sin y=\sin x$$
54	53	neeq1d	$$⊢y=x\to \left(\sin y\ne 0\leftrightarrow \sin x\ne 0\right)$$
55	54	elrab	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\leftrightarrow \left(x\in ℂ\wedge \sin x\ne 0\right)$$
56	55	simprbi	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \sin x\ne 0$$
57	10 56	jca	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left(\sin x\in ℂ\wedge \sin x\ne 0\right)$$
58		eldifsn	$$⊢\sin x\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(\sin x\in ℂ\wedge \sin x\ne 0\right)$$
59	57 58	sylibr	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \sin x\in \left(ℂ\setminus \left\{0\right\}\right)$$
60	59	adantl	$$⊢\left(\top \wedge x\in \left\{y\in ℂ|\sin y\ne 0\right\}\right)\to \sin x\in \left(ℂ\setminus \left\{0\right\}\right)$$
61	9	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to \sin x\in ℂ$$
62	44	feqmptd	$$⊢\top \to \sin =\left(x\in ℂ⟼\sin x\right)$$
63	62	mptru	$$⊢\sin =\left(x\in ℂ⟼\sin x\right)$$
64	63	oveq2i	$$⊢ℂ\mathrm{D}\sin =\frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}$$
65		dvsin	$$⊢ℂ\mathrm{D}\sin =\cos$$
66	64 65	eqtr3i	$$⊢\frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}=\cos$$
67	66 19	eqtri	$$⊢\frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\cos x\right)$$
68	67	a1i	$$⊢\top \to \frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\cos x\right)$$
69	4 61 13 68 25 28 26 51	dvmptres	$$⊢\top \to \frac{d\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\sin x\right)}{d_{ℂ}x}=\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\cos x\right)$$
70	4 8 12 52 60 8 69	dvmptdiv	$$⊢\top \to \frac{d\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\cos x}{\sin x}\right)}{d_{ℂ}x}=\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\left(-\sin x\right)\sin x-\cos x\cos x}{{\sin x}^2}\right)$$
71	70	mptru	$$⊢\frac{d\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\cos x}{\sin x}\right)}{d_{ℂ}x}=\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\left(-\sin x\right)\sin x-\cos x\cos x}{{\sin x}^2}\right)$$
72	10 10	mulneg1d	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left(-\sin x\right)\sin x=-\sin x\sin x$$
73		sqval	$$⊢\sin x\in ℂ\to {\sin x}^2=\sin x\sin x$$
74	10 73	syl	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\sin x}^2=\sin x\sin x$$
75	74	eqcomd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \sin x\sin x={\sin x}^2$$
76	75	negeqd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\sin x\sin x=-{\sin x}^2$$
77	72 76	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left(-\sin x\right)\sin x=-{\sin x}^2$$
78		sqval	$$⊢\cos x\in ℂ\to {\cos x}^2=\cos x\cos x$$
79	7 78	syl	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\cos x}^2=\cos x\cos x$$
80	79	eqcomd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \cos x\cos x={\cos x}^2$$
81	77 80	oveq12d	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left(-\sin x\right)\sin x-\cos x\cos x=-{\sin x}^2-{\cos x}^2$$
82	10	sqcld	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\sin x}^2\in ℂ$$
83	7	sqcld	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\cos x}^2\in ℂ$$
84		negdi2	$$⊢\left({\sin x}^2\in ℂ\wedge {\cos x}^2\in ℂ\right)\to -\left({\sin x}^2+{\cos x}^2\right)=-{\sin x}^2-{\cos x}^2$$
85	82 83 84	syl2anc	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\left({\sin x}^2+{\cos x}^2\right)=-{\sin x}^2-{\cos x}^2$$
86	85	eqcomd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -{\sin x}^2-{\cos x}^2=-\left({\sin x}^2+{\cos x}^2\right)$$
87		sincossq	$$⊢x\in ℂ\to {\sin x}^2+{\cos x}^2=1$$
88	5 87	syl	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\sin x}^2+{\cos x}^2=1$$
89	88	negeqd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\left({\sin x}^2+{\cos x}^2\right)=-1$$
90	86 89	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -{\sin x}^2-{\cos x}^2=-1$$
91	81 90	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left(-\sin x\right)\sin x-\cos x\cos x=-1$$
92	91	oveq1d	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{\left(-\sin x\right)\sin x-\cos x\cos x}{{\sin x}^2}=\frac{-1}{{\sin x}^2}$$
93		ax-1cn	$$⊢1\in ℂ$$
94	93	a1i	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to 1\in ℂ$$
95		sqne0	$$⊢\sin x\in ℂ\to \left({\sin x}^2\ne 0\leftrightarrow \sin x\ne 0\right)$$
96	10 95	syl	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left({\sin x}^2\ne 0\leftrightarrow \sin x\ne 0\right)$$
97	56 96	mpbird	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\sin x}^2\ne 0$$
98		divneg	$$⊢\left(1\in ℂ\wedge {\sin x}^2\in ℂ\wedge {\sin x}^2\ne 0\right)\to -\frac{1}{{\sin x}^2}=\frac{-1}{{\sin x}^2}$$
99	94 82 97 98	syl3anc	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\frac{1}{{\sin x}^2}=\frac{-1}{{\sin x}^2}$$
100	99	eqcomd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{-1}{{\sin x}^2}=-\frac{1}{{\sin x}^2}$$
101	92 100	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{\left(-\sin x\right)\sin x-\cos x\cos x}{{\sin x}^2}=-\frac{1}{{\sin x}^2}$$
102		cscval	$$⊢\left(x\in ℂ\wedge \sin x\ne 0\right)\to \csc \left(x\right)=\frac{1}{\sin x}$$
103	55 102	sylbi	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \csc \left(x\right)=\frac{1}{\sin x}$$
104	103	oveq1d	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\csc \left(x\right)}^2={\left(\frac{1}{\sin x}\right)}^2$$
105		sqdiv	$$⊢\left(1\in ℂ\wedge \sin x\in ℂ\wedge \sin x\ne 0\right)\to {\left(\frac{1}{\sin x}\right)}^2=\frac{1^2}{{\sin x}^2}$$
106	94 10 56 105	syl3anc	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\left(\frac{1}{\sin x}\right)}^2=\frac{1^2}{{\sin x}^2}$$
107		sq1	$$⊢1^2=1$$
108	107	a1i	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to 1^2=1$$
109	108	oveq1d	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{1^2}{{\sin x}^2}=\frac{1}{{\sin x}^2}$$
110	106 109	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\left(\frac{1}{\sin x}\right)}^2=\frac{1}{{\sin x}^2}$$
111	104 110	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\csc \left(x\right)}^2=\frac{1}{{\sin x}^2}$$
112	111	eqcomd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{1}{{\sin x}^2}={\csc \left(x\right)}^2$$
113	112	negeqd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\frac{1}{{\sin x}^2}=-{\csc \left(x\right)}^2$$
114	101 113	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{\left(-\sin x\right)\sin x-\cos x\cos x}{{\sin x}^2}=-{\csc \left(x\right)}^2$$
115	114	mpteq2ia	$$⊢\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\left(-\sin x\right)\sin x-\cos x\cos x}{{\sin x}^2}\right)=\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼-{\csc \left(x\right)}^2\right)$$
116	7 10 56	divcld	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{\cos x}{\sin x}\in ℂ$$
117	1 116	fmpti	$$⊢\cot :\left\{y\in ℂ|\sin y\ne 0\right\}⟶ℂ$$
118	117	fdmi	$$⊢\mathrm{dom}\cot =\left\{y\in ℂ|\sin y\ne 0\right\}$$
119	118	eqcomi	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}=\mathrm{dom}\cot$$
120	119	mpteq1i	$$⊢\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼-{\csc \left(x\right)}^2\right)=\left(x\in \mathrm{dom}\cot ⟼-{\csc \left(x\right)}^2\right)$$
121	115 120	eqtri	$$⊢\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{\left(-\sin x\right)\sin x-\cos x\cos x}{{\sin x}^2}\right)=\left(x\in \mathrm{dom}\cot ⟼-{\csc \left(x\right)}^2\right)$$
122	2 71 121	3eqtri	$$⊢ℂ\mathrm{D}\cot =\left(x\in \mathrm{dom}\cot ⟼-{\csc \left(x\right)}^2\right)$$