Metamath Proof Explorer

Theorem readvcot

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

Ref Expression
Hypothesis readvcot.d 
|- D = { y e. RR | ( sin ` y ) =/= 0 }
Assertion readvcot 
|- ( RR _D ( x e. D |-> ( log ` ( abs ` ( sin ` x ) ) ) ) ) = ( x e. D |-> ( ( cos ` x ) / ( sin ` x ) ) )

Proof

Step Hyp Ref Expression
1 readvcot.d 
 |-  D = { y e. RR | ( sin ` y ) =/= 0 }
2 reelprrecn 
 |-  RR e. { RR , CC }
3 2 a1i 
 |-  ( T. -> RR e. { RR , CC } )
4 fveq2 
 |-  ( y = x -> ( sin ` y ) = ( sin ` x ) )
5 4 neeq1d 
 |-  ( y = x -> ( ( sin ` y ) =/= 0 <-> ( sin ` x ) =/= 0 ) )
6 5 1 elrab2 
 |-  ( x e. D <-> ( x e. RR /\ ( sin ` x ) =/= 0 ) )
7 resincl 
 |-  ( x e. RR -> ( sin ` x ) e. RR )
8 7 adantr 
 |-  ( ( x e. RR /\ ( sin ` x ) =/= 0 ) -> ( sin ` x ) e. RR )
9 simpr 
 |-  ( ( x e. RR /\ ( sin ` x ) =/= 0 ) -> ( sin ` x ) =/= 0 )
10 8 9 eldifsnd 
 |-  ( ( x e. RR /\ ( sin ` x ) =/= 0 ) -> ( sin ` x ) e. ( RR \ { 0 } ) )
11 6 10 sylbi 
 |-  ( x e. D -> ( sin ` x ) e. ( RR \ { 0 } ) )
12 11 adantl 
 |-  ( ( T. /\ x e. D ) -> ( sin ` x ) e. ( RR \ { 0 } ) )
13 fvexd 
 |-  ( ( T. /\ x e. D ) -> ( cos ` x ) e. _V )
14 eldifi 
 |-  ( z e. ( RR \ { 0 } ) -> z e. RR )
15 14 adantl 
 |-  ( ( T. /\ z e. ( RR \ { 0 } ) ) -> z e. RR )
16 15 recnd 
 |-  ( ( T. /\ z e. ( RR \ { 0 } ) ) -> z e. CC )
17 16 abscld 
 |-  ( ( T. /\ z e. ( RR \ { 0 } ) ) -> ( abs ` z ) e. RR )
18 17 recnd 
 |-  ( ( T. /\ z e. ( RR \ { 0 } ) ) -> ( abs ` z ) e. CC )
19 eldifsni 
 |-  ( z e. ( RR \ { 0 } ) -> z =/= 0 )
20 19 adantl 
 |-  ( ( T. /\ z e. ( RR \ { 0 } ) ) -> z =/= 0 )
21 16 20 absne0d 
 |-  ( ( T. /\ z e. ( RR \ { 0 } ) ) -> ( abs ` z ) =/= 0 )
22 18 21 logcld 
 |-  ( ( T. /\ z e. ( RR \ { 0 } ) ) -> ( log ` ( abs ` z ) ) e. CC )
23 ovexd 
 |-  ( ( T. /\ z e. ( RR \ { 0 } ) ) -> ( 1 / z ) e. _V )
24 7 recnd 
 |-  ( x e. RR -> ( sin ` x ) e. CC )
25 24 adantl 
 |-  ( ( T. /\ x e. RR ) -> ( sin ` x ) e. CC )
26 fvexd 
 |-  ( ( T. /\ x e. RR ) -> ( cos ` x ) e. _V )
27 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
28 cnopn 
 |-  CC e. ( TopOpen ` CCfld )
29 28 a1i 
 |-  ( T. -> CC e. ( TopOpen ` CCfld ) )
30 ax-resscn 
 |-  RR C_ CC
31 dfss2 
 |-  ( RR C_ CC <-> ( RR i^i CC ) = RR )
32 30 31 mpbi 
 |-  ( RR i^i CC ) = RR
33 32 a1i 
 |-  ( T. -> ( RR i^i CC ) = RR )
