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 42791

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 11119	. . . . . . 7 ⊢ ℝ ∈ {ℝ, ℂ}
3	2	a1i 11	. . . . . 6 ⊢ (⊤ → ℝ ∈ {ℝ, ℂ})
4		inss1 4178	. . . . . . . . 9 ⊢ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ⊆ 𝐷
5		redvabs.d	. . . . . . . . . . 11 ⊢ 𝐷 = (ℝ ∖ {0})
6		difss 4077	. . . . . . . . . . 11 ⊢ (ℝ ∖ {0}) ⊆ ℝ
7	5, 6	eqsstri 3969	. . . . . . . . . 10 ⊢ 𝐷 ⊆ ℝ
8		ax-resscn 11084	. . . . . . . . . 10 ⊢ ℝ ⊆ ℂ
9	7, 8	sstri 3932	. . . . . . . . 9 ⊢ 𝐷 ⊆ ℂ
10	4, 9	sstri 3932	. . . . . . . 8 ⊢ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ⊆ ℂ
11	10	sseli 3918	. . . . . . 7 ⊢ (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) → 𝑥 ∈ ℂ)
12	11	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) → 𝑥 ∈ ℂ)
13		1cnd 11128	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) → 1 ∈ ℂ)
14	8	a1i 11	. . . . . . . 8 ⊢ (⊤ → ℝ ⊆ ℂ)
15	14	sselda 3922	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
16		1red 11134	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
17	3	dvmptid 25902	. . . . . . 7 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
18		ssinss1 4187	. . . . . . . 8 ⊢ (𝐷 ⊆ ℝ → (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ⊆ ℝ)
19	7, 18	mp1i 13	. . . . . . 7 ⊢ (⊤ → (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ⊆ ℝ)
20		tgioo4 24748	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
21		eqid 2737	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
22	5	eleq2i 2829	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖ {0}))
23		eldifsn 4730	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (ℝ ∖ {0}) ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≠ 0))
24	22, 23	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ ℝ ∧ 𝑥 ≠ 0))
25		vex 3434	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
26		breq1 5089	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 < 0 ↔ 𝑥 < 0))
27	25, 26	elab 3623	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑦 ∣ 𝑦 < 0} ↔ 𝑥 < 0)
28	24, 27	anbi12i 629	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ 𝑥 < 0))
29		lt0ne0 11604	. . . . . . . . . . . . . . . 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 3906	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}))
36		0xr 11180	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
37		elioomnf 13361	. . . . . . . . . . . 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 2734	. . . . . . . . 9 ⊢ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) = (-∞(,)0)
41		iooretop 24708	. . . . . . . . 9 ⊢ (-∞(,)0) ∈ (topGen‘ran (,))
42	40, 41	eqeltri 2833	. . . . . . . 8 ⊢ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,))
43	42	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,)))
44	3, 15, 16, 17, 19, 20, 21, 43	dvmptres 25908	. . . . . 6 ⊢ (⊤ → (ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥)) = (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ 1))
45	3, 12, 13, 44	dvmptneg 25911	. . . . 5 ⊢ (⊤ → (ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥)) = (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -1))
46	45	mptru 1549	. . . 4 ⊢ (ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥)) = (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -1)
47	7	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐷 ⊆ ℝ)
48	47	ssdifssd 4088	. . . . . 6 ⊢ (⊤ → (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ⊆ ℝ)
49	27	notbii 320	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0} ↔ ¬ 𝑥 < 0)
50	24, 49	anbi12i 629	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}) ↔ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0))
51		anass 468	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) ∧ ¬ 𝑥 < 0) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ≠ 0 ∧ ¬ 𝑥 < 0)))
52		elre0re 42685	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
53		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ)
54	52, 53	lttrid 11272	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (0 < 𝑥 ↔ ¬ (0 = 𝑥 ∨ 𝑥 < 0)))
55		ioran 986	. . . . . . . . . . . . . 14 ⊢ (¬ (0 = 𝑥 ∨ 𝑥 < 0) ↔ (¬ 0 = 𝑥 ∧ ¬ 𝑥 < 0))
56		nesym 2989	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ≠ 0 ↔ ¬ 0 = 𝑥)
57	56	bicomi 224	. . . . . . . . . . . . . 14 ⊢ (¬ 0 = 𝑥 ↔ 𝑥 ≠ 0)
58	55, 57	bianbi 628	. . . . . . . . . . . . 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 3900	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↔ (𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}))
63		repos 13363	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 < 𝑥))
64	61, 62, 63	3bitr4i 303	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↔ 𝑥 ∈ (0(,)+∞))
65	64	eqriv 2734	. . . . . . . 8 ⊢ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) = (0(,)+∞)
66		iooretop 24708	. . . . . . . 8 ⊢ (0(,)+∞) ∈ (topGen‘ran (,))
67	65, 66	eqeltri 2833	. . . . . . 7 ⊢ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,))
68	67	a1i 11	. . . . . 6 ⊢ (⊤ → (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,)))
69	3, 15, 16, 17, 48, 20, 21, 68	dvmptres 25908	. . . . 5 ⊢ (⊤ → (ℝ D (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥)) = (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 1))
70	69	mptru 1549	. . . 4 ⊢ (ℝ D (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥)) = (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 1)
71	46, 70	uneq12i 4107	. . 3 ⊢ ((ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥)) ∪ (ℝ D (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))) = ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -1) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 1))
72	12	negcld 11480	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) → -𝑥 ∈ ℂ)
73	72	fmpttd 7059	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥):(𝐷 ∩ {𝑦 ∣ 𝑦 < 0})⟶ℂ)
74		ssdifss 4081	. . . . . . . . . 10 ⊢ (𝐷 ⊆ ℝ → (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ⊆ ℝ)
75	7, 74	ax-mp 5	. . . . . . . . 9 ⊢ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ⊆ ℝ
76	75, 8	sstri 3932	. . . . . . . 8 ⊢ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ⊆ ℂ
77	76	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ⊆ ℂ)
78	77	sselda 3922	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) → 𝑥 ∈ ℂ)
79	78	fmpttd 7059	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥):(𝐷 ∖ {𝑦 ∣ 𝑦 < 0})⟶ℂ)
80		inindif 4316	. . . . . 6 ⊢ ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∩ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) = ∅
81	80	a1i 11	. . . . 5 ⊢ (⊤ → ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∩ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) = ∅)
82		retop 24704	. . . . . . . . 9 ⊢ (topGen‘ran (,)) ∈ Top
83		isopn3i 23025	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) = (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}))
84	82, 42, 83	mp2an 693	. . . . . . . 8 ⊢ ((int‘(topGen‘ran (,)))‘(𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) = (𝐷 ∩ {𝑦 ∣ 𝑦 < 0})
85		isopn3i 23025	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) = (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))
86	82, 67, 85	mp2an 693	. . . . . . . 8 ⊢ ((int‘(topGen‘ran (,)))‘(𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) = (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})
87	84, 86	uneq12i 4107	. . . . . . 7 ⊢ (((int‘(topGen‘ran (,)))‘(𝐷 ∩ {𝑦 ∣ 𝑦 < 0})) ∪ ((int‘(topGen‘ran (,)))‘(𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))) = ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))
88		unopn 22846	. . . . . . . . 9 ⊢ (((topGen‘ran (,)) ∈ Top ∧ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,)) ∧ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ∈ (topGen‘ran (,))) → ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) ∈ (topGen‘ran (,)))
89	82, 42, 67, 88	mp3an 1464	. . . . . . . 8 ⊢ ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) ∈ (topGen‘ran (,))
90		isopn3i 23025	. . . . . . . 8 ⊢ (((topGen‘ran (,)) ∈ Top ∧ ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))) = ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0})))
91	82, 89, 90	mp2an 693	. . . . . . 7 ⊢ ((int‘(topGen‘ran (,)))‘((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))) = ((𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ∪ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}))
92	87, 91	eqtr4i 2763	. . . . . 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 42790	. . . 4 ⊢ (⊤ → ((ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥)) ∪ (ℝ D (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))) = (ℝ D ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))))
95	94	mptru 1549	. . 3 ⊢ ((ℝ D (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥)) ∪ (ℝ D (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))) = (ℝ D ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥)))
96	1, 71, 95	3eqtr2ri 2767	. 2 ⊢ (ℝ D ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -1, 1))
97		partfun 6637	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -𝑥, 𝑥)) = ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))
98		elioore 13292	. . . . . . . . . 10 ⊢ (𝑥 ∈ (-∞(,)0) → 𝑥 ∈ ℝ)
99		0red 11136	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-∞(,)0) → 0 ∈ ℝ)
100	38	simprbi 497	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-∞(,)0) → 𝑥 < 0)
101	98, 99, 100	ltled 11282	. . . . . . . . . 10 ⊢ (𝑥 ∈ (-∞(,)0) → 𝑥 ≤ 0)
102	98, 101	absnidd 15338	. . . . . . . . 9 ⊢ (𝑥 ∈ (-∞(,)0) → (abs‘𝑥) = -𝑥)
103	102	eqcomd 2743	. . . . . . . 8 ⊢ (𝑥 ∈ (-∞(,)0) → -𝑥 = (abs‘𝑥))
104	103, 40	eleq2s 2855	. . . . . . 7 ⊢ (𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) → -𝑥 = (abs‘𝑥))
105	35, 104	sylbir 235	. . . . . 6 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}) → -𝑥 = (abs‘𝑥))
106		rpabsid 42752	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘𝑥) = 𝑥)
107	106	eqcomd 2743	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 = (abs‘𝑥))
108		ioorp 13342	. . . . . . . . 9 ⊢ (0(,)+∞) = ℝ⁺
109	107, 108	eleq2s 2855	. . . . . . . 8 ⊢ (𝑥 ∈ (0(,)+∞) → 𝑥 = (abs‘𝑥))
110	109, 65	eleq2s 2855	. . . . . . 7 ⊢ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) → 𝑥 = (abs‘𝑥))
111	62, 110	sylbir 235	. . . . . 6 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ {𝑦 ∣ 𝑦 < 0}) → 𝑥 = (abs‘𝑥))
112	105, 111	ifeqda 4504	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -𝑥, 𝑥) = (abs‘𝑥))
113	112	mpteq2ia 5181	. . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -𝑥, 𝑥)) = (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))
114	97, 113	eqtr3i 2762	. . 3 ⊢ ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))
115	114	oveq2i 7369	. 2 ⊢ (ℝ D ((𝑥 ∈ (𝐷 ∩ {𝑦 ∣ 𝑦 < 0}) ↦ -𝑥) ∪ (𝑥 ∈ (𝐷 ∖ {𝑦 ∣ 𝑦 < 0}) ↦ 𝑥))) = (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥)))
116		eqid 2737	. . . 4 ⊢ 1 = 1
117	27, 116	ifbieq2i 4493	. . 3 ⊢ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -1, 1) = if(𝑥 < 0, -1, 1)
118	117	mpteq2i 5182	. 2 ⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ {𝑦 ∣ 𝑦 < 0}, -1, 1)) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))
119	96, 115, 118	3eqtr3i 2768	1 ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1542 ⊤wtru 1543 ∈ wcel 2114 {cab 2715 ≠ wne 2933 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 ifcif 4467 {csn 4568 {cpr 4570 class class class wbr 5086 ↦ cmpt 5167 ran crn 5623 ‘cfv 6490 (class class class)co 7358 ℂcc 11025 ℝcr 11026 0cc0 11027 1c1 11028 +∞cpnf 11164 -∞cmnf 11165 ℝ^*cxr 11166 < clt 11167 -cneg 11366 ℝ⁺crp 12906 (,)cioo 13262 abscabs 15158 TopOpenctopn 17342 topGenctg 17358 ℂ_fldccnfld 21311 Topctop 22836 intcnt 22960 D cdv 25808

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104 ax-pre-sup 11105 ax-addf 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 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 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8102 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-er 8634 df-map 8766 df-pm 8767 df-ixp 8837 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-fsupp 9266 df-fi 9315 df-sup 9346 df-inf 9347 df-oi 9416 df-card 9852 df-pnf 11169 df-mnf 11170 df-xr 11171 df-ltxr 11172 df-le 11173 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-7 12214 df-8 12215 df-9 12216 df-n0 12403 df-z 12490 df-dec 12609 df-uz 12753 df-q 12863 df-rp 12907 df-xneg 13027 df-xadd 13028 df-xmul 13029 df-ioo 13266 df-icc 13269 df-fz 13425 df-fzo 13572 df-seq 13926 df-exp 13986 df-hash 14255 df-cj 15023 df-re 15024 df-im 15025 df-sqrt 15159 df-abs 15160 df-struct 17075 df-sets 17092 df-slot 17110 df-ndx 17122 df-base 17138 df-ress 17159 df-plusg 17191 df-mulr 17192 df-starv 17193 df-sca 17194 df-vsca 17195 df-ip 17196 df-tset 17197 df-ple 17198 df-ds 17200 df-unif 17201 df-hom 17202 df-cco 17203 df-rest 17343 df-topn 17344 df-0g 17362 df-gsum 17363 df-topgen 17364 df-pt 17365 df-prds 17368 df-xrs 17424 df-qtop 17429 df-imas 17430 df-xps 17432 df-mre 17506 df-mrc 17507 df-acs 17509 df-mgm 18566 df-sgrp 18645 df-mnd 18661 df-submnd 18710 df-mulg 19002 df-cntz 19250 df-cmn 19715 df-psmet 21303 df-xmet 21304 df-met 21305 df-bl 21306 df-mopn 21307 df-fbas 21308 df-fg 21309 df-cnfld 21312 df-top 22837 df-topon 22854 df-topsp 22876 df-bases 22889 df-cld 22962 df-ntr 22963 df-cls 22964 df-nei 23041 df-lp 23079 df-perf 23080 df-cn 23170 df-cnp 23171 df-haus 23258 df-tx 23505 df-hmeo 23698 df-fil 23789 df-fm 23881 df-flim 23882 df-flf 23883 df-xms 24263 df-ms 24264 df-tms 24265 df-cncf 24823 df-limc 25811 df-dv 25812

This theorem is referenced by: readvrec 42793

W3C validator