Metamath Proof Explorer

Theorem dvsec

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

Ref Expression
Assertion dvsec ( ℂ D sec ) = ( 𝑥 ∈ dom sec ↦ ( ( sec ‘ 𝑥 ) · ( tan ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 df-sec ⊢ sec = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( 1 / ( cos ‘ 𝑥 ) ) )
2 1 oveq2i ⊢ ( ℂ D sec ) = ( ℂ D ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( 1 / ( cos ‘ 𝑥 ) ) ) )
3 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
4 3 a1i ⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } )
5 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
6 elrabi ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → 𝑥 ∈ ℂ )
7 coscl ⊢ ( 𝑥 ∈ ℂ → ( cos ‘ 𝑥 ) ∈ ℂ )
8 6 7 syl ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( cos ‘ 𝑥 ) ∈ ℂ )
9 fveq2 ⊢ ( 𝑦 = 𝑥 → ( cos ‘ 𝑦 ) = ( cos ‘ 𝑥 ) )
10 9 neeq1d ⊢ ( 𝑦 = 𝑥 → ( ( cos ‘ 𝑦 ) ≠ 0 ↔ ( cos ‘ 𝑥 ) ≠ 0 ) )
11 10 elrab ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↔ ( 𝑥 ∈ ℂ ∧ ( cos ‘ 𝑥 ) ≠ 0 ) )
12 11 simprbi ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( cos ‘ 𝑥 ) ≠ 0 )
13 8 12 jca ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( cos ‘ 𝑥 ) ∈ ℂ ∧ ( cos ‘ 𝑥 ) ≠ 0 ) )
14 eldifsn ⊢ ( ( cos ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( cos ‘ 𝑥 ) ∈ ℂ ∧ ( cos ‘ 𝑥 ) ≠ 0 ) )
15 13 14 sylibr ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( cos ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
16 15 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ) → ( cos ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
17 sincl ⊢ ( 𝑥 ∈ ℂ → ( sin ‘ 𝑥 ) ∈ ℂ )
18 6 17 syl ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( sin ‘ 𝑥 ) ∈ ℂ )
19 18 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ) → ( sin ‘ 𝑥 ) ∈ ℂ )
20 19 negcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ) → - ( sin ‘ 𝑥 ) ∈ ℂ )
21 7 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( cos ‘ 𝑥 ) ∈ ℂ )
22 17 negcld ⊢ ( 𝑥 ∈ ℂ → - ( sin ‘ 𝑥 ) ∈ ℂ )
23 22 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - ( sin ‘ 𝑥 ) ∈ ℂ )
24 cosf ⊢ cos : ℂ ⟶ ℂ
25 24 a1i ⊢ ( ⊤ → cos : ℂ ⟶ ℂ )
26 25 feqmptd ⊢ ( ⊤ → cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
27 26 mptru ⊢ cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) )
28 27 oveq2i ⊢ ( ℂ D cos ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
29 dvcos ⊢ ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) )
30 28 29 eqtr3i ⊢ ( ℂ D ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) )
31 30 a1i ⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) )
32 ssrab2 ⊢ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ⊆ ℂ
33 32 a1i ⊢ ( ⊤ → { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ⊆ ℂ )
34 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
35 34 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
36 35 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
37 coscn ⊢ cos ∈ ( ℂ –cn→ ℂ )
38 ssid ⊢ ℂ ⊆ ℂ
39 34 36 36 cncfcn ⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
40 38 38 39 mp2an ⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
41 37 40 eleqtri ⊢ cos ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
42 cnn0opn ⊢ ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld )
43 cnima ⊢ ( ( cos ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) ∧ ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld ) ) → ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ∈ ( TopOpen ‘ ℂfld ) )
44 41 42 43 mp2an ⊢ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ∈ ( TopOpen ‘ ℂfld )
45 coscl ⊢ ( 𝑦 ∈ ℂ → ( cos ‘ 𝑦 ) ∈ ℂ )
46 eldifsn ⊢ ( ( cos ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( cos ‘ 𝑦 ) ∈ ℂ ∧ ( cos ‘ 𝑦 ) ≠ 0 ) )
47 46 baib ⊢ ( ( cos ‘ 𝑦 ) ∈ ℂ → ( ( cos ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( cos ‘ 𝑦 ) ≠ 0 ) )
48 45 47 syl ⊢ ( 𝑦 ∈ ℂ → ( ( cos ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( cos ‘ 𝑦 ) ≠ 0 ) )
49 48 bicomd ⊢ ( 𝑦 ∈ ℂ → ( ( cos ‘ 𝑦 ) ≠ 0 ↔ ( cos ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ) )
50 49 rabbiia ⊢ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } = { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) }
51 25 feqmptd ⊢ ( ⊤ → cos = ( 𝑦 ∈ ℂ ↦ ( cos ‘ 𝑦 ) ) )
52 51 mptru ⊢ cos = ( 𝑦 ∈ ℂ ↦ ( cos ‘ 𝑦 ) )
53 52 mptpreima ⊢ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) = { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ∈ ( ℂ ∖ { 0 } ) }
54 50 53 eqtr4i ⊢ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } = ( ◡ cos “ ( ℂ ∖ { 0 } ) )
55 54 eleq1i ⊢ ( { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ∈ ( TopOpen ‘ ℂfld ) ↔ ( ◡ cos “ ( ℂ ∖ { 0 } ) ) ∈ ( TopOpen ‘ ℂfld ) )
56 44 55 mpbir ⊢ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ∈ ( TopOpen ‘ ℂfld )
57 56 a1i ⊢ ( ⊤ → { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ∈ ( TopOpen ‘ ℂfld ) )
58 4 21 23 31 33 36 34 57 dvmptres ⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( cos ‘ 𝑥 ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ - ( sin ‘ 𝑥 ) ) )
59 4 5 16 20 58 dvrecg ⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( 1 / ( cos ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ - ( ( 1 · - ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) ) )
60 59 mptru ⊢ ( ℂ D ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( 1 / ( cos ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ - ( ( 1 · - ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
61 18 negcld ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → - ( sin ‘ 𝑥 ) ∈ ℂ )
62 61 mullidd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( 1 · - ( sin ‘ 𝑥 ) ) = - ( sin ‘ 𝑥 ) )
63 sqval ⊢ ( ( cos ‘ 𝑥 ) ∈ ℂ → ( ( cos ‘ 𝑥 ) ↑ 2 ) = ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) )
64 8 63 syl ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( cos ‘ 𝑥 ) ↑ 2 ) = ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) )
65 62 64 oveq12d ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( 1 · - ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = ( - ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) )
66 65 negeqd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → - ( ( 1 · - ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = - ( - ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) )
67 8 8 mulcld ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ∈ ℂ )
68 8 8 12 12 mulne0d ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ≠ 0 )
69 61 67 68 divnegd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → - ( - ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) = ( - - ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) )
70 18 negnegd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → - - ( sin ‘ 𝑥 ) = ( sin ‘ 𝑥 ) )
71 70 oveq1d ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( - - ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) = ( ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) )
72 69 71 eqtrd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → - ( - ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) = ( ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) )
73 66 72 eqtrd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → - ( ( 1 · - ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = ( ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) )
74 ax-1cn ⊢ 1 ∈ ℂ
75 74 a1i ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → 1 ∈ ℂ )
76 75 8 18 8 12 12 divmuldivd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( 1 / ( cos ‘ 𝑥 ) ) · ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) ) = ( ( 1 · ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) )
77 18 mullidd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( 1 · ( sin ‘ 𝑥 ) ) = ( sin ‘ 𝑥 ) )
78 77 oveq1d ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( 1 · ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) = ( ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) )
79 76 78 eqtrd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( 1 / ( cos ‘ 𝑥 ) ) · ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) ) = ( ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) )
80 79 eqcomd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) · ( cos ‘ 𝑥 ) ) ) = ( ( 1 / ( cos ‘ 𝑥 ) ) · ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) ) )
81 73 80 eqtrd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → - ( ( 1 · - ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = ( ( 1 / ( cos ‘ 𝑥 ) ) · ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) ) )
82 secval ⊢ ( ( 𝑥 ∈ ℂ ∧ ( cos ‘ 𝑥 ) ≠ 0 ) → ( sec ‘ 𝑥 ) = ( 1 / ( cos ‘ 𝑥 ) ) )
83 11 82 sylbi ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( sec ‘ 𝑥 ) = ( 1 / ( cos ‘ 𝑥 ) ) )
84 83 eqcomd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( 1 / ( cos ‘ 𝑥 ) ) = ( sec ‘ 𝑥 ) )
85 tanval ⊢ ( ( 𝑥 ∈ ℂ ∧ ( cos ‘ 𝑥 ) ≠ 0 ) → ( tan ‘ 𝑥 ) = ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )
86 11 85 sylbi ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( tan ‘ 𝑥 ) = ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )
87 86 eqcomd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) = ( tan ‘ 𝑥 ) )
88 84 87 oveq12d ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( ( 1 / ( cos ‘ 𝑥 ) ) · ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) ) = ( ( sec ‘ 𝑥 ) · ( tan ‘ 𝑥 ) ) )
89 81 88 eqtrd ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → - ( ( 1 · - ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = ( ( sec ‘ 𝑥 ) · ( tan ‘ 𝑥 ) ) )
90 89 mpteq2ia ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ - ( ( 1 · - ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( ( sec ‘ 𝑥 ) · ( tan ‘ 𝑥 ) ) )
91 75 8 12 divcld ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } → ( 1 / ( cos ‘ 𝑥 ) ) ∈ ℂ )
92 1 91 fmpti ⊢ sec : { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ⟶ ℂ
93 92 fdmi ⊢ dom sec = { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 }
94 93 eqcomi ⊢ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } = dom sec
95 94 mpteq1i ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( ( sec ‘ 𝑥 ) · ( tan ‘ 𝑥 ) ) ) = ( 𝑥 ∈ dom sec ↦ ( ( sec ‘ 𝑥 ) · ( tan ‘ 𝑥 ) ) )
96 90 95 eqtri ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ - ( ( 1 · - ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) ) = ( 𝑥 ∈ dom sec ↦ ( ( sec ‘ 𝑥 ) · ( tan ‘ 𝑥 ) ) )
97 60 96 eqtri ⊢ ( ℂ D ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ( cos ‘ 𝑦 ) ≠ 0 } ↦ ( 1 / ( cos ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ dom sec ↦ ( ( sec ‘ 𝑥 ) · ( tan ‘ 𝑥 ) ) )
98 2 97 eqtri ⊢ ( ℂ D sec ) = ( 𝑥 ∈ dom sec ↦ ( ( sec ‘ 𝑥 ) · ( tan ‘ 𝑥 ) ) )