redvmptabs

Description: The derivative of the absolute value, for real numbers. (Contributed by SN, 30-Sep-2025)

		Ref	Expression
	Hypothesis	redvabs.d	$⊢ D = ℝ ∖ \{0\}$
	Assertion	redvmptabs	$⊢ \frac{d (x \in D⟼ \|x\|)}{d_{ℝ} x} = (x \in D ⟼ if (x < 0, - 1, 1))$

Proof

Step	Hyp	Ref	Expression
1		redvabs.d	$⊢ D = ℝ ∖ \{0\}$
2		partfun	$⊢ (x \in D ⟼ if (x \in \{y \| y < 0\}, - 1, 1)) = (x \in (D \cap \{y \| y < 0\}) ⟼ - 1) \cup (x \in (D ∖ \{y \| y < 0\}) ⟼ 1)$
3		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
4	3	a1i	$⊢ ⊤ \to ℝ \in \{ℝ, ℂ\}$
5		inss1	$⊢ D \cap \{y \| y < 0\} \subseteq D$
6		difss	$⊢ ℝ ∖ \{0\} \subseteq ℝ$
7	1 6	eqsstri	$⊢ D \subseteq ℝ$
8		ax-resscn	$⊢ ℝ \subseteq ℂ$
9	7 8	sstri	$⊢ D \subseteq ℂ$
10	5 9	sstri	$⊢ D \cap \{y \| y < 0\} \subseteq ℂ$
11	10	sseli	$⊢ x \in (D \cap \{y \| y < 0\}) \to x \in ℂ$
12	11	adantl	$⊢ (⊤ \land x \in (D \cap \{y \| y < 0\})) \to x \in ℂ$
13		1cnd	$⊢ (⊤ \land x \in (D \cap \{y \| y < 0\})) \to 1 \in ℂ$
14	8	a1i	$⊢ ⊤ \to ℝ \subseteq ℂ$
15	14	sselda	$⊢ (⊤ \land x \in ℝ) \to x \in ℂ$
16		1red	$⊢ (⊤ \land x \in ℝ) \to 1 \in ℝ$
17	4	dvmptid	$⊢ ⊤ \to \frac{d (x \in ℝ⟼ x)}{d_{ℝ} x} = (x \in ℝ ⟼ 1)$
18		ssinss1	$⊢ D \subseteq ℝ \to D \cap \{y \| y < 0\} \subseteq ℝ$
19	7 18	mp1i	$⊢ ⊤ \to D \cap \{y \| y < 0\} \subseteq ℝ$
20		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
21	20	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
22	1	eleq2i	$⊢ x \in D \leftrightarrow x \in (ℝ ∖ \{0\})$
23		eldifsn	$⊢ x \in (ℝ ∖ \{0\}) \leftrightarrow (x \in ℝ \land x \neq 0)$
24	22 23	bitri	$⊢ x \in D \leftrightarrow (x \in ℝ \land x \neq 0)$
25		vex	$⊢ x \in V$
26		breq1	$⊢ y = x \to (y < 0 \leftrightarrow x < 0)$
27	25 26	elab	$⊢ x \in \{y \| y < 0\} \leftrightarrow x < 0$
28	24 27	anbi12i	$⊢ (x \in D \land x \in \{y \| y < 0\}) \leftrightarrow ((x \in ℝ \land x \neq 0) \land x < 0)$
29		lt0ne0	$⊢ (x \in ℝ \land x < 0) \to x \neq 0$
30	29	expcom	$⊢ x < 0 \to (x \in ℝ \to x \neq 0)$
31	30	pm4.71d	$⊢ x < 0 \to (x \in ℝ \leftrightarrow (x \in ℝ \land x \neq 0))$
32	31	bicomd	$⊢ x < 0 \to ((x \in ℝ \land x \neq 0) \leftrightarrow x \in ℝ)$
33	32	pm5.32ri	$⊢ ((x \in ℝ \land x \neq 0) \land x < 0) \leftrightarrow (x \in ℝ \land x < 0)$
34	28 33	bitri	$⊢ (x \in D \land x \in \{y \| y < 0\}) \leftrightarrow (x \in ℝ \land x < 0)$
35		elin	$⊢ x \in (D \cap \{y \| y < 0\}) \leftrightarrow (x \in D \land x \in \{y \| y < 0\})$
36		0xr	$⊢ 0 \in ℝ^{*}$
37		elioomnf	$⊢ 0 \in ℝ^{*} \to (x \in (−∞, 0) \leftrightarrow (x \in ℝ \land x < 0))$
38	36 37	ax-mp	$⊢ x \in (−∞, 0) \leftrightarrow (x \in ℝ \land x < 0)$
39	34 35 38	3bitr4i	$⊢ x \in (D \cap \{y \| y < 0\}) \leftrightarrow x \in (−∞, 0)$
40	39	eqriv	$⊢ D \cap \{y \| y < 0\} = (−∞, 0)$
41		iooretop	$⊢ (−∞, 0) \in topGen (ran (.))$
42	40 41	eqeltri	$⊢ D \cap \{y \| y < 0\} \in topGen (ran (.))$
43	42	a1i	$⊢ ⊤ \to D \cap \{y \| y < 0\} \in topGen (ran (.))$
44	4 15 16 17 19 21 20 43	dvmptres	$⊢ ⊤ \to \frac{d (x \in (D \cap \{y \| y < 0\})⟼ x)}{d_{ℝ} x} = (x \in (D \cap \{y \| y < 0\}) ⟼ 1)$
45	4 12 13 44	dvmptneg	$⊢ ⊤ \to \frac{d (x \in (D \cap \{y \| y < 0\})⟼ - x)}{d_{ℝ} x} = (x \in (D \cap \{y \| y < 0\}) ⟼ - 1)$
46	45	mptru	$⊢ \frac{d (x \in (D \cap \{y \| y < 0\})⟼ - x)}{d_{ℝ} x} = (x \in (D \cap \{y \| y < 0\}) ⟼ - 1)$
47	7	a1i	$⊢ ⊤ \to D \subseteq ℝ$
48	47	ssdifssd	$⊢ ⊤ \to D ∖ \{y \| y < 0\} \subseteq ℝ$
49	27	notbii	$⊢ \neg x \in \{y \| y < 0\} \leftrightarrow \neg x < 0$
50	24 49	anbi12i	$⊢ (x \in D \land \neg x \in \{y \| y < 0\}) \leftrightarrow ((x \in ℝ \land x \neq 0) \land \neg x < 0)$
51		anass	$⊢ ((x \in ℝ \land x \neq 0) \land \neg x < 0) \leftrightarrow (x \in ℝ \land (x \neq 0 \land \neg x < 0))$
52		elre0re	$⊢ x \in ℝ \to 0 \in ℝ$
53		id	$⊢ x \in ℝ \to x \in ℝ$
54	52 53	lttrid	$⊢ x \in ℝ \to (0 < x \leftrightarrow \neg (0 = x \lor x < 0))$
55		ioran	$⊢ \neg (0 = x \lor x < 0) \leftrightarrow (\neg 0 = x \land \neg x < 0)$
56		nesym	$⊢ x \neq 0 \leftrightarrow \neg 0 = x$
57	56	bicomi	$⊢ \neg 0 = x \leftrightarrow x \neq 0$
58	55 57	bianbi	$⊢ \neg (0 = x \lor x < 0) \leftrightarrow (x \neq 0 \land \neg x < 0)$
59	54 58	bitr2di	$⊢ x \in ℝ \to ((x \neq 0 \land \neg x < 0) \leftrightarrow 0 < x)$
60	59	pm5.32i	$⊢ (x \in ℝ \land (x \neq 0 \land \neg x < 0)) \leftrightarrow (x \in ℝ \land 0 < x)$
61	50 51 60	3bitri	$⊢ (x \in D \land \neg x \in \{y \| y < 0\}) \leftrightarrow (x \in ℝ \land 0 < x)$
62		eldif	$⊢ x \in (D ∖ \{y \| y < 0\}) \leftrightarrow (x \in D \land \neg x \in \{y \| y < 0\})$
63		repos	$⊢ x \in (0, +∞) \leftrightarrow (x \in ℝ \land 0 < x)$
64	61 62 63	3bitr4i	$⊢ x \in (D ∖ \{y \| y < 0\}) \leftrightarrow x \in (0, +∞)$
65	64	eqriv	$⊢ D ∖ \{y \| y < 0\} = (0, +∞)$
66		iooretop	$⊢ (0, +∞) \in topGen (ran (.))$
67	65 66	eqeltri	$⊢ D ∖ \{y \| y < 0\} \in topGen (ran (.))$
68	67	a1i	$⊢ ⊤ \to D ∖ \{y \| y < 0\} \in topGen (ran (.))$
69	4 15 16 17 48 21 20 68	dvmptres	$⊢ ⊤ \to \frac{d (x \in (D ∖ \{y \| y < 0\})⟼ x)}{d_{ℝ} x} = (x \in (D ∖ \{y \| y < 0\}) ⟼ 1)$
70	69	mptru	$⊢ \frac{d (x \in (D ∖ \{y \| y < 0\})⟼ x)}{d_{ℝ} x} = (x \in (D ∖ \{y \| y < 0\}) ⟼ 1)$
71	46 70	uneq12i	$⊢ \frac{d (x \in (D \cap \{y \| y < 0\})⟼ - x)}{d_{ℝ} x} \cup \frac{d (x \in (D ∖ \{y \| y < 0\})⟼ x)}{d_{ℝ} x} = (x \in (D \cap \{y \| y < 0\}) ⟼ - 1) \cup (x \in (D ∖ \{y \| y < 0\}) ⟼ 1)$
72	12	negcld	$⊢ (⊤ \land x \in (D \cap \{y \| y < 0\})) \to - x \in ℂ$
73	72	fmpttd	$⊢ ⊤ \to (x \in (D \cap \{y \| y < 0\}) ⟼ - x) : D \cap \{y \| y < 0\} ⟶ ℂ$
74		ssdifss	$⊢ D \subseteq ℝ \to D ∖ \{y \| y < 0\} \subseteq ℝ$
75	7 74	ax-mp	$⊢ D ∖ \{y \| y < 0\} \subseteq ℝ$
76	75 8	sstri	$⊢ D ∖ \{y \| y < 0\} \subseteq ℂ$
77	76	a1i	$⊢ ⊤ \to D ∖ \{y \| y < 0\} \subseteq ℂ$
78	77	sselda	$⊢ (⊤ \land x \in (D ∖ \{y \| y < 0\})) \to x \in ℂ$
79	78	fmpttd	$⊢ ⊤ \to (x \in (D ∖ \{y \| y < 0\}) ⟼ x) : D ∖ \{y \| y < 0\} ⟶ ℂ$
80		inindif	$⊢ (D \cap \{y \| y < 0\}) \cap (D ∖ \{y \| y < 0\}) = \emptyset$
81	80	a1i	$⊢ ⊤ \to (D \cap \{y \| y < 0\}) \cap (D ∖ \{y \| y < 0\}) = \emptyset$
82		retop	$⊢ topGen (ran (.)) \in Top$
83		isopn3i	$⊢ (topGen (ran (.)) \in Top \land D \cap \{y \| y < 0\} \in topGen (ran (.))) \to int (topGen (ran (.))) (D \cap \{y \| y < 0\}) = D \cap \{y \| y < 0\}$
84	82 42 83	mp2an	$⊢ int (topGen (ran (.))) (D \cap \{y \| y < 0\}) = D \cap \{y \| y < 0\}$
85		isopn3i	$⊢ (topGen (ran (.)) \in Top \land D ∖ \{y \| y < 0\} \in topGen (ran (.))) \to int (topGen (ran (.))) (D ∖ \{y \| y < 0\}) = D ∖ \{y \| y < 0\}$
86	82 67 85	mp2an	$⊢ int (topGen (ran (.))) (D ∖ \{y \| y < 0\}) = D ∖ \{y \| y < 0\}$
87	84 86	uneq12i	$⊢ int (topGen (ran (.))) (D \cap \{y \| y < 0\}) \cup int (topGen (ran (.))) (D ∖ \{y \| y < 0\}) = (D \cap \{y \| y < 0\}) \cup (D ∖ \{y \| y < 0\})$
88		unopn	$⊢ (topGen (ran (.)) \in Top \land D \cap \{y \| y < 0\} \in topGen (ran (.)) \land D ∖ \{y \| y < 0\} \in topGen (ran (.))) \to (D \cap \{y \| y < 0\}) \cup (D ∖ \{y \| y < 0\}) \in topGen (ran (.))$
89	82 42 67 88	mp3an	$⊢ (D \cap \{y \| y < 0\}) \cup (D ∖ \{y \| y < 0\}) \in topGen (ran (.))$
90		isopn3i	$⊢ (topGen (ran (.)) \in Top \land (D \cap \{y \| y < 0\}) \cup (D ∖ \{y \| y < 0\}) \in topGen (ran (.))) \to int (topGen (ran (.))) ((D \cap \{y \| y < 0\}) \cup (D ∖ \{y \| y < 0\})) = (D \cap \{y \| y < 0\}) \cup (D ∖ \{y \| y < 0\})$
91	82 89 90	mp2an	$⊢ int (topGen (ran (.))) ((D \cap \{y \| y < 0\}) \cup (D ∖ \{y \| y < 0\})) = (D \cap \{y \| y < 0\}) \cup (D ∖ \{y \| y < 0\})$
92	87 91	eqtr4i	$⊢ int (topGen (ran (.))) (D \cap \{y \| y < 0\}) \cup int (topGen (ran (.))) (D ∖ \{y \| y < 0\}) = int (topGen (ran (.))) ((D \cap \{y \| y < 0\}) \cup (D ∖ \{y \| y < 0\}))$
93	92	a1i	$⊢ ⊤ \to int (topGen (ran (.))) (D \cap \{y \| y < 0\}) \cup int (topGen (ran (.))) (D ∖ \{y \| y < 0\}) = int (topGen (ran (.))) ((D \cap \{y \| y < 0\}) \cup (D ∖ \{y \| y < 0\}))$
94	21 20 14 73 79 19 48 81 93	dvun	$⊢ ⊤ \to \frac{d (x \in (D \cap \{y \| y < 0\})⟼ - x)}{d_{ℝ} x} \cup \frac{d (x \in (D ∖ \{y \| y < 0\})⟼ x)}{d_{ℝ} x} = ℝ D ((x \in (D \cap \{y \| y < 0\}) ⟼ - x) \cup (x \in (D ∖ \{y \| y < 0\}) ⟼ x))$
95	94	mptru	$⊢ \frac{d (x \in (D \cap \{y \| y < 0\})⟼ - x)}{d_{ℝ} x} \cup \frac{d (x \in (D ∖ \{y \| y < 0\})⟼ x)}{d_{ℝ} x} = ℝ D ((x \in (D \cap \{y \| y < 0\}) ⟼ - x) \cup (x \in (D ∖ \{y \| y < 0\}) ⟼ x))$
96	2 71 95	3eqtr2ri	$⊢ ℝ D ((x \in (D \cap \{y \| y < 0\}) ⟼ - x) \cup (x \in (D ∖ \{y \| y < 0\}) ⟼ x)) = (x \in D ⟼ if (x \in \{y \| y < 0\}, - 1, 1))$
97		partfun	$⊢ (x \in D ⟼ if (x \in \{y \| y < 0\}, - x, x)) = (x \in (D \cap \{y \| y < 0\}) ⟼ - x) \cup (x \in (D ∖ \{y \| y < 0\}) ⟼ x)$
98		elioore	$⊢ x \in (−∞, 0) \to x \in ℝ$
99		0red	$⊢ x \in (−∞, 0) \to 0 \in ℝ$
100	38	simprbi	$⊢ x \in (−∞, 0) \to x < 0$
101	98 99 100	ltled	$⊢ x \in (−∞, 0) \to x \leq 0$
102	98 101	absnidd	$⊢ x \in (−∞, 0) \to \|x\| = - x$
103	102	eqcomd	$⊢ x \in (−∞, 0) \to - x = \|x\|$
104	103 40	eleq2s	$⊢ x \in (D \cap \{y \| y < 0\}) \to - x = \|x\|$
105	35 104	sylbir	$⊢ (x \in D \land x \in \{y \| y < 0\}) \to - x = \|x\|$
106		rpabsid	$⊢ x \in ℝ^{+} \to \|x\| = x$
107	106	eqcomd	$⊢ x \in ℝ^{+} \to x = \|x\|$
108		ioorp	$⊢ (0, +∞) = ℝ^{+}$
109	107 108	eleq2s	$⊢ x \in (0, +∞) \to x = \|x\|$
110	109 65	eleq2s	$⊢ x \in (D ∖ \{y \| y < 0\}) \to x = \|x\|$
111	62 110	sylbir	$⊢ (x \in D \land \neg x \in \{y \| y < 0\}) \to x = \|x\|$
112	105 111	ifeqda	$⊢ x \in D \to if (x \in \{y \| y < 0\}, - x, x) = \|x\|$
113	112	mpteq2ia	$⊢ (x \in D ⟼ if (x \in \{y \| y < 0\}, - x, x)) = (x \in D ⟼ \|x\|)$
114	97 113	eqtr3i	$⊢ (x \in (D \cap \{y \| y < 0\}) ⟼ - x) \cup (x \in (D ∖ \{y \| y < 0\}) ⟼ x) = (x \in D ⟼ \|x\|)$
115	114	oveq2i	$⊢ ℝ D ((x \in (D \cap \{y \| y < 0\}) ⟼ - x) \cup (x \in (D ∖ \{y \| y < 0\}) ⟼ x)) = \frac{d (x \in D⟼ \|x\|)}{d_{ℝ} x}$
116		eqid	$⊢ 1 = 1$
117	27 116	ifbieq2i	$⊢ if (x \in \{y \| y < 0\}, - 1, 1) = if (x < 0, - 1, 1)$
118	117	mpteq2i	$⊢ (x \in D ⟼ if (x \in \{y \| y < 0\}, - 1, 1)) = (x \in D ⟼ if (x < 0, - 1, 1))$
119	96 115 118	3eqtr3i	$⊢ \frac{d (x \in D⟼ \|x\|)}{d_{ℝ} x} = (x \in D ⟼ if (x < 0, - 1, 1))$

Metamath Proof Explorer

Theorem redvmptabs

Proof