Metamath Proof Explorer

Theorem dvcot

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

Ref Expression
Assertion dvcot 
|- ( CC _D cot ) = ( x e. dom cot |-> -u ( ( csc ` x ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 df-cot 
 |-  cot = ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( ( cos ` x ) / ( sin ` x ) ) )
2 1 oveq2i 
 |-  ( CC _D cot ) = ( CC _D ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( ( cos ` x ) / ( sin ` x ) ) ) )
3 cnelprrecn 
 |-  CC e. { RR , CC }
4 3 a1i 
 |-  ( T. -> CC e. { RR , CC } )
5 elrabi 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> x e. CC )
6 coscl 
 |-  ( x e. CC -> ( cos ` x ) e. CC )
7 5 6 syl 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( cos ` x ) e. CC )
8 7 adantl 
 |-  ( ( T. /\ x e. { y e. CC | ( sin ` y ) =/= 0 } ) -> ( cos ` x ) e. CC )
9 sincl 
 |-  ( x e. CC -> ( sin ` x ) e. CC )
10 5 9 syl 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( sin ` x ) e. CC )
11 10 negcld 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> -u ( sin ` x ) e. CC )
12 11 adantl 
 |-  ( ( T. /\ x e. { y e. CC | ( sin ` y ) =/= 0 } ) -> -u ( sin ` x ) e. CC )
13 6 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( cos ` x ) e. CC )
14 9 negcld 
 |-  ( x e. CC -> -u ( sin ` x ) e. CC )
15 14 adantl 
 |-  ( ( T. /\ x e. CC ) -> -u ( sin ` x ) e. CC )
16 cosf 
 |-  cos : CC --> CC
17 16 a1i 
 |-  ( T. -> cos : CC --> CC )
18 17 feqmptd 
 |-  ( T. -> cos = ( x e. CC |-> ( cos ` x ) ) )
19 18 mptru 
 |-  cos = ( x e. CC |-> ( cos ` x ) )
20 19 oveq2i 
 |-  ( CC _D cos ) = ( CC _D ( x e. CC |-> ( cos ` x ) ) )
21 dvcos 
 |-  ( CC _D cos ) = ( x e. CC |-> -u ( sin ` x ) )
22 20 21 eqtr3i 
 |-  ( CC _D ( x e. CC |-> ( cos ` x ) ) ) = ( x e. CC |-> -u ( sin ` x ) )
23 22 a1i 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( cos ` x ) ) ) = ( x e. CC |-> -u ( sin ` x ) ) )
24 ssrab2 
 |-  { y e. CC | ( sin ` y ) =/= 0 } C_ CC
25 24 a1i 
 |-  ( T. -> { y e. CC | ( sin ` y ) =/= 0 } C_ CC )
26 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
27 26 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
28 27 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
29 sincn 
 |-  sin e. ( CC -cn-> CC )
30 ssid 
 |-  CC C_ CC
31 26 28 28 cncfcn 
 |-  ( ( CC C_ CC /\ CC C_ CC ) -> ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
32 30 30 31 mp2an 
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
33 29 32 eleqtri 
 |-  sin e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
34 cnn0opn 
 |-  ( CC \ { 0 } ) e. ( TopOpen ` CCfld )
35 cnima 
 |-  ( ( sin e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) /\ ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) ) -> ( `' sin " ( CC \ { 0 } ) ) e. ( TopOpen ` CCfld ) )
36 33 34 35 mp2an 
 |-  ( `' sin " ( CC \ { 0 } ) ) e. ( TopOpen ` CCfld )
37 sincl 
 |-  ( y e. CC -> ( sin ` y ) e. CC )
38 eldifsn 
 |-  ( ( sin ` y ) e. ( CC \ { 0 } ) <-> ( ( sin ` y ) e. CC /\ ( sin ` y ) =/= 0 ) )
39 38 baib 
 |-  ( ( sin ` y ) e. CC -> ( ( sin ` y ) e. ( CC \ { 0 } ) <-> ( sin ` y ) =/= 0 ) )
40 37 39 syl 
 |-  ( y e. CC -> ( ( sin ` y ) e. ( CC \ { 0 } ) <-> ( sin ` y ) =/= 0 ) )
41 40 bicomd 
 |-  ( y e. CC -> ( ( sin ` y ) =/= 0 <-> ( sin ` y ) e. ( CC \ { 0 } ) ) )
42 41 rabbiia 
 |-  { y e. CC | ( sin ` y ) =/= 0 } = { y e. CC | ( sin ` y ) e. ( CC \ { 0 } ) }
43 sinf 
 |-  sin : CC --> CC
44 43 a1i 
 |-  ( T. -> sin : CC --> CC )
45 44 feqmptd 
 |-  ( T. -> sin = ( y e. CC |-> ( sin ` y ) ) )
