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 = ( RR \ { 0 } )
Assertion readvrec 
|- ( RR _D ( x e. D |-> ( log ` ( abs ` x ) ) ) ) = ( 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 cnelprrecn 
 |-  CC e. { RR , CC }
5 4 a1i 
 |-  ( T. -> CC e. { RR , CC } )
6 dfrp2 
 |-  RR+ = ( 0 (,) +oo )
7 mnfxr 
 |-  -oo e. RR*
8 7 a1i 
 |-  ( T. -> -oo e. RR* )
9 0xr 
 |-  0 e. RR*
10 9 a1i 
 |-  ( T. -> 0 e. RR* )
11 pnfxr 
 |-  +oo e. RR*
12 11 a1i 
 |-  ( T. -> +oo e. RR* )
13 8 10 12 iocioodisjd 
 |-  ( T. -> ( ( -oo (,] 0 ) i^i ( 0 (,) +oo ) ) = (/) )
14 13 mptru 
 |-  ( ( -oo (,] 0 ) i^i ( 0 (,) +oo ) ) = (/)
15 14 ineqcomi 
 |-  ( ( 0 (,) +oo ) i^i ( -oo (,] 0 ) ) = (/)
16 disjdif2 
 |-  ( ( ( 0 (,) +oo ) i^i ( -oo (,] 0 ) ) = (/) -> ( ( 0 (,) +oo ) \ ( -oo (,] 0 ) ) = ( 0 (,) +oo ) )
17 15 16 ax-mp 
 |-  ( ( 0 (,) +oo ) \ ( -oo (,] 0 ) ) = ( 0 (,) +oo )
18 6 17 eqtr4i 
 |-  RR+ = ( ( 0 (,) +oo ) \ ( -oo (,] 0 ) )
19 ioosscn 
 |-  ( 0 (,) +oo ) C_ CC
20 ssdif 
 |-  ( ( 0 (,) +oo ) C_ CC -> ( ( 0 (,) +oo ) \ ( -oo (,] 0 ) ) C_ ( CC \ ( -oo (,] 0 ) ) )
21 19 20 ax-mp 
 |-  ( ( 0 (,) +oo ) \ ( -oo (,] 0 ) ) C_ ( CC \ ( -oo (,] 0 ) )
22 18 21 eqsstri 
 |-  RR+ C_ ( CC \ ( -oo (,] 0 ) )
23 1 eleq2i 
 |-  ( x e. D <-> x e. ( RR \ { 0 } ) )
24 eldifsn 
 |-  ( x e. ( RR \ { 0 } ) <-> ( x e. RR /\ x =/= 0 ) )
25 23 24 bitri 
 |-  ( x e. D <-> ( x e. RR /\ x =/= 0 ) )
26 25 simplbi 
 |-  ( x e. D -> x e. RR )
27 26 recnd 
 |-  ( x e. D -> x e. CC )
28 27 adantl 
 |-  ( ( T. /\ x e. D ) -> x e. CC )
29 25 simprbi 
 |-  ( x e. D -> x =/= 0 )
30 29 adantl 
 |-  ( ( T. /\ x e. D ) -> x =/= 0 )
31 28 30 absrpcld 
 |-  ( ( T. /\ x e. D ) -> ( abs ` x ) e. RR+ )
32 22 31 sselid 
 |-  ( ( T. /\ x e. D ) -> ( abs ` x ) e. ( CC \ ( -oo (,] 0 ) ) )
33 negex 
 |-  -u 1 e. _V
34 1ex 
 |-  1 e. _V
35 33 34 ifex 
 |-  if ( x < 0 , -u 1 , 1 ) e. _V
36 35 a1i 
 |-  ( ( T. /\ x e. D ) -> if ( x < 0 , -u 1 , 1 ) e. _V )
37 eldifi 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> y e. CC )
38 37 adantl 
 |-  ( ( T. /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> y e. CC )
39 eldifn 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> -. y e. ( -oo (,] 0 ) )
40 mnflt0 
 |-  -oo < 0
41 ubioc1 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ -oo < 0 ) -> 0 e. ( -oo (,] 0 ) )
42 7 9 40 41 mp3an 
 |-  0 e. ( -oo (,] 0 )
43 eleq1 
 |-  ( y = 0 -> ( y e. ( -oo (,] 0 ) <-> 0 e. ( -oo (,] 0 ) ) )
