Metamath Proof Explorer

Theorem dvcsc

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

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

Proof

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