Metamath Proof Explorer


Theorem readvcot

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

Ref Expression
Hypothesis readvcot.d D = y | sin y 0
Assertion readvcot dx D log sin x d x = x D cos x sin x

Proof

Step Hyp Ref Expression
1 readvcot.d D = y | sin y 0
2 reelprrecn
3 2 a1i
4 fveq2 y = x sin y = sin x
5 4 neeq1d y = x sin y 0 sin x 0
6 5 1 elrab2 x D x sin x 0
7 resincl x sin x
8 7 adantr x sin x 0 sin x
9 simpr x sin x 0 sin x 0
10 8 9 eldifsnd x sin x 0 sin x 0
11 6 10 sylbi x D sin x 0
12 11 adantl x D sin x 0
13 fvexd x D cos x V
14 eldifi z 0 z
15 14 adantl z 0 z
16 15 recnd z 0 z
17 16 abscld z 0 z
18 17 recnd z 0 z
19 eldifsni z 0 z 0
20 19 adantl z 0 z 0
21 16 20 absne0d z 0 z 0
22 18 21 logcld z 0 log z
23 ovexd z 0 1 z V
24 7 recnd x sin x
25 24 adantl x sin x
26 fvexd x cos x 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 x sin x
35 34 adantl x sin x
36 fvexd x cos x V
37 dvsin D sin = cos
38 sinf sin :
39 38 a1i sin :
40 39 feqmptd sin = x sin x
41 40 oveq2d D sin = dx sin x d x
42 cosf cos :
43 42 a1i cos :
44 43 feqmptd cos = x cos x
45 37 41 44 3eqtr3a dx sin x d x = x cos x
46 27 3 29 33 35 36 45 dvmptres3 dx sin x d x = x cos x
47 1 ssrab3 D
48 47 a1i D
49 tgioo4 topGen ran . = TopOpen fld 𝑡
50 1 resuppsinopn D topGen ran .
51 50 a1i D topGen ran .
52 3 25 26 46 48 49 27 51 dvmptres dx D sin x d x = x D cos x
53 eqid 0 = 0
54 53 readvrec dz 0 log z d z = z 0 1 z
55 54 a1i dz 0 log z d z = z 0 1 z
56 2fveq3 z = sin x log z = log sin x
57 oveq2 z = sin x 1 z = 1 sin x
58 3 3 12 13 22 23 52 55 56 57 dvmptco dx D log sin x d x = x D 1 sin x cos x
59 58 mptru dx D log sin x d x = x D 1 sin x cos x
60 6 simplbi x D x
61 60 recoscld x D cos x
62 61 recnd x D cos x
63 6 8 sylbi x D sin x
64 63 recnd x D sin x
65 6 9 sylbi x D sin x 0
66 62 64 65 divrec2d x D cos x sin x = 1 sin x cos x
67 66 mpteq2ia x D cos x sin x = x D 1 sin x cos x
68 59 67 eqtr4i dx D log sin x d x = x D cos x sin x