redvmptabs - Mathbox for Steven Nguyen

	Mathbox for Steven Nguyen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > redvmptabs		Structured version Visualization version GIF version

Theorem redvmptabs 42557

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

**Hypothesis**
Ref	Expression
redvabs.d	⊢ 𝐷 = (ℝ ∖ {0})

**Assertion**
Ref	Expression
redvmptabs	⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))

Distinct variable group: 𝑥,𝐷

Proof of Theorem redvmptabs Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		partfun 6637	. . 3 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -1, 1)) = ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -1) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 1))
2		reelprrecn 11116	. . . . . . 7 ⊢ ℝ ∈ {ℝ, ℂ}
3	2	a1i 11	. . . . . 6 ⊢ (⊤ → ℝ ∈ {ℝ, ℂ})
4		inss1 4187	. . . . . . . . 9 ⊢ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ⊆ 𝐷
5		redvabs.d	. . . . . . . . . . 11 ⊢ 𝐷 = (ℝ ∖ {0})
6		difss 4086	. . . . . . . . . . 11 ⊢ (ℝ ∖ {0}) ⊆ ℝ
7	5, 6	eqsstri 3978	. . . . . . . . . 10 ⊢ 𝐷 ⊆ ℝ
8		ax-resscn 11081	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
9	7, 8	sstri 3941	. . . . . . . . 9 ⊢ 𝐷 ⊆ ℂ
10	4, 9	sstri 3941	. . . . . . . 8 ⊢ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ⊆ ℂ
11	10	sseli 3927	. . . . . . 7 ⊢ (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) → 𝑥 ∈ ℂ)
12	11	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) → 𝑥 ∈ ℂ)
13		1cnd 11125	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) → 1 ∈ ℂ)
14	8	a1i 11	. . . . . . . 8 ⊢ (⊤ → ℝ ⊆ ℂ)
15	14	sselda 3931	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
16		1red 11131	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
17	3	dvmptid 25915	. . . . . . 7 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
18		ssinss1 4196	. . . . . . . 8 ⊢ (𝐷 ⊆ ℝ → (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ⊆ ℝ)
19	7, 18	mp1i 13	. . . . . . 7 ⊢ (⊤ → (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ⊆ ℝ)
20		tgioo4 24747	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
21		eqid 2734	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
22	5	eleq2i 2826	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖ {0}))
23		eldifsn 4740	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (ℝ ∖ {0}) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≠ 0))
24	22, 23	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≠ 0))
25		vex 3442	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
26		breq1 5099	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 < 0 ↔ 𝑥 < 0))
27	25, 26	elab 3632	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑦 ∣ 𝑦 < 0} ↔ 𝑥 < 0)
28	24, 27	anbi12i 628	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0))
29		lt0ne0 11601	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 < 0) → 𝑥 ≠ 0)
30	29	expcom 413	. . . . . . . . . . . . . . 15 ⊢ (𝑥 < 0 → (𝑥 ∈ ℝ → 𝑥 ≠ 0))
31	30	pm4.71d 561	. . . . . . . . . . . . . 14 ⊢ (𝑥 < 0 → (𝑥 ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≠ 0)))
32	31	bicomd 223	. . . . . . . . . . . . 13 ⊢ (𝑥 < 0 → ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ↔ 𝑥 ∈ ℝ))
33	32	pm5.32ri 575	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 0))
34	28, 33	bitri 275	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 0))
35		elin 3915	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}))
36		0xr 11177	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
37		elioomnf 13358	. . . . . . . . . . . 12 ⊢ (0 ∈ ℝ^* → (𝑥 ∈ (-∞(,)0) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 0)))
38	36, 37	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-∞(,)0) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 0))
39	34, 35, 38	3bitr4i 303	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↔ 𝑥 ∈ (-∞(,)0))
40	39	eqriv 2731	. . . . . . . . 9 ⊢ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) = (-∞(,)0)
41		iooretop 24707	. . . . . . . . 9 ⊢ (-∞(,)0) ∈ (topGen‘ran (,))
42	40, 41	eqeltri 2830	. . . . . . . 8 ⊢ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,))
43	42	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,)))
44	3, 15, 16, 17, 19, 20, 21, 43	dvmptres 25921	. . . . . 6 ⊢ (⊤ → (ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥)) = (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ 1))
45	3, 12, 13, 44	dvmptneg 25924	. . . . 5 ⊢ (⊤ → (ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥)) = (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -1))
46	45	mptru 1548	. . . 4 ⊢ (ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥)) = (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -1)
47	7	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐷 ⊆ ℝ)
48	47	ssdifssd 4097	. . . . . 6 ⊢ (⊤ → (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ⊆ ℝ)
49	27	notbii 320	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0} ↔ ¬ 𝑥 < 0)
50	24, 49	anbi12i 628	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0))
51		anass 468	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ≠ 0 ∧ ¬ 𝑥 < 0)))
52		elre0re 42451	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
53		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ)
54	52, 53	lttrid 11269	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (0 < 𝑥 ↔ ¬ (0 = 𝑥 ∨ 𝑥 < 0)))
55		ioran 985	. . . . . . . . . . . . . 14 ⊢ (¬ (0 = 𝑥 ∨ 𝑥 < 0) ↔ (¬ 0 = 𝑥 ∧ ¬ 𝑥 < 0))
56		nesym 2986	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ≠ 0 ↔ ¬ 0 = 𝑥)
57	56	bicomi 224	. . . . . . . . . . . . . 14 ⊢ (¬ 0 = 𝑥 ↔ 𝑥 ≠ 0)
58	55, 57	bianbi 627	. . . . . . . . . . . . 13 ⊢ (¬ (0 = 𝑥 ∨ 𝑥 < 0) ↔ (𝑥 ≠ 0 ∧ ¬ 𝑥 < 0))
59	54, 58	bitr2di 288	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((𝑥 ≠ 0 ∧ ¬ 𝑥 < 0) ↔ 0 < 𝑥))
60	59	pm5.32i 574	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ (𝑥 ≠ 0 ∧ ¬ 𝑥 < 0)) ↔ (𝑥 ∈ ℝ ∧ 0 < 𝑥))
61	50, 51, 60	3bitri 297	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}) ↔ (𝑥 ∈ ℝ ∧ 0 < 𝑥))
62		eldif 3909	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↔ (𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}))
63		repos 13360	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 < 𝑥))
64	61, 62, 63	3bitr4i 303	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↔ 𝑥 ∈ (0(,)+∞))
65	64	eqriv 2731	. . . . . . . 8 ⊢ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) = (0(,)+∞)
66		iooretop 24707	. . . . . . . 8 ⊢ (0(,)+∞) ∈ (topGen‘ran (,))
67	65, 66	eqeltri 2830	. . . . . . 7 ⊢ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,))
68	67	a1i 11	. . . . . 6 ⊢ (⊤ → (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,)))
69	3, 15, 16, 17, 48, 20, 21, 68	dvmptres 25921	. . . . 5 ⊢ (⊤ → (ℝ D (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥)) = (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 1))
70	69	mptru 1548	. . . 4 ⊢ (ℝ D (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥)) = (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 1)
71	46, 70	uneq12i 4116	. . 3 ⊢ ((ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥)) ∪ (ℝ D (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))) = ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -1) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 1))
72	12	negcld 11477	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) → -𝑥 ∈ ℂ)
73	72	fmpttd 7058	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥):(𝐷 ∩ {𝑦 ∣ 𝑦 < 0})⟶ℂ)
74		ssdifss 4090	. . . . . . . . . 10 ⊢ (𝐷 ⊆ ℝ → (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ⊆ ℝ)
75	7, 74	ax-mp 5	. . . . . . . . 9 ⊢ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ⊆ ℝ
76	75, 8	sstri 3941	. . . . . . . 8 ⊢ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ⊆ ℂ
77	76	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ⊆ ℂ)
78	77	sselda 3931	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) → 𝑥 ∈ ℂ)
79	78	fmpttd 7058	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥):(𝐷 ∖ {𝑦 ∣ 𝑦 < 0})⟶ℂ)
80		inindif 4325	. . . . . 6 ⊢ ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∩ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) = ∅
81	80	a1i 11	. . . . 5 ⊢ (⊤ → ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∩ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) = ∅)
82		retop 24703	. . . . . . . . 9 ⊢ (topGen‘ran (,)) ∈ Top
83		isopn3i 23024	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) = (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}))
84	82, 42, 83	mp2an 692	. . . . . . . 8 ⊢ ((int‘(topGen‘ran (,)))‘(𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) = (𝐷 ∩ {𝑦 ∣ 𝑦 < 0})
85		isopn3i 23024	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) = (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))
86	82, 67, 85	mp2an 692	. . . . . . . 8 ⊢ ((int‘(topGen‘ran (,)))‘(𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) = (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})
87	84, 86	uneq12i 4116	. . . . . . 7 ⊢ (((int‘(topGen‘ran (,)))‘(𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) ∪ ((int‘(topGen‘ran (,)))‘(𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))) = ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))
88		unopn 22845	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,)) ∧ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,))) → ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) ∈ (topGen‘ran (,)))
89	82, 42, 67, 88	mp3an 1463	. . . . . . . 8 ⊢ ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) ∈ (topGen‘ran (,))
90		isopn3i 23024	. . . . . . . 8 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))) = ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})))
91	82, 89, 90	mp2an 692	. . . . . . 7 ⊢ ((int‘(topGen‘ran (,)))‘((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))) = ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))
92	87, 91	eqtr4i 2760	. . . . . 6 ⊢ (((int‘(topGen‘ran (,)))‘(𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) ∪ ((int‘(topGen‘ran (,)))‘(𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))) = ((int‘(topGen‘ran (,)))‘((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})))
93	92	a1i 11	. . . . 5 ⊢ (⊤ → (((int‘(topGen‘ran (,)))‘(𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) ∪ ((int‘(topGen‘ran (,)))‘(𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))) = ((int‘(topGen‘ran (,)))‘((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))))
94	20, 21, 14, 73, 79, 19, 48, 81, 93	dvun 42556	. . . 4 ⊢ (⊤ → ((ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥)) ∪ (ℝ D (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))) = (ℝ D ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))))
95	94	mptru 1548	. . 3 ⊢ ((ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥)) ∪ (ℝ D (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))) = (ℝ D ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥)))
96	1, 71, 95	3eqtr2ri 2764	. 2 ⊢ (ℝ D ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -1, 1))
97		partfun 6637	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -𝑥, 𝑥)) = ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))
98		elioore 13289	. . . . . . . . . 10 ⊢ (𝑥 ∈ (-∞(,)0) → 𝑥 ∈ ℝ)
99		0red 11133	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-∞(,)0) → 0 ∈ ℝ)
100	38	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-∞(,)0) → 𝑥 < 0)
101	98, 99, 100	ltled 11279	. . . . . . . . . 10 ⊢ (𝑥 ∈ (-∞(,)0) → 𝑥 ≤ 0)
102	98, 101	absnidd 15335	. . . . . . . . 9 ⊢ (𝑥 ∈ (-∞(,)0) → (abs‘𝑥) = -𝑥)
103	102	eqcomd 2740	. . . . . . . 8 ⊢ (𝑥 ∈ (-∞(,)0) → -𝑥 = (abs‘𝑥))
104	103, 40	eleq2s 2852	. . . . . . 7 ⊢ (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) → -𝑥 = (abs‘𝑥))
105	35, 104	sylbir 235	. . . . . 6 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}) → -𝑥 = (abs‘𝑥))
106		rpabsid 42518	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘𝑥) = 𝑥)
107	106	eqcomd 2740	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 = (abs‘𝑥))
108		ioorp 13339	. . . . . . . . 9 ⊢ (0(,)+∞) = ℝ⁺
109	107, 108	eleq2s 2852	. . . . . . . 8 ⊢ (𝑥 ∈ (0(,)+∞) → 𝑥 = (abs‘𝑥))
110	109, 65	eleq2s 2852	. . . . . . 7 ⊢ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) → 𝑥 = (abs‘𝑥))
111	62, 110	sylbir 235	. . . . . 6 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}) → 𝑥 = (abs‘𝑥))
112	105, 111	ifeqda 4514	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -𝑥, 𝑥) = (abs‘𝑥))
113	112	mpteq2ia 5191	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -𝑥, 𝑥)) = (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))
114	97, 113	eqtr3i 2759	. . 3 ⊢ ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))
115	114	oveq2i 7367	. 2 ⊢ (ℝ D ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))) = (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥)))
116		eqid 2734	. . . 4 ⊢ 1 = 1
117	27, 116	ifbieq2i 4503	. . 3 ⊢ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -1, 1) = if(𝑥 < 0, -1, 1)
118	117	mpteq2i 5192	. 2 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -1, 1)) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))
119	96, 115, 118	3eqtr3i 2765	1 ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1541 ⊤wtru 1542 ∈ wcel 2113 {cab 2712 ≠ wne 2930 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4283 ifcif 4477 {csn 4578 {cpr 4580 class class class wbr 5096 ↦ cmpt 5177 ran crn 5623 ‘cfv 6490 (class class class)co 7356 ℂcc 11022 ℝcr 11023 0cc0 11024 1c1 11025 +∞cpnf 11161 -∞cmnf 11162 ℝ^*cxr 11163 < clt 11164 -cneg 11363 ℝ⁺crp 12903 (,)cioo 13259 abscabs 15155 TopOpenctopn 17339 topGenctg 17355 ℂ_fldccnfld 21307 Topctop 22835 intcnt 22959 D cdv 25818

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101 ax-pre-sup 11102 ax-addf 11103

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-tp 4583 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-iin 4947 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8633 df-map 8763 df-pm 8764 df-ixp 8834 df-en 8882 df-dom 8883 df-sdom 8884 df-fin 8885 df-fsupp 9263 df-fi 9312 df-sup 9343 df-inf 9344 df-oi 9413 df-card 9849 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-div 11793 df-nn 12144 df-2 12206 df-3 12207 df-4 12208 df-5 12209 df-6 12210 df-7 12211 df-8 12212 df-9 12213 df-n0 12400 df-z 12487 df-dec 12606 df-uz 12750 df-q 12860 df-rp 12904 df-xneg 13024 df-xadd 13025 df-xmul 13026 df-ioo 13263 df-icc 13266 df-fz 13422 df-fzo 13569 df-seq 13923 df-exp 13983 df-hash 14252 df-cj 15020 df-re 15021 df-im 15022 df-sqrt 15156 df-abs 15157 df-struct 17072 df-sets 17089 df-slot 17107 df-ndx 17119 df-base 17135 df-ress 17156 df-plusg 17188 df-mulr 17189 df-starv 17190 df-sca 17191 df-vsca 17192 df-ip 17193 df-tset 17194 df-ple 17195 df-ds 17197 df-unif 17198 df-hom 17199 df-cco 17200 df-rest 17340 df-topn 17341 df-0g 17359 df-gsum 17360 df-topgen 17361 df-pt 17362 df-prds 17365 df-xrs 17421 df-qtop 17426 df-imas 17427 df-xps 17429 df-mre 17503 df-mrc 17504 df-acs 17506 df-mgm 18563 df-sgrp 18642 df-mnd 18658 df-submnd 18707 df-mulg 18996 df-cntz 19244 df-cmn 19709 df-psmet 21299 df-xmet 21300 df-met 21301 df-bl 21302 df-mopn 21303 df-fbas 21304 df-fg 21305 df-cnfld 21308 df-top 22836 df-topon 22853 df-topsp 22875 df-bases 22888 df-cld 22961 df-ntr 22962 df-cls 22963 df-nei 23040 df-lp 23078 df-perf 23079 df-cn 23169 df-cnp 23170 df-haus 23257 df-tx 23504 df-hmeo 23697 df-fil 23788 df-fm 23880 df-flim 23881 df-flf 23882 df-xms 24262 df-ms 24263 df-tms 24264 df-cncf 24825 df-limc 25821 df-dv 25822

This theorem is referenced by: readvrec 42559

W3C validator