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 = ℝ ∖ \{0\}$
	Assertion	readvrec	$⊢ \frac{d (x \in D⟼ \log \|x\|)}{d_{ℝ} x} = (x \in D ⟼ \frac{1}{x})$

Proof

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

Metamath Proof Explorer

Theorem readvrec

Proof