Metamath Proof Explorer


Theorem readvrec2

Description: The antiderivative of 1/x in real numbers, without using the absolute value function. (Contributed by SN, 1-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 redvabs.d D = 0
2 reelprrecn
3 2 a1i
4 1 eleq2i x D x 0
5 eldifsn x 0 x x 0
6 4 5 bitri x D x x 0
7 6 simplbi x D x
8 7 recnd x D x
9 8 sqcld x D x 2
10 6 simprbi x D x 0
11 sqne0 x x 2 0 x 0
12 8 11 syl x D x 2 0 x 0
13 10 12 mpbird x D x 2 0
14 9 13 logcld x D log x 2
15 14 adantl x D log x 2
16 ovexd x D 1 x 2 2 x V
17 cnelprrecn
18 17 a1i
19 incom + −∞ 0 = −∞ 0 +
20 dfrp2 + = 0 +∞
21 20 ineq2i −∞ 0 + = −∞ 0 0 +∞
22 mnfxr −∞ *
23 22 a1i −∞ *
24 0xr 0 *
25 24 a1i 0 *
26 pnfxr +∞ *
27 26 a1i +∞ *
28 23 25 27 iocioodisjd −∞ 0 0 +∞ =
29 28 mptru −∞ 0 0 +∞ =
30 19 21 29 3eqtri + −∞ 0 =
31 disjdif2 + −∞ 0 = + −∞ 0 = +
32 30 31 ax-mp + −∞ 0 = +
33 rpsscn +
34 ssdif + + −∞ 0 −∞ 0
35 33 34 ax-mp + −∞ 0 −∞ 0
36 32 35 eqsstrri + −∞ 0
37 10 adantl x D x 0
38 sqn0rp x x 0 x 2 +
39 7 37 38 syl2an2 x D x 2 +
40 36 39 sselid x D x 2 −∞ 0
41 ovexd x D 2 x V
42 eldifi y −∞ 0 y
43 eldifn y −∞ 0 ¬ y −∞ 0
44 mnflt0 −∞ < 0
45 0le0 0 0
46 elioc1 −∞ * 0 * 0 −∞ 0 0 * −∞ < 0 0 0
47 22 24 46 mp2an 0 −∞ 0 0 * −∞ < 0 0 0
48 24 44 45 47 mpbir3an 0 −∞ 0
49 eleq1 y = 0 y −∞ 0 0 −∞ 0
50 48 49 mpbiri y = 0 y −∞ 0
51 50 necon3bi ¬ y −∞ 0 y 0
52 43 51 syl y −∞ 0 y 0
53 42 52 logcld y −∞ 0 log y
54 53 adantl y −∞ 0 log y
55 ovexd y −∞ 0 1 y V
56 recn x x
57 56 adantl x x
58 57 sqcld x x 2
59 ovexd x 2 x 2 1 V
60 eqid TopOpen fld = TopOpen fld
61 cnopn TopOpen fld
62 61 a1i TopOpen fld
63 ax-resscn
64 dfss2 =
65 63 64 mpbi =
66 65 a1i =
67 sqcl x x 2
68 67 adantl x x 2
69 ovexd x 2 x 2 1 V
70 2nn 2
71 dvexp 2 dx x 2 d x = x 2 x 2 1
72 70 71 mp1i dx x 2 d x = x 2 x 2 1
73 60 3 62 66 68 69 72 dvmptres3 dx x 2 d x = x 2 x 2 1
74 7 ssriv D
75 74 a1i D
76 60 tgioo2 topGen ran . = TopOpen fld 𝑡
77 rehaus topGen ran . Haus
78 0re 0
79 uniretop = topGen ran .
80 79 sncld topGen ran . Haus 0 0 Clsd topGen ran .
81 77 78 80 mp2an 0 Clsd topGen ran .
82 79 cldopn 0 Clsd topGen ran . 0 topGen ran .
83 81 82 ax-mp 0 topGen ran .
84 1 83 eqeltri D topGen ran .
85 84 a1i D topGen ran .
86 3 58 59 73 75 76 60 85 dvmptres dx D x 2 d x = x D 2 x 2 1
87 2m1e1 2 1 = 1
88 87 oveq2i x 2 1 = x 1
89 8 exp1d x D x 1 = x
90 88 89 eqtrid x D x 2 1 = x
91 90 oveq2d x D 2 x 2 1 = 2 x
92 91 mpteq2ia x D 2 x 2 1 = x D 2 x
93 86 92 eqtrdi dx D x 2 d x = x D 2 x
94 logf1o log : 0 1-1 onto ran log
95 f1of log : 0 1-1 onto ran log log : 0 ran log
96 94 95 mp1i log : 0 ran log
97 snssi 0 −∞ 0 0 −∞ 0
98 48 97 ax-mp 0 −∞ 0
99 sscon 0 −∞ 0 −∞ 0 0
100 98 99 mp1i −∞ 0 0
101 96 100 feqresmpt log −∞ 0 = y −∞ 0 log y
102 101 oveq2d D log −∞ 0 = dy −∞ 0 log y d y
103 eqid −∞ 0 = −∞ 0
104 103 dvlog D log −∞ 0 = y −∞ 0 1 y
105 102 104 eqtr3di dy −∞ 0 log y d y = y −∞ 0 1 y
106 fveq2 y = x 2 log y = log x 2
107 oveq2 y = x 2 1 y = 1 x 2
108 3 18 40 41 54 55 93 105 106 107 dvmptco dx D log x 2 d x = x D 1 x 2 2 x
109 2cnd 2
110 2ne0 2 0
111 110 a1i 2 0
112 3 15 16 108 109 111 dvmptdivc dx D log x 2 2 d x = x D 1 x 2 2 x 2
113 112 mptru dx D log x 2 2 d x = x D 1 x 2 2 x 2
114 7 resqcld x D x 2
115 114 13 rereccld x D 1 x 2
116 115 recnd x D 1 x 2
117 2cnd x D 2
118 116 117 8 mul12d x D 1 x 2 2 x = 2 1 x 2 x
119 118 oveq1d x D 1 x 2 2 x 2 = 2 1 x 2 x 2
120 116 8 mulcld x D 1 x 2 x
121 110 a1i x D 2 0
122 120 117 121 divcan3d x D 2 1 x 2 x 2 = 1 x 2 x
123 8 sqvald x D x 2 = x x
124 123 oveq2d x D 1 x 2 = 1 x x
125 124 oveq1d x D 1 x 2 x = 1 x x x
126 8 8 10 10 recdiv2d x D 1 x x = 1 x x
127 126 oveq1d x D 1 x x x = 1 x x x
128 8 10 reccld x D 1 x
129 128 8 10 divcan1d x D 1 x x x = 1 x
130 125 127 129 3eqtr2d x D 1 x 2 x = 1 x
131 119 122 130 3eqtrd x D 1 x 2 2 x 2 = 1 x
132 131 mpteq2ia x D 1 x 2 2 x 2 = x D 1 x
133 113 132 eqtri dx D log x 2 2 d x = x D 1 x