46 45 mptru 
 |-  sin = ( y e. CC |-> ( sin ` y ) )
47 46 mptpreima 
 |-  ( `' sin " ( CC \ { 0 } ) ) = { y e. CC | ( sin ` y ) e. ( CC \ { 0 } ) }
48 42 47 eqtr4i 
 |-  { y e. CC | ( sin ` y ) =/= 0 } = ( `' sin " ( CC \ { 0 } ) )
49 48 eleq1i 
 |-  ( { y e. CC | ( sin ` y ) =/= 0 } e. ( TopOpen ` CCfld ) <-> ( `' sin " ( CC \ { 0 } ) ) e. ( TopOpen ` CCfld ) )
50 36 49 mpbir 
 |-  { y e. CC | ( sin ` y ) =/= 0 } e. ( TopOpen ` CCfld )
51 50 a1i 
 |-  ( T. -> { y e. CC | ( sin ` y ) =/= 0 } e. ( TopOpen ` CCfld ) )
52 4 13 15 23 25 28 26 51 dvmptres 
 |-  ( T. -> ( CC _D ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( cos ` x ) ) ) = ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> -u ( sin ` x ) ) )
53 fveq2 
 |-  ( y = x -> ( sin ` y ) = ( sin ` x ) )
54 53 neeq1d 
 |-  ( y = x -> ( ( sin ` y ) =/= 0 <-> ( sin ` x ) =/= 0 ) )
55 54 elrab 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } <-> ( x e. CC /\ ( sin ` x ) =/= 0 ) )
56 55 simprbi 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( sin ` x ) =/= 0 )
57 10 56 jca 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( sin ` x ) e. CC /\ ( sin ` x ) =/= 0 ) )
58 eldifsn 
 |-  ( ( sin ` x ) e. ( CC \ { 0 } ) <-> ( ( sin ` x ) e. CC /\ ( sin ` x ) =/= 0 ) )
59 57 58 sylibr 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( sin ` x ) e. ( CC \ { 0 } ) )
60 59 adantl 
 |-  ( ( T. /\ x e. { y e. CC | ( sin ` y ) =/= 0 } ) -> ( sin ` x ) e. ( CC \ { 0 } ) )
61 9 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( sin ` x ) e. CC )
62 44 feqmptd 
 |-  ( T. -> sin = ( x e. CC |-> ( sin ` x ) ) )
63 62 mptru 
 |-  sin = ( x e. CC |-> ( sin ` x ) )
64 63 oveq2i 
 |-  ( CC _D sin ) = ( CC _D ( x e. CC |-> ( sin ` x ) ) )
65 dvsin 
 |-  ( CC _D sin ) = cos
66 64 65 eqtr3i 
 |-  ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = cos
67 66 19 eqtri 
 |-  ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = ( x e. CC |-> ( cos ` x ) )
68 67 a1i 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = ( x e. CC |-> ( cos ` x ) ) )
69 4 61 13 68 25 28 26 51 dvmptres 
 |-  ( T. -> ( CC _D ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( sin ` x ) ) ) = ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( cos ` x ) ) )
70 4 8 12 52 60 8 69 dvmptdiv 
 |-  ( T. -> ( CC _D ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( ( cos ` x ) / ( sin ` x ) ) ) ) = ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( ( ( -u ( sin ` x ) x. ( sin ` x ) ) - ( ( cos ` x ) x. ( cos ` x ) ) ) / ( ( sin ` x ) ^ 2 ) ) ) )
71 70 mptru 
 |-  ( CC _D ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( ( cos ` x ) / ( sin ` x ) ) ) ) = ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( ( ( -u ( sin ` x ) x. ( sin ` x ) ) - ( ( cos ` x ) x. ( cos ` x ) ) ) / ( ( sin ` x ) ^ 2 ) ) )
72 10 10 mulneg1d 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( -u ( sin ` x ) x. ( sin ` x ) ) = -u ( ( sin ` x ) x. ( sin ` x ) ) )
73 sqval 
 |-  ( ( sin ` x ) e. CC -> ( ( sin ` x ) ^ 2 ) = ( ( sin ` x ) x. ( sin ` x ) ) )
