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 / 𝑥 ) )