Theorem readvcot

Description: Real antiderivative of cotangent. (Contributed by SN, 7-Oct-2025)

	Ref	Expression
Hypothesis	readvcot.d	$$⊢D=\left\{y\in ℝ|\sin y\ne 0\right\}$$
Assertion	readvcot	$$⊢\frac{d\left(x\in D⟼\log \left|\sin x\right|\right)}{d_{ℝ}x}=\left(x\in D⟼\frac{\cos x}{\sin x}\right)$$

Proof

Step	Hyp	Ref	Expression
1		readvcot.d	$$⊢D=\left\{y\in ℝ|\sin y\ne 0\right\}$$
2		reelprrecn	$$⊢ℝ\in \left\{ℝ,ℂ\right\}$$
3	2	a1i	$$⊢\top \to ℝ\in \left\{ℝ,ℂ\right\}$$
4		fveq2	$$⊢y=x\to \sin y=\sin x$$
5	4	neeq1d	$$⊢y=x\to \left(\sin y\ne 0\leftrightarrow \sin x\ne 0\right)$$
6	5 1	elrab2	$$⊢x\in D\leftrightarrow \left(x\in ℝ\wedge \sin x\ne 0\right)$$
7		resincl	$$⊢x\in ℝ\to \sin x\in ℝ$$
8	7	adantr	$$⊢\left(x\in ℝ\wedge \sin x\ne 0\right)\to \sin x\in ℝ$$
9		simpr	$$⊢\left(x\in ℝ\wedge \sin x\ne 0\right)\to \sin x\ne 0$$
10	8 9	eldifsnd	$$⊢\left(x\in ℝ\wedge \sin x\ne 0\right)\to \sin x\in \left(ℝ\setminus \left\{0\right\}\right)$$
11	6 10	sylbi	$$⊢x\in D\to \sin x\in \left(ℝ\setminus \left\{0\right\}\right)$$
12	11	adantl	$$⊢\left(\top \wedge x\in D\right)\to \sin x\in \left(ℝ\setminus \left\{0\right\}\right)$$
13		fvexd	$$⊢\left(\top \wedge x\in D\right)\to \cos x\in \mathrm{V}$$
14		eldifi	$$⊢z\in \left(ℝ\setminus \left\{0\right\}\right)\to z\in ℝ$$
15	14	adantl	$$⊢\left(\top \wedge z\in \left(ℝ\setminus \left\{0\right\}\right)\right)\to z\in ℝ$$
16	15	recnd	$$⊢\left(\top \wedge z\in \left(ℝ\setminus \left\{0\right\}\right)\right)\to z\in ℂ$$
17	16	abscld	$$⊢\left(\top \wedge z\in \left(ℝ\setminus \left\{0\right\}\right)\right)\to \left|z\right|\in ℝ$$
18	17	recnd	$$⊢\left(\top \wedge z\in \left(ℝ\setminus \left\{0\right\}\right)\right)\to \left|z\right|\in ℂ$$
19		eldifsni	$$⊢z\in \left(ℝ\setminus \left\{0\right\}\right)\to z\ne 0$$
20	19	adantl	$$⊢\left(\top \wedge z\in \left(ℝ\setminus \left\{0\right\}\right)\right)\to z\ne 0$$
21	16 20	absne0d	$$⊢\left(\top \wedge z\in \left(ℝ\setminus \left\{0\right\}\right)\right)\to \left|z\right|\ne 0$$
22	18 21	logcld	$$⊢\left(\top \wedge z\in \left(ℝ\setminus \left\{0\right\}\right)\right)\to \log \left|z\right|\in ℂ$$
23		ovexd	$$⊢\left(\top \wedge z\in \left(ℝ\setminus \left\{0\right\}\right)\right)\to \frac{1}{z}\in \mathrm{V}$$
24	7	recnd	$$⊢x\in ℝ\to \sin x\in ℂ$$
25	24	adantl	$$⊢\left(\top \wedge x\in ℝ\right)\to \sin x\in ℂ$$
26		fvexd	$$⊢\left(\top \wedge x\in ℝ\right)\to \cos x\in \mathrm{V}$$
27		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
28		cnopn	$$⊢ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
29	28	a1i	$$⊢\top \to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
30		ax-resscn	$$⊢ℝ\subseteq ℂ$$
31		dfss2	$$⊢ℝ\subseteq ℂ\leftrightarrow ℝ\cap ℂ=ℝ$$
32	30 31	mpbi	$$⊢ℝ\cap ℂ=ℝ$$
33	32	a1i	$$⊢\top \to ℝ\cap ℂ=ℝ$$
34		sincl	$$⊢x\in ℂ\to \sin x\in ℂ$$
35	34	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to \sin x\in ℂ$$
36		fvexd	$$⊢\left(\top \wedge x\in ℂ\right)\to \cos x\in \mathrm{V}$$
37		dvsin	$$⊢ℂ\mathrm{D}\sin =\cos$$
38		sinf	$$⊢\sin :ℂ⟶ℂ$$
39	38	a1i	$$⊢\top \to \sin :ℂ⟶ℂ$$
40	39	feqmptd	$$⊢\top \to \sin =\left(x\in ℂ⟼\sin x\right)$$
41	40	oveq2d	$$⊢\top \to ℂ\mathrm{D}\sin =\frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}$$
42		cosf	$$⊢\cos :ℂ⟶ℂ$$
43	42	a1i	$$⊢\top \to \cos :ℂ⟶ℂ$$
44	43	feqmptd	$$⊢\top \to \cos =\left(x\in ℂ⟼\cos x\right)$$
45	37 41 44	3eqtr3a	$$⊢\top \to \frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\cos x\right)$$
46	27 3 29 33 35 36 45	dvmptres3	$$⊢\top \to \frac{d\left(x\in ℝ⟼\sin x\right)}{d_{ℝ}x}=\left(x\in ℝ⟼\cos x\right)$$
47	1	ssrab3	$$⊢D\subseteq ℝ$$
48	47	a1i	$$⊢\top \to D\subseteq ℝ$$
49		tgioo4	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
50	1	resuppsinopn	$$⊢D\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
51	50	a1i	$$⊢\top \to D\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
52	3 25 26 46 48 49 27 51	dvmptres	$$⊢\top \to \frac{d\left(x\in D⟼\sin x\right)}{d_{ℝ}x}=\left(x\in D⟼\cos x\right)$$
53		eqid	$$⊢ℝ\setminus \left\{0\right\}=ℝ\setminus \left\{0\right\}$$
54	53	readvrec	$$⊢\frac{d\left(z\in \left(ℝ\setminus \left\{0\right\}\right)⟼\log \left|z\right|\right)}{d_{ℝ}z}=\left(z\in \left(ℝ\setminus \left\{0\right\}\right)⟼\frac{1}{z}\right)$$
55	54	a1i	$$⊢\top \to \frac{d\left(z\in \left(ℝ\setminus \left\{0\right\}\right)⟼\log \left|z\right|\right)}{d_{ℝ}z}=\left(z\in \left(ℝ\setminus \left\{0\right\}\right)⟼\frac{1}{z}\right)$$
56		2fveq3	$$⊢z=\sin x\to \log \left|z\right|=\log \left|\sin x\right|$$
57		oveq2	$$⊢z=\sin x\to \frac{1}{z}=\frac{1}{\sin x}$$
58	3 3 12 13 22 23 52 55 56 57	dvmptco	$$⊢\top \to \frac{d\left(x\in D⟼\log \left|\sin x\right|\right)}{d_{ℝ}x}=\left(x\in D⟼\left(\frac{1}{\sin x}\right)\cos x\right)$$
59	58	mptru	$$⊢\frac{d\left(x\in D⟼\log \left|\sin x\right|\right)}{d_{ℝ}x}=\left(x\in D⟼\left(\frac{1}{\sin x}\right)\cos x\right)$$
60	6	simplbi	$$⊢x\in D\to x\in ℝ$$
61	60	recoscld	$$⊢x\in D\to \cos x\in ℝ$$
62	61	recnd	$$⊢x\in D\to \cos x\in ℂ$$
63	6 8	sylbi	$$⊢x\in D\to \sin x\in ℝ$$
64	63	recnd	$$⊢x\in D\to \sin x\in ℂ$$
65	6 9	sylbi	$$⊢x\in D\to \sin x\ne 0$$
66	62 64 65	divrec2d	$$⊢x\in D\to \frac{\cos x}{\sin x}=\left(\frac{1}{\sin x}\right)\cos x$$
67	66	mpteq2ia	$$⊢\left(x\in D⟼\frac{\cos x}{\sin x}\right)=\left(x\in D⟼\left(\frac{1}{\sin x}\right)\cos x\right)$$
68	59 67	eqtr4i	$$⊢\frac{d\left(x\in D⟼\log \left|\sin x\right|\right)}{d_{ℝ}x}=\left(x\in D⟼\frac{\cos x}{\sin x}\right)$$