44 42 43 mpbiri 
 |-  ( y = 0 -> y e. ( -oo (,] 0 ) )
45 44 necon3bi 
 |-  ( -. y e. ( -oo (,] 0 ) -> y =/= 0 )
46 39 45 syl 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> y =/= 0 )
47 46 adantl 
 |-  ( ( T. /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> y =/= 0 )
48 38 47 logcld 
 |-  ( ( T. /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> ( log ` y ) e. CC )
49 ovexd 
 |-  ( ( T. /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> ( 1 / y ) e. _V )
50 1 redvmptabs 
 |-  ( RR _D ( x e. D |-> ( abs ` x ) ) ) = ( x e. D |-> if ( x < 0 , -u 1 , 1 ) )
51 50 a1i 
 |-  ( T. -> ( RR _D ( x e. D |-> ( abs ` x ) ) ) = ( x e. D |-> if ( x < 0 , -u 1 , 1 ) ) )
52 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
53 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
54 52 53 ax-mp 
 |-  log : ( CC \ { 0 } ) --> ran log
55 54 a1i 
 |-  ( T. -> log : ( CC \ { 0 } ) --> ran log )
56 55 feqmptd 
 |-  ( T. -> log = ( y e. ( CC \ { 0 } ) |-> ( log ` y ) ) )
57 56 mptru 
 |-  log = ( y e. ( CC \ { 0 } ) |-> ( log ` y ) )
58 57 reseq1i 
 |-  ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( ( y e. ( CC \ { 0 } ) |-> ( log ` y ) ) |` ( CC \ ( -oo (,] 0 ) ) )
59 c0ex 
 |-  0 e. _V
60 59 snss 
 |-  ( 0 e. ( -oo (,] 0 ) <-> { 0 } C_ ( -oo (,] 0 ) )
61 42 60 mpbi 
 |-  { 0 } C_ ( -oo (,] 0 )
62 sscon 
 |-  ( { 0 } C_ ( -oo (,] 0 ) -> ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } ) )
63 resmpt 
 |-  ( ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } ) -> ( ( y e. ( CC \ { 0 } ) |-> ( log ` y ) ) |` ( CC \ ( -oo (,] 0 ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) )
64 61 62 63 mp2b 
 |-  ( ( y e. ( CC \ { 0 } ) |-> ( log ` y ) ) |` ( CC \ ( -oo (,] 0 ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) )
65 58 64 eqtr2i 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) = ( log |` ( CC \ ( -oo (,] 0 ) ) )
66 65 oveq2i 
 |-  ( CC _D ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) ) = ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) )
67 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
68 67 dvlog 
 |-  ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / y ) )
69 66 68 eqtri 
 |-  ( CC _D ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / y ) )
70 69 a1i 
 |-  ( T. -> ( CC _D ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / y ) ) )
71 fveq2 
 |-  ( y = ( abs ` x ) -> ( log ` y ) = ( log ` ( abs ` x ) ) )
72 oveq2 
 |-  ( y = ( abs ` x ) -> ( 1 / y ) = ( 1 / ( abs ` x ) ) )
