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 ax-mp ⊢ log : ( ℂ ∖ { 0 } ) ⟶ ran log
55 54 a1i ⊢ ( ⊤ → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
56 55 feqmptd ⊢ ( ⊤ → log = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( log ‘ 𝑦 ) ) )
57 56 mptru ⊢ log = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( log ‘ 𝑦 ) )
58 57 reseq1i ⊢ ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( log ‘ 𝑦 ) ) ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) )
59 c0ex ⊢ 0 ∈ V
60 59 snss ⊢ ( 0 ∈ ( -∞ (,] 0 ) ↔ { 0 } ⊆ ( -∞ (,] 0 ) )
61 42 60 mpbi ⊢ { 0 } ⊆ ( -∞ (,] 0 )
62 sscon ⊢ ( { 0 } ⊆ ( -∞ (,] 0 ) → ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ { 0 } ) )
63 resmpt ⊢ ( ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ( ℂ ∖ { 0 } ) → ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( log ‘ 𝑦 ) ) ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) )
64 61 62 63 mp2b ⊢ ( ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( log ‘ 𝑦 ) ) ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) )
65 58 64 eqtr2i ⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) = ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) )
66 65 oveq2i ⊢ ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) = ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
67 eqid ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
68 67 dvlog ⊢ ( ℂ D ( log ↾ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) )
69 66 68 eqtri ⊢ ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) )
70 69 a1i ⊢ ( ⊤ → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( log ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 1 / 𝑦 ) ) )
71 fveq2 ⊢ ( 𝑦 = ( abs ‘ 𝑥 ) → ( log ‘ 𝑦 ) = ( log ‘ ( abs ‘ 𝑥 ) ) )
72 oveq2 ⊢ ( 𝑦 = ( abs ‘ 𝑥 ) → ( 1 / 𝑦 ) = ( 1 / ( abs ‘ 𝑥 ) ) )
73 3 5 32 36 48 49 51 70 71 72 dvmptco ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( abs ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( abs ‘ 𝑥 ) ) · if ( 𝑥 < 0 , - 1 , 1 ) ) ) )
74 73 mptru ⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( abs ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( abs ‘ 𝑥 ) ) · if ( 𝑥 < 0 , - 1 , 1 ) ) )
75 ovif2 ⊢ ( ( 1 / ( abs ‘ 𝑥 ) ) · if ( 𝑥 < 0 , - 1 , 1 ) ) = if ( 𝑥 < 0 , ( ( 1 / ( abs ‘ 𝑥 ) ) · - 1 ) , ( ( 1 / ( abs ‘ 𝑥 ) ) · 1 ) )
76 simpll ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 𝑥 ∈ ℝ )
77 76 recnd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 𝑥 ∈ ℂ )
78 77 abscld ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) ∈ ℝ )
79 78 recnd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) ∈ ℂ )
80 simplr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 𝑥 ≠ 0 )
81 77 80 absne0d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) ≠ 0 )
82 79 81 reccld ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( 1 / ( abs ‘ 𝑥 ) ) ∈ ℂ )
83 neg1cn ⊢ - 1 ∈ ℂ
84 83 a1i ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → - 1 ∈ ℂ )
85 82 84 mulcomd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · - 1 ) = ( - 1 · ( 1 / ( abs ‘ 𝑥 ) ) ) )
86 82 mulm1d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( - 1 · ( 1 / ( abs ‘ 𝑥 ) ) ) = - ( 1 / ( abs ‘ 𝑥 ) ) )
87 1cnd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 1 ∈ ℂ )
88 87 79 81 divneg2d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → - ( 1 / ( abs ‘ 𝑥 ) ) = ( 1 / - ( abs ‘ 𝑥 ) ) )
89 0red ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 0 ∈ ℝ )
90 simpr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 𝑥 < 0 )
91 76 89 90 ltled ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → 𝑥 ≤ 0 )
92 76 91 absnidd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) = - 𝑥 )
93 92 eqcomd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → - 𝑥 = ( abs ‘ 𝑥 ) )
94 77 93 negcon1ad ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → - ( abs ‘ 𝑥 ) = 𝑥 )
95 94 oveq2d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( 1 / - ( abs ‘ 𝑥 ) ) = ( 1 / 𝑥 ) )
96 88 95 eqtrd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → - ( 1 / ( abs ‘ 𝑥 ) ) = ( 1 / 𝑥 ) )
97 85 86 96 3eqtrd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · - 1 ) = ( 1 / 𝑥 ) )
98 25 97 sylanb ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · - 1 ) = ( 1 / 𝑥 ) )
99 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
100 99 abscld ⊢ ( 𝑥 ∈ ℝ → ( abs ‘ 𝑥 ) ∈ ℝ )
101 100 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) ∈ ℝ )
102 99 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → 𝑥 ∈ ℂ )
103 simplr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → 𝑥 ≠ 0 )
104 102 103 absne0d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) ≠ 0 )
105 101 104 rereccld ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( 1 / ( abs ‘ 𝑥 ) ) ∈ ℝ )
106 105 recnd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( 1 / ( abs ‘ 𝑥 ) ) ∈ ℂ )
107 106 mulridd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · 1 ) = ( 1 / ( abs ‘ 𝑥 ) ) )
108 simpll ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → 𝑥 ∈ ℝ )
109 0red ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) → 0 ∈ ℝ )
110 simpl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) → 𝑥 ∈ ℝ )
111 109 110 lenltd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) → ( 0 ≤ 𝑥 ↔ ¬ 𝑥 < 0 ) )
112 111 biimpar ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → 0 ≤ 𝑥 )
113 108 112 absidd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( abs ‘ 𝑥 ) = 𝑥 )
114 113 oveq2d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( 1 / ( abs ‘ 𝑥 ) ) = ( 1 / 𝑥 ) )
115 107 114 eqtrd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · 1 ) = ( 1 / 𝑥 ) )
116 25 115 sylanb ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 < 0 ) → ( ( 1 / ( abs ‘ 𝑥 ) ) · 1 ) = ( 1 / 𝑥 ) )
117 98 116 ifeqda ⊢ ( 𝑥 ∈ 𝐷 → if ( 𝑥 < 0 , ( ( 1 / ( abs ‘ 𝑥 ) ) · - 1 ) , ( ( 1 / ( abs ‘ 𝑥 ) ) · 1 ) ) = ( 1 / 𝑥 ) )
118 75 117 eqtrid ⊢ ( 𝑥 ∈ 𝐷 → ( ( 1 / ( abs ‘ 𝑥 ) ) · if ( 𝑥 < 0 , - 1 , 1 ) ) = ( 1 / 𝑥 ) )
119 118 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ( 1 / ( abs ‘ 𝑥 ) ) · if ( 𝑥 < 0 , - 1 , 1 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )
120 74 119 eqtri ⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( log ‘ ( abs ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / 𝑥 ) )