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 = ( RR \ { 0 } )
Assertion readvrec2 
|- ( RR _D ( x e. D |-> ( ( log ` ( x ^ 2 ) ) / 2 ) ) ) = ( x e. D |-> ( 1 / x ) )

Proof

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