73 3 5 32 36 48 49 51 70 71 72 dvmptco 
 |-  ( T. -> ( RR _D ( x e. D |-> ( log ` ( abs ` x ) ) ) ) = ( x e. D |-> ( ( 1 / ( abs ` x ) ) x. if ( x < 0 , -u 1 , 1 ) ) ) )
74 73 mptru 
 |-  ( RR _D ( x e. D |-> ( log ` ( abs ` x ) ) ) ) = ( x e. D |-> ( ( 1 / ( abs ` x ) ) x. if ( x < 0 , -u 1 , 1 ) ) )
75 ovif2 
 |-  ( ( 1 / ( abs ` x ) ) x. if ( x < 0 , -u 1 , 1 ) ) = if ( x < 0 , ( ( 1 / ( abs ` x ) ) x. -u 1 ) , ( ( 1 / ( abs ` x ) ) x. 1 ) )
76 simpll 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> x e. RR )
77 76 recnd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> x e. CC )
78 77 abscld 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> ( abs ` x ) e. RR )
79 78 recnd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> ( abs ` x ) e. CC )
80 simplr 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> x =/= 0 )
81 77 80 absne0d 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> ( abs ` x ) =/= 0 )
82 79 81 reccld 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> ( 1 / ( abs ` x ) ) e. CC )
83 neg1cn 
 |-  -u 1 e. CC
84 83 a1i 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> -u 1 e. CC )
85 82 84 mulcomd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> ( ( 1 / ( abs ` x ) ) x. -u 1 ) = ( -u 1 x. ( 1 / ( abs ` x ) ) ) )
86 82 mulm1d 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> ( -u 1 x. ( 1 / ( abs ` x ) ) ) = -u ( 1 / ( abs ` x ) ) )
87 1cnd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> 1 e. CC )
88 87 79 81 divneg2d 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> -u ( 1 / ( abs ` x ) ) = ( 1 / -u ( abs ` x ) ) )
89 0red 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> 0 e. RR )
90 simpr 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> x < 0 )
91 76 89 90 ltled 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> x <_ 0 )
92 76 91 absnidd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> ( abs ` x ) = -u x )
93 92 eqcomd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> -u x = ( abs ` x ) )
94 77 93 negcon1ad 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> -u ( abs ` x ) = x )
95 94 oveq2d 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> ( 1 / -u ( abs ` x ) ) = ( 1 / x ) )
96 88 95 eqtrd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> -u ( 1 / ( abs ` x ) ) = ( 1 / x ) )
97 85 86 96 3eqtrd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ x < 0 ) -> ( ( 1 / ( abs ` x ) ) x. -u 1 ) = ( 1 / x ) )
98 25 97 sylanb 
 |-  ( ( x e. D /\ x < 0 ) -> ( ( 1 / ( abs ` x ) ) x. -u 1 ) = ( 1 / x ) )
99 recn 
 |-  ( x e. RR -> x e. CC )
100 99 abscld 
 |-  ( x e. RR -> ( abs ` x ) e. RR )
101 100 ad2antrr 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> ( abs ` x ) e. RR )
102 99 ad2antrr 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> x e. CC )
103 simplr 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> x =/= 0 )
104 102 103 absne0d 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> ( abs ` x ) =/= 0 )
105 101 104 rereccld 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> ( 1 / ( abs ` x ) ) e. RR )
106 105 recnd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> ( 1 / ( abs ` x ) ) e. CC )
107 106 mulridd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> ( ( 1 / ( abs ` x ) ) x. 1 ) = ( 1 / ( abs ` x ) ) )
108 simpll 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> x e. RR )
109 0red 
 |-  ( ( x e. RR /\ x =/= 0 ) -> 0 e. RR )
110 simpl 
 |-  ( ( x e. RR /\ x =/= 0 ) -> x e. RR )
111 109 110 lenltd 
 |-  ( ( x e. RR /\ x =/= 0 ) -> ( 0 <_ x <-> -. x < 0 ) )
112 111 biimpar 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> 0 <_ x )
113 108 112 absidd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> ( abs ` x ) = x )
114 113 oveq2d 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> ( 1 / ( abs ` x ) ) = ( 1 / x ) )
115 107 114 eqtrd 
 |-  ( ( ( x e. RR /\ x =/= 0 ) /\ -. x < 0 ) -> ( ( 1 / ( abs ` x ) ) x. 1 ) = ( 1 / x ) )
116 25 115 sylanb 
 |-  ( ( x e. D /\ -. x < 0 ) -> ( ( 1 / ( abs ` x ) ) x. 1 ) = ( 1 / x ) )
117 98 116 ifeqda 
 |-  ( x e. D -> if ( x < 0 , ( ( 1 / ( abs ` x ) ) x. -u 1 ) , ( ( 1 / ( abs ` x ) ) x. 1 ) ) = ( 1 / x ) )
118 75 117 eqtrid 
 |-  ( x e. D -> ( ( 1 / ( abs ` x ) ) x. if ( x < 0 , -u 1 , 1 ) ) = ( 1 / x ) )
119 118 mpteq2ia 
 |-  ( x e. D |-> ( ( 1 / ( abs ` x ) ) x. if ( x < 0 , -u 1 , 1 ) ) ) = ( x e. D |-> ( 1 / x ) )
120 74 119 eqtri 
 |-  ( RR _D ( x e. D |-> ( log ` ( abs ` x ) ) ) ) = ( x e. D |-> ( 1 / x ) )