Metamath Proof Explorer

Theorem dvcot

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

Ref Expression
Assertion dvcot ( ℂ D cot ) = ( 𝑥 ∈ dom cot ↦ - ( ( csc ‘ 𝑥 ) ↑ 2 ) )

Proof

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