Theorem dvtan

Description: Derivative of tangent. (Contributed by Brendan Leahy, 7-Aug-2018)

	Ref	Expression
Assertion	dvtan	$$⊢ℂ\mathrm{D}\tan =\left(x\in \mathrm{dom}\tan ⟼{\cos x}^{-2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-tan	$$⊢\tan =\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sin x}{\cos x}\right)$$
2		cnvimass	$$⊢{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq \mathrm{dom}\cos$$
3		cosf	$$⊢\cos :ℂ⟶ℂ$$
4	3	fdmi	$$⊢\mathrm{dom}\cos =ℂ$$
5	2 4	sseqtri	$$⊢{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq ℂ$$
6	5	sseli	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to x\in ℂ$$
7	6	sincld	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \sin x\in ℂ$$
8	6	coscld	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \cos x\in ℂ$$
9		ffn	$$⊢\cos :ℂ⟶ℂ\to \cos Fnℂ$$
10		elpreima	$$⊢\cos Fnℂ\to \left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(x\in ℂ\wedge \cos x\in \left(ℂ\setminus \left\{0\right\}\right)\right)\right)$$
11	3 9 10	mp2b	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\leftrightarrow \left(x\in ℂ\wedge \cos x\in \left(ℂ\setminus \left\{0\right\}\right)\right)$$
12		eldifsni	$$⊢\cos x\in \left(ℂ\setminus \left\{0\right\}\right)\to \cos x\ne 0$$
13	12	adantl	$$⊢\left(x\in ℂ\wedge \cos x\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to \cos x\ne 0$$
14	11 13	sylbi	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \cos x\ne 0$$
15	7 8 14	divrecd	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \frac{\sin x}{\cos x}=\sin x\left(\frac{1}{\cos x}\right)$$
16	15	mpteq2ia	$$⊢\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{\sin x}{\cos x}\right)=\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\sin x\left(\frac{1}{\cos x}\right)\right)$$
17	1 16	eqtri	$$⊢\tan =\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\sin x\left(\frac{1}{\cos x}\right)\right)$$
18	17	oveq2i	$$⊢ℂ\mathrm{D}\tan =\frac{d\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\sin x\left(\frac{1}{\cos x}\right)\right)}{d_{ℂ}x}$$
19		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
20	19	a1i	$$⊢\top \to ℂ\in \left\{ℝ,ℂ\right\}$$
21		difss	$$⊢ℂ\setminus \left\{0\right\}\subseteq ℂ$$
22		imass2	$$⊢ℂ\setminus \left\{0\right\}\subseteq ℂ\to {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq {\cos }^{-1}\left[ℂ\right]$$
23	21 22	ax-mp	$$⊢{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq {\cos }^{-1}\left[ℂ\right]$$
24		fimacnv	$$⊢\cos :ℂ⟶ℂ\to {\cos }^{-1}\left[ℂ\right]=ℂ$$
25	3 24	ax-mp	$$⊢{\cos }^{-1}\left[ℂ\right]=ℂ$$
26	23 25	sseqtri	$$⊢{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq ℂ$$
27	26	sseli	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to x\in ℂ$$
28	27	sincld	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \sin x\in ℂ$$
29	28	adantl	$$⊢\left(\top \wedge x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)\to \sin x\in ℂ$$
30	8	adantl	$$⊢\left(\top \wedge x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)\to \cos x\in ℂ$$
31		sincl	$$⊢x\in ℂ\to \sin x\in ℂ$$
32	31	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to \sin x\in ℂ$$
33		coscl	$$⊢x\in ℂ\to \cos x\in ℂ$$
34	33	adantl	$$⊢\left(\top \wedge x\in ℂ\right)\to \cos x\in ℂ$$
35		dvsin	$$⊢ℂ\mathrm{D}\sin =\cos$$
36		sinf	$$⊢\sin :ℂ⟶ℂ$$
37	36	a1i	$$⊢\top \to \sin :ℂ⟶ℂ$$
38	37	feqmptd	$$⊢\top \to \sin =\left(x\in ℂ⟼\sin x\right)$$
39	38	oveq2d	$$⊢\top \to ℂ\mathrm{D}\sin =\frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}$$
40	3	a1i	$$⊢\top \to \cos :ℂ⟶ℂ$$
41	40	feqmptd	$$⊢\top \to \cos =\left(x\in ℂ⟼\cos x\right)$$
42	35 39 41	3eqtr3a	$$⊢\top \to \frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\cos x\right)$$
43	26	a1i	$$⊢\top \to {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\subseteq ℂ$$
44		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
45	44	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
46	45	toponrestid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
47		dvtanlem	$$⊢{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
48	47	a1i	$$⊢\top \to {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
49	20 32 34 42 43 46 44 48	dvmptres	$$⊢\top \to \frac{d\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\sin x\right)}{d_{ℂ}x}=\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\cos x\right)$$
50	8 14	reccld	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \frac{1}{\cos x}\in ℂ$$
51	50	adantl	$$⊢\left(\top \wedge x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)\to \frac{1}{\cos x}\in ℂ$$
52		ovexd	$$⊢\left(\top \wedge x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)\to \left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\in \mathrm{V}$$
53	11	simprbi	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \cos x\in \left(ℂ\setminus \left\{0\right\}\right)$$
54	53	adantl	$$⊢\left(\top \wedge x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)\to \cos x\in \left(ℂ\setminus \left\{0\right\}\right)$$
55	29	negcld	$$⊢\left(\top \wedge x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\right)\to -\sin x\in ℂ$$
56		eldifi	$$⊢y\in \left(ℂ\setminus \left\{0\right\}\right)\to y\in ℂ$$
57		eldifsni	$$⊢y\in \left(ℂ\setminus \left\{0\right\}\right)\to y\ne 0$$
58	56 57	reccld	$$⊢y\in \left(ℂ\setminus \left\{0\right\}\right)\to \frac{1}{y}\in ℂ$$
59	58	adantl	$$⊢\left(\top \wedge y\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to \frac{1}{y}\in ℂ$$
60		negex	$$⊢-\frac{1}{y^2}\in \mathrm{V}$$
61	60	a1i	$$⊢\left(\top \wedge y\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to -\frac{1}{y^2}\in \mathrm{V}$$
62	32	negcld	$$⊢\left(\top \wedge x\in ℂ\right)\to -\sin x\in ℂ$$
63	41	oveq2d	$$⊢\top \to ℂ\mathrm{D}\cos =\frac{d\left(x\in ℂ⟼\cos x\right)}{d_{ℂ}x}$$
64		dvcos	$$⊢ℂ\mathrm{D}\cos =\left(x\in ℂ⟼-\sin x\right)$$
65	63 64	eqtr3di	$$⊢\top \to \frac{d\left(x\in ℂ⟼\cos x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼-\sin x\right)$$
66	20 34 62 65 43 46 44 48	dvmptres	$$⊢\top \to \frac{d\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\cos x\right)}{d_{ℂ}x}=\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼-\sin x\right)$$
67		ax-1cn	$$⊢1\in ℂ$$
68		dvrec	$$⊢1\in ℂ\to \frac{d\left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right)}{d_{ℂ}y}=\left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼-\frac{1}{y^2}\right)$$
69	67 68	mp1i	$$⊢\top \to \frac{d\left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{1}{y}\right)}{d_{ℂ}y}=\left(y\in \left(ℂ\setminus \left\{0\right\}\right)⟼-\frac{1}{y^2}\right)$$
70		oveq2	$$⊢y=\cos x\to \frac{1}{y}=\frac{1}{\cos x}$$
71		oveq1	$$⊢y=\cos x\to y^2={\cos x}^2$$
72	71	oveq2d	$$⊢y=\cos x\to \frac{1}{y^2}=\frac{1}{{\cos x}^2}$$
73	72	negeqd	$$⊢y=\cos x\to -\frac{1}{y^2}=-\frac{1}{{\cos x}^2}$$
74	20 20 54 55 59 61 66 69 70 73	dvmptco	$$⊢\top \to \frac{d\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\frac{1}{\cos x}\right)}{d_{ℂ}x}=\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\right)$$
75	20 29 30 49 51 52 74	dvmptmul	$$⊢\top \to \frac{d\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\sin x\left(\frac{1}{\cos x}\right)\right)}{d_{ℂ}x}=\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\cos x\left(\frac{1}{\cos x}\right)+\left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\sin x\right)$$
76	75	mptru	$$⊢\frac{d\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\sin x\left(\frac{1}{\cos x}\right)\right)}{d_{ℂ}x}=\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\cos x\left(\frac{1}{\cos x}\right)+\left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\sin x\right)$$
77		ovex	$$⊢\frac{\sin x}{\cos x}\in \mathrm{V}$$
78	77 1	dmmpti	$$⊢\mathrm{dom}\tan ={\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]$$
79	78	eqcomi	$$⊢{\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]=\mathrm{dom}\tan$$
80	8	sqcld	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to {\cos x}^2\in ℂ$$
81	7	sqcld	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to {\sin x}^2\in ℂ$$
82		sqne0	$$⊢\cos x\in ℂ\to \left({\cos x}^2\ne 0\leftrightarrow \cos x\ne 0\right)$$
83	8 82	syl	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \left({\cos x}^2\ne 0\leftrightarrow \cos x\ne 0\right)$$
84	14 83	mpbird	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to {\cos x}^2\ne 0$$
85	80 81 80 84	divdird	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \frac{{\cos x}^2+{\sin x}^2}{{\cos x}^2}=\left(\frac{{\cos x}^2}{{\cos x}^2}\right)+\left(\frac{{\sin x}^2}{{\cos x}^2}\right)$$
86	80 81	addcomd	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to {\cos x}^2+{\sin x}^2={\sin x}^2+{\cos x}^2$$
87		sincossq	$$⊢x\in ℂ\to {\sin x}^2+{\cos x}^2=1$$
88	6 87	syl	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to {\sin x}^2+{\cos x}^2=1$$
89	86 88	eqtrd	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to {\cos x}^2+{\sin x}^2=1$$
90	89	oveq1d	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \frac{{\cos x}^2+{\sin x}^2}{{\cos x}^2}=\frac{1}{{\cos x}^2}$$
91	85 90	eqtr3d	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \left(\frac{{\cos x}^2}{{\cos x}^2}\right)+\left(\frac{{\sin x}^2}{{\cos x}^2}\right)=\frac{1}{{\cos x}^2}$$
92	8 14	recidd	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \cos x\left(\frac{1}{\cos x}\right)=1$$
93	80 84	dividd	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \frac{{\cos x}^2}{{\cos x}^2}=1$$
94	92 93	eqtr4d	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \cos x\left(\frac{1}{\cos x}\right)=\frac{{\cos x}^2}{{\cos x}^2}$$
95	7 7 80 84	div23d	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \frac{\sin x\sin x}{{\cos x}^2}=\left(\frac{\sin x}{{\cos x}^2}\right)\sin x$$
96	7	sqvald	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to {\sin x}^2=\sin x\sin x$$
97	96	oveq1d	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \frac{{\sin x}^2}{{\cos x}^2}=\frac{\sin x\sin x}{{\cos x}^2}$$
98	80 84	reccld	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \frac{1}{{\cos x}^2}\in ℂ$$
99	98 7	mul2negd	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)=\left(\frac{1}{{\cos x}^2}\right)\sin x$$
100	7 80 84	divrec2d	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \frac{\sin x}{{\cos x}^2}=\left(\frac{1}{{\cos x}^2}\right)\sin x$$
101	99 100	eqtr4d	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)=\frac{\sin x}{{\cos x}^2}$$
102	101	oveq1d	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\sin x=\left(\frac{\sin x}{{\cos x}^2}\right)\sin x$$
103	95 97 102	3eqtr4rd	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\sin x=\frac{{\sin x}^2}{{\cos x}^2}$$
104	94 103	oveq12d	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \cos x\left(\frac{1}{\cos x}\right)+\left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\sin x=\left(\frac{{\cos x}^2}{{\cos x}^2}\right)+\left(\frac{{\sin x}^2}{{\cos x}^2}\right)$$
105		2nn0	$$⊢2\in {\mathbb{N}}_0$$
106		expneg	$$⊢\left(\cos x\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to {\cos x}^{-2}=\frac{1}{{\cos x}^2}$$
107	8 105 106	sylancl	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to {\cos x}^{-2}=\frac{1}{{\cos x}^2}$$
108	91 104 107	3eqtr4d	$$⊢x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\to \cos x\left(\frac{1}{\cos x}\right)+\left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\sin x={\cos x}^{-2}$$
109	108	rgen	$$⊢\forall x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\cos x\left(\frac{1}{\cos x}\right)+\left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\sin x={\cos x}^{-2}$$
110		mpteq12	$$⊢\left({\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]=\mathrm{dom}\tan \wedge \forall x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]\cos x\left(\frac{1}{\cos x}\right)+\left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\sin x={\cos x}^{-2}\right)\to \left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\cos x\left(\frac{1}{\cos x}\right)+\left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\sin x\right)=\left(x\in \mathrm{dom}\tan ⟼{\cos x}^{-2}\right)$$
111	79 109 110	mp2an	$$⊢\left(x\in {\cos }^{-1}\left[ℂ\setminus \left\{0\right\}\right]⟼\cos x\left(\frac{1}{\cos x}\right)+\left(-\frac{1}{{\cos x}^2}\right)\left(-\sin x\right)\sin x\right)=\left(x\in \mathrm{dom}\tan ⟼{\cos x}^{-2}\right)$$
112	18 76 111	3eqtri	$$⊢ℂ\mathrm{D}\tan =\left(x\in \mathrm{dom}\tan ⟼{\cos x}^{-2}\right)$$