Metamath Proof Explorer


Theorem dvtan

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

Ref Expression
Assertion dvtan ( ℂ D tan ) = ( 𝑥 ∈ dom tan ↦ ( ( cos ‘ 𝑥 ) ↑ - 2 ) )

Proof

Step Hyp Ref Expression
1 df-tan tan = ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) )
2 cnvimass ( cos “ ( ℂ ∖ { 0 } ) ) ⊆ dom cos
3 cosf cos : ℂ ⟶ ℂ
4 3 fdmi dom cos = ℂ
5 2 4 sseqtri ( cos “ ( ℂ ∖ { 0 } ) ) ⊆ ℂ
6 5 sseli ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
7 6 sincld ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( sin ‘ 𝑥 ) ∈ ℂ )
8 6 coscld ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( cos ‘ 𝑥 ) ∈ ℂ )
9 ffn ( cos : ℂ ⟶ ℂ → cos Fn ℂ )
10 elpreima ( cos Fn ℂ → ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( cos ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) ) )
11 3 9 10 mp2b ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( cos ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) )
12 eldifsni ( ( cos ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) → ( cos ‘ 𝑥 ) ≠ 0 )
13 12 adantl ( ( 𝑥 ∈ ℂ ∧ ( cos ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) → ( cos ‘ 𝑥 ) ≠ 0 )
14 11 13 sylbi ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( cos ‘ 𝑥 ) ≠ 0 )
15 7 8 14 divrecd ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) = ( ( sin ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) )
16 15 mpteq2ia ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) )
17 1 16 eqtri tan = ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) )
18 17 oveq2i ( ℂ D tan ) = ( ℂ D ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) ) )
19 cnelprrecn ℂ ∈ { ℝ , ℂ }
20 19 a1i ( ⊤ → ℂ ∈ { ℝ , ℂ } )
21 difss ( ℂ ∖ { 0 } ) ⊆ ℂ
22 imass2 ( ( ℂ ∖ { 0 } ) ⊆ ℂ → ( cos “ ( ℂ ∖ { 0 } ) ) ⊆ ( cos “ ℂ ) )
23 21 22 ax-mp ( cos “ ( ℂ ∖ { 0 } ) ) ⊆ ( cos “ ℂ )
24 fimacnv ( cos : ℂ ⟶ ℂ → ( cos “ ℂ ) = ℂ )
25 3 24 ax-mp ( cos “ ℂ ) = ℂ
26 23 25 sseqtri ( cos “ ( ℂ ∖ { 0 } ) ) ⊆ ℂ
27 26 sseli ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
28 27 sincld ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( sin ‘ 𝑥 ) ∈ ℂ )
29 28 adantl ( ( ⊤ ∧ 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ) → ( sin ‘ 𝑥 ) ∈ ℂ )
30 8 adantl ( ( ⊤ ∧ 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ) → ( cos ‘ 𝑥 ) ∈ ℂ )
31 sincl ( 𝑥 ∈ ℂ → ( sin ‘ 𝑥 ) ∈ ℂ )
32 31 adantl ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( sin ‘ 𝑥 ) ∈ ℂ )
33 coscl ( 𝑥 ∈ ℂ → ( cos ‘ 𝑥 ) ∈ ℂ )
34 33 adantl ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( cos ‘ 𝑥 ) ∈ ℂ )
35 dvsin ( ℂ D sin ) = cos
36 sinf sin : ℂ ⟶ ℂ
37 36 a1i ( ⊤ → sin : ℂ ⟶ ℂ )
38 37 feqmptd ( ⊤ → sin = ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) )
39 38 oveq2d ( ⊤ → ( ℂ D sin ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) ) )
40 3 a1i ( ⊤ → cos : ℂ ⟶ ℂ )
41 40 feqmptd ( ⊤ → cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
42 35 39 41 3eqtr3a ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
43 26 a1i ( ⊤ → ( cos “ ( ℂ ∖ { 0 } ) ) ⊆ ℂ )
44 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
45 44 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
46 45 toponrestid ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
47 dvtanlem ( cos “ ( ℂ ∖ { 0 } ) ) ∈ ( TopOpen ‘ ℂfld )
48 47 a1i ( ⊤ → ( cos “ ( ℂ ∖ { 0 } ) ) ∈ ( TopOpen ‘ ℂfld ) )
49 20 32 34 42 43 46 44 48 dvmptres ( ⊤ → ( ℂ D ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( sin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( cos ‘ 𝑥 ) ) )
50 8 14 reccld ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( 1 / ( cos ‘ 𝑥 ) ) ∈ ℂ )
51 50 adantl ( ( ⊤ ∧ 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ) → ( 1 / ( cos ‘ 𝑥 ) ) ∈ ℂ )
52 ovexd ( ( ⊤ ∧ 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ) → ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) ∈ V )
53 11 simprbi ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( cos ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
54 53 adantl ( ( ⊤ ∧ 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ) → ( cos ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
55 29 negcld ( ( ⊤ ∧ 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ) → - ( sin ‘ 𝑥 ) ∈ ℂ )
56 eldifi ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ∈ ℂ )
57 eldifsni ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ≠ 0 )
58 56 57 reccld ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑦 ) ∈ ℂ )
59 58 adantl ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 1 / 𝑦 ) ∈ ℂ )
60 negex - ( 1 / ( 𝑦 ↑ 2 ) ) ∈ V
61 60 a1i ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → - ( 1 / ( 𝑦 ↑ 2 ) ) ∈ V )
62 32 negcld ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - ( sin ‘ 𝑥 ) ∈ ℂ )
63 41 oveq2d ( ⊤ → ( ℂ D cos ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ) )
64 dvcos ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) )
65 63 64 eqtr3di ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) )
66 20 34 62 65 43 46 44 48 dvmptres ( ⊤ → ( ℂ D ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( cos ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ - ( sin ‘ 𝑥 ) ) )
67 ax-1cn 1 ∈ ℂ
68 dvrec ( 1 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 1 / ( 𝑦 ↑ 2 ) ) ) )
69 67 68 mp1i ( ⊤ → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 1 / ( 𝑦 ↑ 2 ) ) ) )
70 oveq2 ( 𝑦 = ( cos ‘ 𝑥 ) → ( 1 / 𝑦 ) = ( 1 / ( cos ‘ 𝑥 ) ) )
71 oveq1 ( 𝑦 = ( cos ‘ 𝑥 ) → ( 𝑦 ↑ 2 ) = ( ( cos ‘ 𝑥 ) ↑ 2 ) )
72 71 oveq2d ( 𝑦 = ( cos ‘ 𝑥 ) → ( 1 / ( 𝑦 ↑ 2 ) ) = ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
73 72 negeqd ( 𝑦 = ( cos ‘ 𝑥 ) → - ( 1 / ( 𝑦 ↑ 2 ) ) = - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
74 20 20 54 55 59 61 66 69 70 73 dvmptco ( ⊤ → ( ℂ D ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( 1 / ( cos ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) ) )
75 20 29 30 49 51 52 74 dvmptmul ( ⊤ → ( ℂ D ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( ( cos ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) + ( ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) · ( sin ‘ 𝑥 ) ) ) ) )
76 75 mptru ( ℂ D ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( sin ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( ( cos ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) + ( ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) · ( sin ‘ 𝑥 ) ) ) )
77 ovex ( ( sin ‘ 𝑥 ) / ( cos ‘ 𝑥 ) ) ∈ V
78 77 1 dmmpti dom tan = ( cos “ ( ℂ ∖ { 0 } ) )
79 78 eqcomi ( cos “ ( ℂ ∖ { 0 } ) ) = dom tan
80 8 sqcld ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( cos ‘ 𝑥 ) ↑ 2 ) ∈ ℂ )
81 7 sqcld ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( sin ‘ 𝑥 ) ↑ 2 ) ∈ ℂ )
82 sqne0 ( ( cos ‘ 𝑥 ) ∈ ℂ → ( ( ( cos ‘ 𝑥 ) ↑ 2 ) ≠ 0 ↔ ( cos ‘ 𝑥 ) ≠ 0 ) )
83 8 82 syl ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( cos ‘ 𝑥 ) ↑ 2 ) ≠ 0 ↔ ( cos ‘ 𝑥 ) ≠ 0 ) )
84 14 83 mpbird ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( cos ‘ 𝑥 ) ↑ 2 ) ≠ 0 )
85 80 81 80 84 divdird ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( ( cos ‘ 𝑥 ) ↑ 2 ) + ( ( sin ‘ 𝑥 ) ↑ 2 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( ( cos ‘ 𝑥 ) ↑ 2 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) + ( ( ( sin ‘ 𝑥 ) ↑ 2 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) ) )
86 80 81 addcomd ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( cos ‘ 𝑥 ) ↑ 2 ) + ( ( sin ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( sin ‘ 𝑥 ) ↑ 2 ) + ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
87 sincossq ( 𝑥 ∈ ℂ → ( ( ( sin ‘ 𝑥 ) ↑ 2 ) + ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = 1 )
88 6 87 syl ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( sin ‘ 𝑥 ) ↑ 2 ) + ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = 1 )
89 86 88 eqtrd ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( cos ‘ 𝑥 ) ↑ 2 ) + ( ( sin ‘ 𝑥 ) ↑ 2 ) ) = 1 )
90 89 oveq1d ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( ( cos ‘ 𝑥 ) ↑ 2 ) + ( ( sin ‘ 𝑥 ) ↑ 2 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
91 85 90 eqtr3d ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( ( cos ‘ 𝑥 ) ↑ 2 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) + ( ( ( sin ‘ 𝑥 ) ↑ 2 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) ) = ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
92 8 14 recidd ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( cos ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) = 1 )
93 80 84 dividd ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( cos ‘ 𝑥 ) ↑ 2 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = 1 )
94 92 93 eqtr4d ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( cos ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) = ( ( ( cos ‘ 𝑥 ) ↑ 2 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
95 7 7 80 84 div23d ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( sin ‘ 𝑥 ) · ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · ( sin ‘ 𝑥 ) ) )
96 7 sqvald ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( sin ‘ 𝑥 ) ↑ 2 ) = ( ( sin ‘ 𝑥 ) · ( sin ‘ 𝑥 ) ) )
97 96 oveq1d ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( sin ‘ 𝑥 ) ↑ 2 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = ( ( ( sin ‘ 𝑥 ) · ( sin ‘ 𝑥 ) ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
98 80 84 reccld ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) ∈ ℂ )
99 98 7 mul2negd ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) = ( ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · ( sin ‘ 𝑥 ) ) )
100 7 80 84 divrec2d ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) = ( ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · ( sin ‘ 𝑥 ) ) )
101 99 100 eqtr4d ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) = ( ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
102 101 oveq1d ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) · ( sin ‘ 𝑥 ) ) = ( ( ( sin ‘ 𝑥 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · ( sin ‘ 𝑥 ) ) )
103 95 97 102 3eqtr4rd ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) · ( sin ‘ 𝑥 ) ) = ( ( ( sin ‘ 𝑥 ) ↑ 2 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
104 94 103 oveq12d ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( cos ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) + ( ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) · ( sin ‘ 𝑥 ) ) ) = ( ( ( ( cos ‘ 𝑥 ) ↑ 2 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) + ( ( ( sin ‘ 𝑥 ) ↑ 2 ) / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) ) )
105 2nn0 2 ∈ ℕ0
106 expneg ( ( ( cos ‘ 𝑥 ) ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( ( cos ‘ 𝑥 ) ↑ - 2 ) = ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
107 8 105 106 sylancl ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( cos ‘ 𝑥 ) ↑ - 2 ) = ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) )
108 91 104 107 3eqtr4d ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) → ( ( ( cos ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) + ( ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) · ( sin ‘ 𝑥 ) ) ) = ( ( cos ‘ 𝑥 ) ↑ - 2 ) )
109 108 rgen 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ( ( ( cos ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) + ( ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) · ( sin ‘ 𝑥 ) ) ) = ( ( cos ‘ 𝑥 ) ↑ - 2 )
110 mpteq12 ( ( ( cos “ ( ℂ ∖ { 0 } ) ) = dom tan ∧ ∀ 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ( ( ( cos ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) + ( ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) · ( sin ‘ 𝑥 ) ) ) = ( ( cos ‘ 𝑥 ) ↑ - 2 ) ) → ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( ( cos ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) + ( ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) · ( sin ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ dom tan ↦ ( ( cos ‘ 𝑥 ) ↑ - 2 ) ) )
111 79 109 110 mp2an ( 𝑥 ∈ ( cos “ ( ℂ ∖ { 0 } ) ) ↦ ( ( ( cos ‘ 𝑥 ) · ( 1 / ( cos ‘ 𝑥 ) ) ) + ( ( - ( 1 / ( ( cos ‘ 𝑥 ) ↑ 2 ) ) · - ( sin ‘ 𝑥 ) ) · ( sin ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ dom tan ↦ ( ( cos ‘ 𝑥 ) ↑ - 2 ) )
112 18 76 111 3eqtri ( ℂ D tan ) = ( 𝑥 ∈ dom tan ↦ ( ( cos ‘ 𝑥 ) ↑ - 2 ) )