Metamath Proof Explorer

Theorem dvsec

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

Ref Expression
Assertion dvsec 
|- ( CC _D sec ) = ( x e. dom sec |-> ( ( sec ` x ) x. ( tan ` x ) ) )

Proof

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