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

Proof

Step Hyp Ref Expression
1 redvabs.d ⊢ 𝐷 = ( ℝ ∖ { 0 } )
2 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
3 2 a1i ⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } )
4 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
5 4 a1i ⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } )
6 dfrp2 ⊢ ℝ+ = ( 0 (,) +∞ )
7 mnfxr ⊢ -∞ ∈ ℝ*
8 7 a1i ⊢ ( ⊤ → -∞ ∈ ℝ* )
9 0xr ⊢ 0 ∈ ℝ*
10 9 a1i ⊢ ( ⊤ → 0 ∈ ℝ* )
11 pnfxr ⊢ +∞ ∈ ℝ*
12 11 a1i ⊢ ( ⊤ → +∞ ∈ ℝ* )
13 8 10 12 iocioodisjd ⊢ ( ⊤ → ( ( -∞ (,] 0 ) ∩ ( 0 (,) +∞ ) ) = ∅ )
14 13 mptru ⊢ ( ( -∞ (,] 0 ) ∩ ( 0 (,) +∞ ) ) = ∅
15 14 ineqcomi ⊢ ( ( 0 (,) +∞ ) ∩ ( -∞ (,] 0 ) ) = ∅
16 disjdif2 ⊢ ( ( ( 0 (,) +∞ ) ∩ ( -∞ (,] 0 ) ) = ∅ → ( ( 0 (,) +∞ ) ∖ ( -∞ (,] 0 ) ) = ( 0 (,) +∞ ) )
17 15 16 ax-mp ⊢ ( ( 0 (,) +∞ ) ∖ ( -∞ (,] 0 ) ) = ( 0 (,) +∞ )
18 6 17 eqtr4i ⊢ ℝ+ = ( ( 0 (,) +∞ ) ∖ ( -∞ (,] 0 ) )
19 ioosscn ⊢ ( 0 (,) +∞ ) ⊆ ℂ
20 ssdif ⊢ ( ( 0 (,) +∞ ) ⊆ ℂ → ( ( 0 (,) +∞ ) ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) )
21 19 20 ax-mp ⊢ ( ( 0 (,) +∞ ) ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ ( -∞ (,] 0 ) )
22 18 21 eqsstri ⊢ ℝ+ ⊆ ( ℂ ∖ ( -∞ (,] 0 ) )
23 1 eleq2i ⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ ( ℝ ∖ { 0 } ) )
24 eldifsn ⊢ ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) )
25 23 24 bitri ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) )
26 25 simplbi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℝ )
27 26 recnd ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
28 27 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ℂ )
29 25 simprbi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 )
30 29 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ≠ 0 )
31 28 30 absrpcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( abs ‘ 𝑥 ) ∈ ℝ+ )
32 22 31 sselid ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( abs ‘ 𝑥 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
33 negex ⊢ - 1 ∈ V
34 1ex ⊢ 1 ∈ V
35 33 34 ifex ⊢ if ( 𝑥 < 0 , - 1 , 1 ) ∈ V
36 35 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → if ( 𝑥 < 0 , - 1 , 1 ) ∈ V )
37 eldifi ⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝑦 ∈ ℂ )
38 37 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → 𝑦 ∈ ℂ )
39 eldifn ⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ¬ 𝑦 ∈ ( -∞ (,] 0 ) )
40 mnflt0 ⊢ -∞ < 0
41 ubioc1 ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ -∞ < 0 ) → 0 ∈ ( -∞ (,] 0 ) )
42 7 9 40 41 mp3an ⊢ 0 ∈ ( -∞ (,] 0 )
43 eleq1 ⊢ ( 𝑦 = 0 → ( 𝑦 ∈ ( -∞ (,] 0 ) ↔ 0 ∈ ( -∞ (,] 0 ) ) )
44 42 43 mpbiri ⊢ ( 𝑦 = 0 → 𝑦 ∈ ( -∞ (,] 0 ) )
45 44 necon3bi ⊢ ( ¬ 𝑦 ∈ ( -∞ (,] 0 ) → 𝑦 ≠ 0 )
46 39 45 syl ⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝑦 ≠ 0 )
47 46 adantl ⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → 𝑦 ≠ 0 )
48 38 47 logcld ⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( log ‘ 𝑦 ) ∈ ℂ )
49 ovexd ⊢ ( ( ⊤ ∧ 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( 1 / 𝑦 ) ∈ V )
50 1 redvmptabs ⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 < 0 , - 1 , 1 ) )
51 50 a1i ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 < 0 , - 1 , 1 ) ) )
52 logf1o ⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
53 f1of ⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
54 52 53 mp1i ⊢ ( ⊤ → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
55 eqid ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
56 55 logdmss ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ { 0 } )
57 56 a1i ⊢ ( ⊤ → ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ { 0 } ) )
58 54 57 feqresmpt ⊢ ( ⊤ → ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) )
59 58 mptru ⊢ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) )
60 59 oveq2i ⊢ ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) )
61 55 dvlog ⊢ ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) )
62 60 61 eqtr3i ⊢ ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) )
63 62 a1i ⊢ ( ⊤ → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) ) )
64 fveq2 ⊢ ( 𝑦 = ( abs ‘ 𝑥 ) → ( log ‘ 𝑦 ) = ( log ‘ ( abs ‘ 𝑥 ) ) )
65 oveq2 ⊢ ( 𝑦 = ( abs ‘ 𝑥 ) → ( 1 / 𝑦 ) = ( 1 / ( abs ‘ 𝑥 ) ) )
66 3 5 32 36 48 49 51 63 64 65 dvmptco ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( abs ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( abs ‘ 𝑥 ) ) · if ( 𝑥 < 0 , - 1 , 1 ) ) ) )
67 66 mptru ⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( abs ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( abs ‘ 𝑥 ) ) · if ( 𝑥 < 0 , - 1 , 1 ) ) )
68 ovif2 ⊢ ( ( 1 / ( abs ‘ 𝑥 ) ) · if ( 𝑥 < 0 , - 1 , 1 ) ) = if ( 𝑥 < 0 , ( ( 1 / ( abs ‘ 𝑥 ) ) · - 1 ) , ( ( 1 / ( abs ‘ 𝑥 ) ) · 1 ) )
69 simpll ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 𝑥 ∈ ℝ )
70 69 recnd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 𝑥 ∈ ℂ )
71 70 abscld ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) ∈ ℝ )
72 71 recnd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) ∈ ℂ )
73 simplr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 𝑥 ≠ 0 )
74 70 73 absne0d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) ≠ 0 )
75 72 74 reccld ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( 1 / ( abs ‘ 𝑥 ) ) ∈ ℂ )
76 neg1cn ⊢ - 1 ∈ ℂ
77 76 a1i ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → - 1 ∈ ℂ )
78 75 77 mulcomd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · - 1 ) = ( - 1 · ( 1 / ( abs ‘ 𝑥 ) ) ) )
79 75 mulm1d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( - 1 · ( 1 / ( abs ‘ 𝑥 ) ) ) = - ( 1 / ( abs ‘ 𝑥 ) ) )
80 1cnd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 1 ∈ ℂ )
81 80 72 74 divneg2d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → - ( 1 / ( abs ‘ 𝑥 ) ) = ( 1 / - ( abs ‘ 𝑥 ) ) )
82 0red ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 0 ∈ ℝ )
83 simpr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 𝑥 < 0 )
84 69 82 83 ltled ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 𝑥 ≤ 0 )
85 69 84 absnidd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) = - 𝑥 )
86 85 eqcomd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → - 𝑥 = ( abs ‘ 𝑥 ) )
87 70 86 negcon1ad ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → - ( abs ‘ 𝑥 ) = 𝑥 )
88 87 oveq2d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( 1 / - ( abs ‘ 𝑥 ) ) = ( 1 / 𝑥 ) )
89 81 88 eqtrd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → - ( 1 / ( abs ‘ 𝑥 ) ) = ( 1 / 𝑥 ) )
90 78 79 89 3eqtrd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · - 1 ) = ( 1 / 𝑥 ) )
91 25 90 sylanb ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · - 1 ) = ( 1 / 𝑥 ) )
92 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
93 92 abscld ⊢ ( 𝑥 ∈ ℝ → ( abs ‘ 𝑥 ) ∈ ℝ )
94 93 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) ∈ ℝ )
95 92 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → 𝑥 ∈ ℂ )
96 simplr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → 𝑥 ≠ 0 )
97 95 96 absne0d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) ≠ 0 )
98 94 97 rereccld ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( 1 / ( abs ‘ 𝑥 ) ) ∈ ℝ )
99 98 recnd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( 1 / ( abs ‘ 𝑥 ) ) ∈ ℂ )
100 99 mulridd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · 1 ) = ( 1 / ( abs ‘ 𝑥 ) ) )
101 simpll ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → 𝑥 ∈ ℝ )
102 0red ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) → 0 ∈ ℝ )
103 simpl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) → 𝑥 ∈ ℝ )
104 102 103 lenltd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) → ( 0 ≤ 𝑥 ↔ ¬ 𝑥 < 0 ) )
105 104 biimpar ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → 0 ≤ 𝑥 )
106 101 105 absidd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) = 𝑥 )
107 106 oveq2d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( 1 / ( abs ‘ 𝑥 ) ) = ( 1 / 𝑥 ) )
108 100 107 eqtrd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · 1 ) = ( 1 / 𝑥 ) )
109 25 108 sylanb ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · 1 ) = ( 1 / 𝑥 ) )
110 91 109 ifeqda ⊢ ( 𝑥 ∈ 𝐷 → if ( 𝑥 < 0 , ( ( 1 / ( abs ‘ 𝑥 ) ) · - 1 ) , ( ( 1 / ( abs ‘ 𝑥 ) ) · 1 ) ) = ( 1 / 𝑥 ) )
111 68 110 eqtrid ⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / ( abs ‘ 𝑥 ) ) · if ( 𝑥 < 0 , - 1 , 1 ) ) = ( 1 / 𝑥 ) )
112 111 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( abs ‘ 𝑥 ) ) · if ( 𝑥 < 0 , - 1 , 1 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )
113 67 112 eqtri ⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( abs ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )