Metamath Proof Explorer

Theorem readvcot

Description: Real antiderivative of cotangent. (Contributed by SN, 7-Oct-2025)

Ref Expression
Hypothesis readvcot.d ⊢ 𝐷 = { 𝑦 ∈ ℝ ∣ ( sin ‘ 𝑦 ) ≠ 0 }
Assertion readvcot ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( abs ‘ ( sin ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( cos ‘ 𝑥 ) / ( sin ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 readvcot.d ⊢ 𝐷 = { 𝑦 ∈ ℝ ∣ ( sin ‘ 𝑦 ) ≠ 0 }
2 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
3 2 a1i ⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } )
4 fveq2 ⊢ ( 𝑦 = 𝑥 → ( sin ‘ 𝑦 ) = ( sin ‘ 𝑥 ) )
5 4 neeq1d ⊢ ( 𝑦 = 𝑥 → ( ( sin ‘ 𝑦 ) ≠ 0 ↔ ( sin ‘ 𝑥 ) ≠ 0 ) )
6 5 1 elrab2 ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℝ ∧ ( sin ‘ 𝑥 ) ≠ 0 ) )
7 resincl ⊢ ( 𝑥 ∈ ℝ → ( sin ‘ 𝑥 ) ∈ ℝ )
8 7 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ ( sin ‘ 𝑥 ) ≠ 0 ) → ( sin ‘ 𝑥 ) ∈ ℝ )
9 simpr ⊢ ( ( 𝑥 ∈ ℝ ∧ ( sin ‘ 𝑥 ) ≠ 0 ) → ( sin ‘ 𝑥 ) ≠ 0 )
10 8 9 eldifsnd ⊢ ( ( 𝑥 ∈ ℝ ∧ ( sin ‘ 𝑥 ) ≠ 0 ) → ( sin ‘ 𝑥 ) ∈ ( ℝ ∖ { 0 } ) )
11 6 10 sylbi ⊢ ( 𝑥 ∈ 𝐷 → ( sin ‘ 𝑥 ) ∈ ( ℝ ∖ { 0 } ) )
12 11 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( sin ‘ 𝑥 ) ∈ ( ℝ ∖ { 0 } ) )
13 fvexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( cos ‘ 𝑥 ) ∈ V )
14 eldifi ⊢ ( 𝑧 ∈ ( ℝ ∖ { 0 } ) → 𝑧 ∈ ℝ )
15 14 adantl ⊢ ( ( ⊤ ∧ 𝑧 ∈ ( ℝ ∖ { 0 } ) ) → 𝑧 ∈ ℝ )
16 15 recnd ⊢ ( ( ⊤ ∧ 𝑧 ∈ ( ℝ ∖ { 0 } ) ) → 𝑧 ∈ ℂ )
17 16 abscld ⊢ ( ( ⊤ ∧ 𝑧 ∈ ( ℝ ∖ { 0 } ) ) → ( abs ‘ 𝑧 ) ∈ ℝ )
18 17 recnd ⊢ ( ( ⊤ ∧ 𝑧 ∈ ( ℝ ∖ { 0 } ) ) → ( abs ‘ 𝑧 ) ∈ ℂ )
19 eldifsni ⊢ ( 𝑧 ∈ ( ℝ ∖ { 0 } ) → 𝑧 ≠ 0 )
20 19 adantl ⊢ ( ( ⊤ ∧ 𝑧 ∈ ( ℝ ∖ { 0 } ) ) → 𝑧 ≠ 0 )
21 16 20 absne0d ⊢ ( ( ⊤ ∧ 𝑧 ∈ ( ℝ ∖ { 0 } ) ) → ( abs ‘ 𝑧 ) ≠ 0 )
22 18 21 logcld ⊢ ( ( ⊤ ∧ 𝑧 ∈ ( ℝ ∖ { 0 } ) ) → ( log ‘ ( abs ‘ 𝑧 ) ) ∈ ℂ )
23 ovexd ⊢ ( ( ⊤ ∧ 𝑧 ∈ ( ℝ ∖ { 0 } ) ) → ( 1 / 𝑧 ) ∈ V )
24 7 recnd ⊢ ( 𝑥 ∈ ℝ → ( sin ‘ 𝑥 ) ∈ ℂ )
25 24 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( sin ‘ 𝑥 ) ∈ ℂ )
26 fvexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( cos ‘ 𝑥 ) ∈ V )
27 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
28 cnopn ⊢ ℂ ∈ ( TopOpen ‘ ℂfld )
29 28 a1i ⊢ ( ⊤ → ℂ ∈ ( TopOpen ‘ ℂfld ) )
30 ax-resscn ⊢ ℝ ⊆ ℂ
31 dfss2 ⊢ ( ℝ ⊆ ℂ ↔ ( ℝ ∩ ℂ ) = ℝ )
32 30 31 mpbi ⊢ ( ℝ ∩ ℂ ) = ℝ
33 32 a1i ⊢ ( ⊤ → ( ℝ ∩ ℂ ) = ℝ )
34 sincl ⊢ ( 𝑥 ∈ ℂ → ( sin ‘ 𝑥 ) ∈ ℂ )
35 34 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( sin ‘ 𝑥 ) ∈ ℂ )
36 fvexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( cos ‘ 𝑥 ) ∈ V )
37 dvsin ⊢ ( ℂ D sin ) = cos
38 sinf ⊢ sin : ℂ ⟶ ℂ
39 38 a1i ⊢ ( ⊤ → sin : ℂ ⟶ ℂ )
40 39 feqmptd ⊢ ( ⊤ → sin = ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) )
41 40 oveq2d ⊢ ( ⊤ → ( ℂ D sin ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) ) )
42 cosf ⊢ cos : ℂ ⟶ ℂ
43 42 a1i ⊢ ( ⊤ → cos : ℂ ⟶ ℂ )
44 43 feqmptd ⊢ ( ⊤ → cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
45 37 41 44 3eqtr3a ⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
46 27 3 29 33 35 36 45 dvmptres3 ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( cos ‘ 𝑥 ) ) )
47 1 ssrab3 ⊢ 𝐷 ⊆ ℝ
48 47 a1i ⊢ ( ⊤ → 𝐷 ⊆ ℝ )
49 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
50 1 resuppsinopn ⊢ 𝐷 ∈ ( topGen ‘ ran (,) )
51 50 a1i ⊢ ( ⊤ → 𝐷 ∈ ( topGen ‘ ran (,) ) )
52 3 25 26 46 48 49 27 51 dvmptres ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( sin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( cos ‘ 𝑥 ) ) )
53 eqid ⊢ ( ℝ ∖ { 0 } ) = ( ℝ ∖ { 0 } )
54 53 readvrec ⊢ ( ℝ D ( 𝑧 ∈ ( ℝ ∖ { 0 } ) ↦ ( log ‘ ( abs ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( ℝ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) )
55 54 a1i ⊢ ( ⊤ → ( ℝ D ( 𝑧 ∈ ( ℝ ∖ { 0 } ) ↦ ( log ‘ ( abs ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( ℝ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) )
56 2fveq3 ⊢ ( 𝑧 = ( sin ‘ 𝑥 ) → ( log ‘ ( abs ‘ 𝑧 ) ) = ( log ‘ ( abs ‘ ( sin ‘ 𝑥 ) ) ) )
57 oveq2 ⊢ ( 𝑧 = ( sin ‘ 𝑥 ) → ( 1 / 𝑧 ) = ( 1 / ( sin ‘ 𝑥 ) ) )
58 3 3 12 13 22 23 52 55 56 57 dvmptco ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( abs ‘ ( sin ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( sin ‘ 𝑥 ) ) · ( cos ‘ 𝑥 ) ) ) )
59 58 mptru ⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( abs ‘ ( sin ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( sin ‘ 𝑥 ) ) · ( cos ‘ 𝑥 ) ) )
60 6 simplbi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℝ )
61 60 recoscld ⊢ ( 𝑥 ∈ 𝐷 → ( cos ‘ 𝑥 ) ∈ ℝ )
62 61 recnd ⊢ ( 𝑥 ∈ 𝐷 → ( cos ‘ 𝑥 ) ∈ ℂ )
63 6 8 sylbi ⊢ ( 𝑥 ∈ 𝐷 → ( sin ‘ 𝑥 ) ∈ ℝ )
64 63 recnd ⊢ ( 𝑥 ∈ 𝐷 → ( sin ‘ 𝑥 ) ∈ ℂ )
65 6 9 sylbi ⊢ ( 𝑥 ∈ 𝐷 → ( sin ‘ 𝑥 ) ≠ 0 )
66 62 64 65 divrec2d ⊢ ( 𝑥 ∈ 𝐷 → ( ( cos ‘ 𝑥 ) / ( sin ‘ 𝑥 ) ) = ( ( 1 / ( sin ‘ 𝑥 ) ) · ( cos ‘ 𝑥 ) ) )
67 66 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( cos ‘ 𝑥 ) / ( sin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( sin ‘ 𝑥 ) ) · ( cos ‘ 𝑥 ) ) )
68 59 67 eqtr4i ⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( abs ‘ ( sin ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( cos ‘ 𝑥 ) / ( sin ‘ 𝑥 ) ) )