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 ⊢ 𝐷 = ( ℝ ∖ { 0 } )
Assertion readvrec2 ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( ( log ‘ ( 𝑥 ↑ 2 ) ) / 2 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )

Proof

Step Hyp Ref Expression
1 redvabs.d ⊢ 𝐷 = ( ℝ ∖ { 0 } )
2 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
3 2 a1i ⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } )
4 1 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ ( ℝ ∖ { 0 } ) )
5 eldifsn ⊢ ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) )
6 4 5 bitri ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) )
7 6 simplbi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℝ )
8 7 recnd ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
9 8 sqcld ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑ 2 ) ∈ ℂ )
10 6 simprbi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 )
11 sqne0 ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 ↑ 2 ) ≠ 0 ↔ 𝑥 ≠ 0 ) )
12 8 11 syl ⊢ ( 𝑥 ∈ 𝐷 → ( ( 𝑥 ↑ 2 ) ≠ 0 ↔ 𝑥 ≠ 0 ) )
13 10 12 mpbird ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑ 2 ) ≠ 0 )
14 9 13 logcld ⊢ ( 𝑥 ∈ 𝐷 → ( log ‘ ( 𝑥 ↑ 2 ) ) ∈ ℂ )
15 14 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( log ‘ ( 𝑥 ↑ 2 ) ) ∈ ℂ )
16 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( ( 1 / ( 𝑥 ↑ 2 ) ) · ( 2 · 𝑥 ) ) ∈ 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 ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ≠ 0 )
38 sqn0rp ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
39 7 37 38 syl2an2 ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
40 36 39 sselid ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↑ 2 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
41 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( 2 · 𝑥 ) ∈ V )
42 eldifi ⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝑦 ∈ ℂ )
43 eldifn ⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ¬ 𝑦 ∈ ( -∞ (,] 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 ⊢ ( 𝑦 = 0 → ( 𝑦 ∈ ( -∞ (,] 0 ) ↔ 0 ∈ ( -∞ (,] 0 ) ) )
50 48 49 mpbiri ⊢ ( 𝑦 = 0 → 𝑦 ∈ ( -∞ (,] 0 ) )
51 50 necon3bi ⊢ ( ¬ 𝑦 ∈ ( -∞ (,] 0 ) → 𝑦 ≠ 0 )
52 43 51 syl ⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝑦 ≠ 0 )
53 42 52 logcld ⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( log ‘ 𝑦 ) ∈ ℂ )
54 53 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( log ‘ 𝑦 ) ∈ ℂ )
55 ovexd ⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( 1 / 𝑦 ) ∈ V )
56 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
57 56 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
58 57 sqcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ↑ 2 ) ∈ ℂ )
59 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( 2 · ( 𝑥 ↑ ( 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 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 2 ) ∈ ℂ )
68 67 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ 2 ) ∈ ℂ )
69 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ∈ V )
70 2nn ⊢ 2 ∈ ℕ
71 dvexp ⊢ ( 2 ∈ ℕ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) )
72 70 71 mp1i ⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) )
73 60 3 62 66 68 69 72 dvmptres3 ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) )
74 7 ssriv ⊢ 𝐷 ⊆ ℝ
75 74 a1i ⊢ ( ⊤ → 𝐷 ⊆ ℝ )
76 60 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
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 ⊢ 𝐷 ∈ ( topGen ‘ ran (,) )
85 84 a1i ⊢ ( ⊤ → 𝐷 ∈ ( topGen ‘ ran (,) ) )
86 3 58 59 73 75 76 60 85 dvmptres ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) )
87 2m1e1 ⊢ ( 2 − 1 ) = 1
88 87 oveq2i ⊢ ( 𝑥 ↑ ( 2 − 1 ) ) = ( 𝑥 ↑ 1 )
89 8 exp1d ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑ 1 ) = 𝑥 )
90 88 89 eqtrid ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑ ( 2 − 1 ) ) = 𝑥 )
91 90 oveq2d ⊢ ( 𝑥 ∈ 𝐷 → ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) = ( 2 · 𝑥 ) )
92 91 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ ( 2 · ( 𝑥 ↑ ( 2 − 1 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 2 · 𝑥 ) )
93 86 92 eqtrdi ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 2 · 𝑥 ) ) )
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 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) )
102 101 oveq2d ⊢ ( ⊤ → ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) )
103 eqid ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
104 103 dvlog ⊢ ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) )
105 102 104 eqtr3di ⊢ ( ⊤ → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) ) )
106 fveq2 ⊢ ( 𝑦 = ( 𝑥 ↑ 2 ) → ( log ‘ 𝑦 ) = ( log ‘ ( 𝑥 ↑ 2 ) ) )
107 oveq2 ⊢ ( 𝑦 = ( 𝑥 ↑ 2 ) → ( 1 / 𝑦 ) = ( 1 / ( 𝑥 ↑ 2 ) ) )
108 3 18 40 41 54 55 93 105 106 107 dvmptco ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( 𝑥 ↑ 2 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( 𝑥 ↑ 2 ) ) · ( 2 · 𝑥 ) ) ) )
109 2cnd ⊢ ( ⊤ → 2 ∈ ℂ )
110 2ne0 ⊢ 2 ≠ 0
111 110 a1i ⊢ ( ⊤ → 2 ≠ 0 )
112 3 15 16 108 109 111 dvmptdivc ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( ( log ‘ ( 𝑥 ↑ 2 ) ) / 2 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( ( 1 / ( 𝑥 ↑ 2 ) ) · ( 2 · 𝑥 ) ) / 2 ) ) )
113 112 mptru ⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( ( log ‘ ( 𝑥 ↑ 2 ) ) / 2 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( ( 1 / ( 𝑥 ↑ 2 ) ) · ( 2 · 𝑥 ) ) / 2 ) )
114 7 resqcld ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑ 2 ) ∈ ℝ )
115 114 13 rereccld ⊢ ( 𝑥 ∈ 𝐷 → ( 1 / ( 𝑥 ↑ 2 ) ) ∈ ℝ )
116 115 recnd ⊢ ( 𝑥 ∈ 𝐷 → ( 1 / ( 𝑥 ↑ 2 ) ) ∈ ℂ )
117 2cnd ⊢ ( 𝑥 ∈ 𝐷 → 2 ∈ ℂ )
118 116 117 8 mul12d ⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / ( 𝑥 ↑ 2 ) ) · ( 2 · 𝑥 ) ) = ( 2 · ( ( 1 / ( 𝑥 ↑ 2 ) ) · 𝑥 ) ) )
119 118 oveq1d ⊢ ( 𝑥 ∈ 𝐷 → ( ( ( 1 / ( 𝑥 ↑ 2 ) ) · ( 2 · 𝑥 ) ) / 2 ) = ( ( 2 · ( ( 1 / ( 𝑥 ↑ 2 ) ) · 𝑥 ) ) / 2 ) )
120 116 8 mulcld ⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / ( 𝑥 ↑ 2 ) ) · 𝑥 ) ∈ ℂ )
121 110 a1i ⊢ ( 𝑥 ∈ 𝐷 → 2 ≠ 0 )
122 120 117 121 divcan3d ⊢ ( 𝑥 ∈ 𝐷 → ( ( 2 · ( ( 1 / ( 𝑥 ↑ 2 ) ) · 𝑥 ) ) / 2 ) = ( ( 1 / ( 𝑥 ↑ 2 ) ) · 𝑥 ) )
123 8 sqvald ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑ 2 ) = ( 𝑥 · 𝑥 ) )
124 123 oveq2d ⊢ ( 𝑥 ∈ 𝐷 → ( 1 / ( 𝑥 ↑ 2 ) ) = ( 1 / ( 𝑥 · 𝑥 ) ) )
125 124 oveq1d ⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / ( 𝑥 ↑ 2 ) ) · 𝑥 ) = ( ( 1 / ( 𝑥 · 𝑥 ) ) · 𝑥 ) )
126 8 8 10 10 recdiv2d ⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / 𝑥 ) / 𝑥 ) = ( 1 / ( 𝑥 · 𝑥 ) ) )
127 126 oveq1d ⊢ ( 𝑥 ∈ 𝐷 → ( ( ( 1 / 𝑥 ) / 𝑥 ) · 𝑥 ) = ( ( 1 / ( 𝑥 · 𝑥 ) ) · 𝑥 ) )
128 8 10 reccld ⊢ ( 𝑥 ∈ 𝐷 → ( 1 / 𝑥 ) ∈ ℂ )
129 128 8 10 divcan1d ⊢ ( 𝑥 ∈ 𝐷 → ( ( ( 1 / 𝑥 ) / 𝑥 ) · 𝑥 ) = ( 1 / 𝑥 ) )
130 125 127 129 3eqtr2d ⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / ( 𝑥 ↑ 2 ) ) · 𝑥 ) = ( 1 / 𝑥 ) )
131 119 122 130 3eqtrd ⊢ ( 𝑥 ∈ 𝐷 → ( ( ( 1 / ( 𝑥 ↑ 2 ) ) · ( 2 · 𝑥 ) ) / 2 ) = ( 1 / 𝑥 ) )
132 131 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( ( 1 / ( 𝑥 ↑ 2 ) ) · ( 2 · 𝑥 ) ) / 2 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )
133 113 132 eqtri ⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( ( log ‘ ( 𝑥 ↑ 2 ) ) / 2 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )