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 tgioo4 ⊢ 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