74 10 73 syl 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( sin ` x ) ^ 2 ) = ( ( sin ` x ) x. ( sin ` x ) ) )
75 74 eqcomd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( sin ` x ) x. ( sin ` x ) ) = ( ( sin ` x ) ^ 2 ) )
76 75 negeqd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> -u ( ( sin ` x ) x. ( sin ` x ) ) = -u ( ( sin ` x ) ^ 2 ) )
77 72 76 eqtrd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( -u ( sin ` x ) x. ( sin ` x ) ) = -u ( ( sin ` x ) ^ 2 ) )
78 sqval 
 |-  ( ( cos ` x ) e. CC -> ( ( cos ` x ) ^ 2 ) = ( ( cos ` x ) x. ( cos ` x ) ) )
79 7 78 syl 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( cos ` x ) ^ 2 ) = ( ( cos ` x ) x. ( cos ` x ) ) )
80 79 eqcomd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( cos ` x ) x. ( cos ` x ) ) = ( ( cos ` x ) ^ 2 ) )
81 77 80 oveq12d 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( -u ( sin ` x ) x. ( sin ` x ) ) - ( ( cos ` x ) x. ( cos ` x ) ) ) = ( -u ( ( sin ` x ) ^ 2 ) - ( ( cos ` x ) ^ 2 ) ) )
82 10 sqcld 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( sin ` x ) ^ 2 ) e. CC )
83 7 sqcld 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( cos ` x ) ^ 2 ) e. CC )
84 negdi2 
 |-  ( ( ( ( sin ` x ) ^ 2 ) e. CC /\ ( ( cos ` x ) ^ 2 ) e. CC ) -> -u ( ( ( sin ` x ) ^ 2 ) + ( ( cos ` x ) ^ 2 ) ) = ( -u ( ( sin ` x ) ^ 2 ) - ( ( cos ` x ) ^ 2 ) ) )
85 82 83 84 syl2anc 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> -u ( ( ( sin ` x ) ^ 2 ) + ( ( cos ` x ) ^ 2 ) ) = ( -u ( ( sin ` x ) ^ 2 ) - ( ( cos ` x ) ^ 2 ) ) )
86 85 eqcomd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( -u ( ( sin ` x ) ^ 2 ) - ( ( cos ` x ) ^ 2 ) ) = -u ( ( ( sin ` x ) ^ 2 ) + ( ( cos ` x ) ^ 2 ) ) )
87 sincossq 
 |-  ( x e. CC -> ( ( ( sin ` x ) ^ 2 ) + ( ( cos ` x ) ^ 2 ) ) = 1 )
88 5 87 syl 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( ( sin ` x ) ^ 2 ) + ( ( cos ` x ) ^ 2 ) ) = 1 )
89 88 negeqd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> -u ( ( ( sin ` x ) ^ 2 ) + ( ( cos ` x ) ^ 2 ) ) = -u 1 )
90 86 89 eqtrd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( -u ( ( sin ` x ) ^ 2 ) - ( ( cos ` x ) ^ 2 ) ) = -u 1 )
91 81 90 eqtrd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( -u ( sin ` x ) x. ( sin ` x ) ) - ( ( cos ` x ) x. ( cos ` x ) ) ) = -u 1 )
92 91 oveq1d 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( ( -u ( sin ` x ) x. ( sin ` x ) ) - ( ( cos ` x ) x. ( cos ` x ) ) ) / ( ( sin ` x ) ^ 2 ) ) = ( -u 1 / ( ( sin ` x ) ^ 2 ) ) )
93 ax-1cn 
 |-  1 e. CC
94 93 a1i 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> 1 e. CC )
95 sqne0 
 |-  ( ( sin ` x ) e. CC -> ( ( ( sin ` x ) ^ 2 ) =/= 0 <-> ( sin ` x ) =/= 0 ) )
96 10 95 syl 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( ( sin ` x ) ^ 2 ) =/= 0 <-> ( sin ` x ) =/= 0 ) )
97 56 96 mpbird 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( sin ` x ) ^ 2 ) =/= 0 )
98 divneg 
 |-  ( ( 1 e. CC /\ ( ( sin ` x ) ^ 2 ) e. CC /\ ( ( sin ` x ) ^ 2 ) =/= 0 ) -> -u ( 1 / ( ( sin ` x ) ^ 2 ) ) = ( -u 1 / ( ( sin ` x ) ^ 2 ) ) )
