Metamath Proof Explorer


Theorem dvtan

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

Ref Expression
Assertion dvtan D tan = x dom tan cos x 2

Proof

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