Theorem dvcsc

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

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

Proof

Step	Hyp	Ref	Expression
1		df-csc	$$⊢\csc =\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{1}{\sin x}\right)$$
2	1	oveq2i	$$⊢ℂ\mathrm{D}\csc =\frac{d\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{1}{\sin x}\right)}{d_{ℂ}x}$$
3		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
4	3	a1i	$$⊢\top \to ℂ\in \left\{ℝ,ℂ\right\}$$
5		1cnd	$$⊢\top \to 1\in ℂ$$
6		elrabi	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to x\in ℂ$$
7		sincl	$$⊢x\in ℂ\to \sin x\in ℂ$$
8	6 7	syl	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \sin x\in ℂ$$
9		fveq2	$$⊢y=x\to \sin y=\sin x$$
10	9	neeq1d	$$⊢y=x\to \left(\sin y\ne 0\leftrightarrow \sin x\ne 0\right)$$
11	10	elrab	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\leftrightarrow \left(x\in ℂ\wedge \sin x\ne 0\right)$$
12	11	simprbi	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \sin x\ne 0$$
13	8 12	jca	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left(\sin x\in ℂ\wedge \sin x\ne 0\right)$$
14		eldifsn	$$⊢\sin x\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(\sin x\in ℂ\wedge \sin x\ne 0\right)$$
15	13 14	sylibr	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \sin x\in \left(ℂ\setminus \left\{0\right\}\right)$$
16	15	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)$$
17		coscl	$$⊢x\in ℂ\to \cos x\in ℂ$$
18	6 17	syl	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \cos x\in ℂ$$
19	18	adantl	$$⊢\left(\top \wedge x\in \left\{y\in ℂ|\sin y\ne 0\right\}\right)\to \cos x\in ℂ$$
20	7	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to \sin x\in ℂ$$
21	17	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to \cos x\in ℂ$$
22		sinf	$$⊢\sin :ℂ⟶ℂ$$
23	22	a1i	$$⊢\top \to \sin :ℂ⟶ℂ$$
24	23	feqmptd	$$⊢\top \to \sin =\left(x\in ℂ⟼\sin x\right)$$
25	24	mptru	$$⊢\sin =\left(x\in ℂ⟼\sin x\right)$$
26	25	oveq2i	$$⊢ℂ\mathrm{D}\sin =\frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}$$
27		dvsin	$$⊢ℂ\mathrm{D}\sin =\cos$$
28	26 27	eqtr3i	$$⊢\frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}=\cos$$
29		cosf	$$⊢\cos :ℂ⟶ℂ$$
30	29	a1i	$$⊢\top \to \cos :ℂ⟶ℂ$$
31	30	feqmptd	$$⊢\top \to \cos =\left(x\in ℂ⟼\cos x\right)$$
32	31	mptru	$$⊢\cos =\left(x\in ℂ⟼\cos x\right)$$
33	28 32	eqtri	$$⊢\frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\cos x\right)$$
34	33	a1i	$$⊢\top \to \frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\cos x\right)$$
35		ssrab2	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}\subseteq ℂ$$
36	35	a1i	$$⊢\top \to \left\{y\in ℂ|\sin y\ne 0\right\}\subseteq ℂ$$
37		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
38	37	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
39	38	toponrestid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
40		sincn	$$⊢\sin :ℂ\underset{cn}{⟶}ℂ$$
41		ssid	$$⊢ℂ\subseteq ℂ$$
42	37 39 39	cncfcn	$$⊢\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
43	41 41 42	mp2an	$$⊢ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
44	40 43	eleqtri	$$⊢\sin \in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
45		cnn0opn	$$⊢ℂ\setminus \left\{0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
46		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)$$
47	44 45 46	mp2an	$$⊢{\sin }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
48		sincl	$$⊢y\in ℂ\to \sin y\in ℂ$$
49		eldifsn	$$⊢\sin y\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(\sin y\in ℂ\wedge \sin y\ne 0\right)$$
50	49	baib	$$⊢\sin y\in ℂ\to \left(\sin y\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \sin y\ne 0\right)$$
51	48 50	syl	$$⊢y\in ℂ\to \left(\sin y\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \sin y\ne 0\right)$$
52	51	bicomd	$$⊢y\in ℂ\to \left(\sin y\ne 0\leftrightarrow \sin y\in \left(ℂ\setminus \left\{0\right\}\right)\right)$$
53	52	rabbiia	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}=\left\{y\in ℂ|\sin y\in \left(ℂ\setminus \left\{0\right\}\right)\right\}$$
54	23	feqmptd	$$⊢\top \to \sin =\left(y\in ℂ⟼\sin y\right)$$
55	54	mptru	$$⊢\sin =\left(y\in ℂ⟼\sin y\right)$$
56	55	mptpreima	$$⊢{\sin }^{-1}\left[ℂ\setminus \left\{0\right\}\right]=\left\{y\in ℂ|\sin y\in \left(ℂ\setminus \left\{0\right\}\right)\right\}$$
57	53 56	eqtr4i	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}={\sin }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
58	57	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)$$
59	47 58	mpbir	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
60	59	a1i	$$⊢\top \to \left\{y\in ℂ|\sin y\ne 0\right\}\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
61	4 20 21 34 36 39 37 60	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)$$
62	4 5 16 19 61	dvrecg	$$⊢\top \to \frac{d\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{1}{\sin x}\right)}{d_{ℂ}x}=\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼-\frac{1\cos x}{{\sin x}^2}\right)$$
63	62	mptru	$$⊢\frac{d\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\frac{1}{\sin x}\right)}{d_{ℂ}x}=\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼-\frac{1\cos x}{{\sin x}^2}\right)$$
64	18	mullidd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to 1\cos x=\cos x$$
65		sqval	$$⊢\sin x\in ℂ\to {\sin x}^2=\sin x\sin x$$
66	8 65	syl	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to {\sin x}^2=\sin x\sin x$$
67	64 66	oveq12d	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{1\cos x}{{\sin x}^2}=\frac{\cos x}{\sin x\sin x}$$
68	67	negeqd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\frac{1\cos x}{{\sin x}^2}=-\frac{\cos x}{\sin x\sin x}$$
69		ax-1cn	$$⊢1\in ℂ$$
70	69	a1i	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to 1\in ℂ$$
71	70 8 18 8 12 12	divmuldivd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left(\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)=\frac{1\cos x}{\sin x\sin x}$$
72	64	oveq1d	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{1\cos x}{\sin x\sin x}=\frac{\cos x}{\sin x\sin x}$$
73	71 72	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left(\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)=\frac{\cos x}{\sin x\sin x}$$
74	73	eqcomd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{\cos x}{\sin x\sin x}=\left(\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)$$
75	74	negeqd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\frac{\cos x}{\sin x\sin x}=-\left(\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)$$
76	68 75	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\frac{1\cos x}{{\sin x}^2}=-\left(\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)$$
77	70 8 12	divcld	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{1}{\sin x}\in ℂ$$
78	18 8 12	divcld	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{\cos x}{\sin x}\in ℂ$$
79	77 78	mulneg1d	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left(-\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)=-\left(\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)$$
80	79	eqcomd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\left(\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)=\left(-\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)$$
81	76 80	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\frac{1\cos x}{{\sin x}^2}=\left(-\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)$$
82		cscval	$$⊢\left(x\in ℂ\wedge \sin x\ne 0\right)\to \csc \left(x\right)=\frac{1}{\sin x}$$
83	11 82	sylbi	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \csc \left(x\right)=\frac{1}{\sin x}$$
84	83	eqcomd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{1}{\sin x}=\csc \left(x\right)$$
85	84	negeqd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\frac{1}{\sin x}=-\csc \left(x\right)$$
86		cotval	$$⊢\left(x\in ℂ\wedge \sin x\ne 0\right)\to \cot \left(x\right)=\frac{\cos x}{\sin x}$$
87	11 86	sylbi	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \cot \left(x\right)=\frac{\cos x}{\sin x}$$
88	87	eqcomd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \frac{\cos x}{\sin x}=\cot \left(x\right)$$
89	85 88	oveq12d	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to \left(-\frac{1}{\sin x}\right)\left(\frac{\cos x}{\sin x}\right)=\left(-\csc \left(x\right)\right)\cot \left(x\right)$$
90	81 89	eqtrd	$$⊢x\in \left\{y\in ℂ|\sin y\ne 0\right\}\to -\frac{1\cos x}{{\sin x}^2}=\left(-\csc \left(x\right)\right)\cot \left(x\right)$$
91	90	mpteq2ia	$$⊢\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼-\frac{1\cos x}{{\sin x}^2}\right)=\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\left(-\csc \left(x\right)\right)\cot \left(x\right)\right)$$
92	1 77	fmpti	$$⊢\csc :\left\{y\in ℂ|\sin y\ne 0\right\}⟶ℂ$$
93	92	fdmi	$$⊢\mathrm{dom}\csc =\left\{y\in ℂ|\sin y\ne 0\right\}$$
94	93	eqcomi	$$⊢\left\{y\in ℂ|\sin y\ne 0\right\}=\mathrm{dom}\csc$$
95	94	mpteq1i	$$⊢\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼\left(-\csc \left(x\right)\right)\cot \left(x\right)\right)=\left(x\in \mathrm{dom}\csc ⟼\left(-\csc \left(x\right)\right)\cot \left(x\right)\right)$$
96	91 95	eqtri	$$⊢\left(x\in \left\{y\in ℂ|\sin y\ne 0\right\}⟼-\frac{1\cos x}{{\sin x}^2}\right)=\left(x\in \mathrm{dom}\csc ⟼\left(-\csc \left(x\right)\right)\cot \left(x\right)\right)$$
97	2 63 96	3eqtri	$$⊢ℂ\mathrm{D}\csc =\left(x\in \mathrm{dom}\csc ⟼\left(-\csc \left(x\right)\right)\cot \left(x\right)\right)$$