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

Metamath Proof Explorer

Theorem readvrec

Proof