Metamath Proof Explorer


Theorem readvrec

Description: For real numbers, the antiderivative of 1/x is ln|x|. (Contributed by SN, 30-Sep-2025)

Ref Expression
Hypothesis redvabs.d D = 0
Assertion readvrec dx D log x d x = x D 1 x

Proof

Step Hyp Ref Expression
1 redvabs.d D = 0
2 reelprrecn
3 2 a1i
4 cnelprrecn
5 4 a1i
6 dfrp2 + = 0 +∞
7 mnfxr −∞ *
8 7 a1i −∞ *
9 0xr 0 *
10 9 a1i 0 *
11 pnfxr +∞ *
12 11 a1i +∞ *
13 8 10 12 iocioodisjd −∞ 0 0 +∞ =
14 13 mptru −∞ 0 0 +∞ =
15 14 ineqcomi 0 +∞ −∞ 0 =
16 disjdif2 0 +∞ −∞ 0 = 0 +∞ −∞ 0 = 0 +∞
17 15 16 ax-mp 0 +∞ −∞ 0 = 0 +∞
18 6 17 eqtr4i + = 0 +∞ −∞ 0
19 ioosscn 0 +∞
20 ssdif 0 +∞ 0 +∞ −∞ 0 −∞ 0
21 19 20 ax-mp 0 +∞ −∞ 0 −∞ 0
22 18 21 eqsstri + −∞ 0
23 1 eleq2i x D x 0
24 eldifsn x 0 x x 0
25 23 24 bitri x D x x 0
26 25 simplbi x D x
27 26 recnd x D x
28 27 adantl x D x
29 25 simprbi x D x 0
30 29 adantl x D x 0
31 28 30 absrpcld x D x +
32 22 31 sselid x D x −∞ 0
33 negex 1 V
34 1ex 1 V
35 33 34 ifex if x < 0 1 1 V
36 35 a1i x D if x < 0 1 1 V
37 eldifi y −∞ 0 y
38 37 adantl y −∞ 0 y
39 eldifn y −∞ 0 ¬ y −∞ 0
40 mnflt0 −∞ < 0
41 ubioc1 −∞ * 0 * −∞ < 0 0 −∞ 0
42 7 9 40 41 mp3an 0 −∞ 0
43 eleq1 y = 0 y −∞ 0 0 −∞ 0
44 42 43 mpbiri y = 0 y −∞ 0
45 44 necon3bi ¬ y −∞ 0 y 0
46 39 45 syl y −∞ 0 y 0
47 46 adantl y −∞ 0 y 0
48 38 47 logcld y −∞ 0 log y
49 ovexd y −∞ 0 1 y V
50 1 redvmptabs dx D x d x = x D if x < 0 1 1
51 50 a1i dx D x d x = x D if x < 0 1 1
52 logf1o log : 0 1-1 onto ran log
53 f1of log : 0 1-1 onto ran log log : 0 ran log
54 52 53 mp1i log : 0 ran log
55 eqid −∞ 0 = −∞ 0
56 55 logdmss −∞ 0 0
57 56 a1i −∞ 0 0
58 54 57 feqresmpt log −∞ 0 = y −∞ 0 log y
59 58 mptru log −∞ 0 = y −∞ 0 log y
60 59 oveq2i D log −∞ 0 = dy −∞ 0 log y d y
61 55 dvlog D log −∞ 0 = y −∞ 0 1 y
62 60 61 eqtr3i dy −∞ 0 log y d y = y −∞ 0 1 y
63 62 a1i dy −∞ 0 log y d y = y −∞ 0 1 y
64 fveq2 y = x log y = log x
65 oveq2 y = x 1 y = 1 x
66 3 5 32 36 48 49 51 63 64 65 dvmptco dx D log x d x = x D 1 x if x < 0 1 1
67 66 mptru dx D log x d x = x D 1 x if x < 0 1 1
68 ovif2 1 x if x < 0 1 1 = if x < 0 1 x -1 1 x 1
69 simpll x x 0 x < 0 x
70 69 recnd x x 0 x < 0 x
71 70 abscld x x 0 x < 0 x
72 71 recnd x x 0 x < 0 x
73 simplr x x 0 x < 0 x 0
74 70 73 absne0d x x 0 x < 0 x 0
75 72 74 reccld x x 0 x < 0 1 x
76 neg1cn 1
77 76 a1i x x 0 x < 0 1
78 75 77 mulcomd x x 0 x < 0 1 x -1 = -1 1 x
79 75 mulm1d x x 0 x < 0 -1 1 x = 1 x
80 1cnd x x 0 x < 0 1
81 80 72 74 divneg2d x x 0 x < 0 1 x = 1 x
82 0red x x 0 x < 0 0
83 simpr x x 0 x < 0 x < 0
84 69 82 83 ltled x x 0 x < 0 x 0
85 69 84 absnidd x x 0 x < 0 x = x
86 85 eqcomd x x 0 x < 0 x = x
87 70 86 negcon1ad x x 0 x < 0 x = x
88 87 oveq2d x x 0 x < 0 1 x = 1 x
89 81 88 eqtrd x x 0 x < 0 1 x = 1 x
90 78 79 89 3eqtrd x x 0 x < 0 1 x -1 = 1 x
91 25 90 sylanb x D x < 0 1 x -1 = 1 x
92 recn x x
93 92 abscld x x
94 93 ad2antrr x x 0 ¬ x < 0 x
95 92 ad2antrr x x 0 ¬ x < 0 x
96 simplr x x 0 ¬ x < 0 x 0
97 95 96 absne0d x x 0 ¬ x < 0 x 0
98 94 97 rereccld x x 0 ¬ x < 0 1 x
99 98 recnd x x 0 ¬ x < 0 1 x
100 99 mulridd x x 0 ¬ x < 0 1 x 1 = 1 x
101 simpll x x 0 ¬ x < 0 x
102 0red x x 0 0
103 simpl x x 0 x
104 102 103 lenltd x x 0 0 x ¬ x < 0
105 104 biimpar x x 0 ¬ x < 0 0 x
106 101 105 absidd x x 0 ¬ x < 0 x = x
107 106 oveq2d x x 0 ¬ x < 0 1 x = 1 x
108 100 107 eqtrd x x 0 ¬ x < 0 1 x 1 = 1 x
109 25 108 sylanb x D ¬ x < 0 1 x 1 = 1 x
110 91 109 ifeqda x D if x < 0 1 x -1 1 x 1 = 1 x
111 68 110 eqtrid x D 1 x if x < 0 1 1 = 1 x
112 111 mpteq2ia x D 1 x if x < 0 1 1 = x D 1 x
113 67 112 eqtri dx D log x d x = x D 1 x