34 sincl 
 |-  ( x e. CC -> ( sin ` x ) e. CC )
35 34 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( sin ` x ) e. CC )
36 fvexd 
 |-  ( ( T. /\ x e. CC ) -> ( cos ` x ) e. _V )
37 dvsin 
 |-  ( CC _D sin ) = cos
38 sinf 
 |-  sin : CC --> CC
39 38 a1i 
 |-  ( T. -> sin : CC --> CC )
40 39 feqmptd 
 |-  ( T. -> sin = ( x e. CC |-> ( sin ` x ) ) )
41 40 oveq2d 
 |-  ( T. -> ( CC _D sin ) = ( CC _D ( x e. CC |-> ( sin ` x ) ) ) )
42 cosf 
 |-  cos : CC --> CC
43 42 a1i 
 |-  ( T. -> cos : CC --> CC )
44 43 feqmptd 
 |-  ( T. -> cos = ( x e. CC |-> ( cos ` x ) ) )
45 37 41 44 3eqtr3a 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( sin ` x ) ) ) = ( x e. CC |-> ( cos ` x ) ) )
46 27 3 29 33 35 36 45 dvmptres3 
 |-  ( T. -> ( RR _D ( x e. RR |-> ( sin ` x ) ) ) = ( x e. RR |-> ( cos ` x ) ) )
47 1 ssrab3 
 |-  D C_ RR
48 47 a1i 
 |-  ( T. -> D C_ RR )
49 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
50 1 resuppsinopn 
 |-  D e. ( topGen ` ran (,) )
51 50 a1i 
 |-  ( T. -> D e. ( topGen ` ran (,) ) )
52 3 25 26 46 48 49 27 51 dvmptres 
 |-  ( T. -> ( RR _D ( x e. D |-> ( sin ` x ) ) ) = ( x e. D |-> ( cos ` x ) ) )
53 eqid 
 |-  ( RR \ { 0 } ) = ( RR \ { 0 } )
54 53 readvrec 
 |-  ( RR _D ( z e. ( RR \ { 0 } ) |-> ( log ` ( abs ` z ) ) ) ) = ( z e. ( RR \ { 0 } ) |-> ( 1 / z ) )
55 54 a1i 
 |-  ( T. -> ( RR _D ( z e. ( RR \ { 0 } ) |-> ( log ` ( abs ` z ) ) ) ) = ( z e. ( RR \ { 0 } ) |-> ( 1 / z ) ) )
56 2fveq3 
 |-  ( z = ( sin ` x ) -> ( log ` ( abs ` z ) ) = ( log ` ( abs ` ( sin ` x ) ) ) )
57 oveq2 
 |-  ( z = ( sin ` x ) -> ( 1 / z ) = ( 1 / ( sin ` x ) ) )
58 3 3 12 13 22 23 52 55 56 57 dvmptco 
 |-  ( T. -> ( RR _D ( x e. D |-> ( log ` ( abs ` ( sin ` x ) ) ) ) ) = ( x e. D |-> ( ( 1 / ( sin ` x ) ) x. ( cos ` x ) ) ) )
59 58 mptru 
 |-  ( RR _D ( x e. D |-> ( log ` ( abs ` ( sin ` x ) ) ) ) ) = ( x e. D |-> ( ( 1 / ( sin ` x ) ) x. ( cos ` x ) ) )
60 6 simplbi 
 |-  ( x e. D -> x e. RR )
61 60 recoscld 
 |-  ( x e. D -> ( cos ` x ) e. RR )
62 61 recnd 
 |-  ( x e. D -> ( cos ` x ) e. CC )
63 6 8 sylbi 
 |-  ( x e. D -> ( sin ` x ) e. RR )
64 63 recnd 
 |-  ( x e. D -> ( sin ` x ) e. CC )
65 6 9 sylbi 
 |-  ( x e. D -> ( sin ` x ) =/= 0 )
66 62 64 65 divrec2d 
 |-  ( x e. D -> ( ( cos ` x ) / ( sin ` x ) ) = ( ( 1 / ( sin ` x ) ) x. ( cos ` x ) ) )
67 66 mpteq2ia 
 |-  ( x e. D |-> ( ( cos ` x ) / ( sin ` x ) ) ) = ( x e. D |-> ( ( 1 / ( sin ` x ) ) x. ( cos ` x ) ) )
68 59 67 eqtr4i 
 |-  ( RR _D ( x e. D |-> ( log ` ( abs ` ( sin ` x ) ) ) ) ) = ( x e. D |-> ( ( cos ` x ) / ( sin ` x ) ) )