99 94 82 97 98 syl3anc 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> -u ( 1 / ( ( sin ` x ) ^ 2 ) ) = ( -u 1 / ( ( sin ` x ) ^ 2 ) ) )
100 99 eqcomd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( -u 1 / ( ( sin ` x ) ^ 2 ) ) = -u ( 1 / ( ( sin ` x ) ^ 2 ) ) )
101 92 100 eqtrd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( ( -u ( sin ` x ) x. ( sin ` x ) ) - ( ( cos ` x ) x. ( cos ` x ) ) ) / ( ( sin ` x ) ^ 2 ) ) = -u ( 1 / ( ( sin ` x ) ^ 2 ) ) )
102 cscval 
 |-  ( ( x e. CC /\ ( sin ` x ) =/= 0 ) -> ( csc ` x ) = ( 1 / ( sin ` x ) ) )
103 55 102 sylbi 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( csc ` x ) = ( 1 / ( sin ` x ) ) )
104 103 oveq1d 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( csc ` x ) ^ 2 ) = ( ( 1 / ( sin ` x ) ) ^ 2 ) )
105 sqdiv 
 |-  ( ( 1 e. CC /\ ( sin ` x ) e. CC /\ ( sin ` x ) =/= 0 ) -> ( ( 1 / ( sin ` x ) ) ^ 2 ) = ( ( 1 ^ 2 ) / ( ( sin ` x ) ^ 2 ) ) )
106 94 10 56 105 syl3anc 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( 1 / ( sin ` x ) ) ^ 2 ) = ( ( 1 ^ 2 ) / ( ( sin ` x ) ^ 2 ) ) )
107 sq1 
 |-  ( 1 ^ 2 ) = 1
108 107 a1i 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( 1 ^ 2 ) = 1 )
109 108 oveq1d 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( 1 ^ 2 ) / ( ( sin ` x ) ^ 2 ) ) = ( 1 / ( ( sin ` x ) ^ 2 ) ) )
110 106 109 eqtrd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( 1 / ( sin ` x ) ) ^ 2 ) = ( 1 / ( ( sin ` x ) ^ 2 ) ) )
111 104 110 eqtrd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( csc ` x ) ^ 2 ) = ( 1 / ( ( sin ` x ) ^ 2 ) ) )
112 111 eqcomd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( 1 / ( ( sin ` x ) ^ 2 ) ) = ( ( csc ` x ) ^ 2 ) )
113 112 negeqd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> -u ( 1 / ( ( sin ` x ) ^ 2 ) ) = -u ( ( csc ` x ) ^ 2 ) )
114 101 113 eqtrd 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( ( -u ( sin ` x ) x. ( sin ` x ) ) - ( ( cos ` x ) x. ( cos ` x ) ) ) / ( ( sin ` x ) ^ 2 ) ) = -u ( ( csc ` x ) ^ 2 ) )
115 114 mpteq2ia 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( ( ( -u ( sin ` x ) x. ( sin ` x ) ) - ( ( cos ` x ) x. ( cos ` x ) ) ) / ( ( sin ` x ) ^ 2 ) ) ) = ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> -u ( ( csc ` x ) ^ 2 ) )
116 7 10 56 divcld 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } -> ( ( cos ` x ) / ( sin ` x ) ) e. CC )
117 1 116 fmpti 
 |-  cot : { y e. CC | ( sin ` y ) =/= 0 } --> CC
118 117 fdmi 
 |-  dom cot = { y e. CC | ( sin ` y ) =/= 0 }
119 118 eqcomi 
 |-  { y e. CC | ( sin ` y ) =/= 0 } = dom cot
120 119 mpteq1i 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> -u ( ( csc ` x ) ^ 2 ) ) = ( x e. dom cot |-> -u ( ( csc ` x ) ^ 2 ) )
121 115 120 eqtri 
 |-  ( x e. { y e. CC | ( sin ` y ) =/= 0 } |-> ( ( ( -u ( sin ` x ) x. ( sin ` x ) ) - ( ( cos ` x ) x. ( cos ` x ) ) ) / ( ( sin ` x ) ^ 2 ) ) ) = ( x e. dom cot |-> -u ( ( csc ` x ) ^ 2 ) )
122 2 71 121 3eqtri 
 |-  ( CC _D cot ) = ( x e. dom cot |-> -u ( ( csc ` x ) ^ 2 ) )