Theorem dvsec

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

	Ref	Expression
Assertion	dvsec	$$⊢ℂ\mathrm{D}\sec =\left(x\in \mathrm{dom}\sec ⟼\sec \left(x\right)\tan x\right)$$

Proof

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