Metamath Proof Explorer

Theorem dvtan

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

Ref Expression
Assertion dvtan 
|- ( CC _D tan ) = ( x e. dom tan |-> ( ( cos ` x ) ^ -u 2 ) )

Proof

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