voliooico

Description: An open interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	voliooico.1	$⊢ φ \to A \in ℝ$
	voliooico.2	$⊢ φ \to B \in ℝ$
Assertion	voliooico	$⊢ φ \to vol ((A, B)) = vol ([A, B))$

Proof

Step	Hyp	Ref	Expression
1		voliooico.1	$⊢ φ \to A \in ℝ$
2		voliooico.2	$⊢ φ \to B \in ℝ$
3		iftrue	$⊢ A < B \to if (A < B, B - A, 0) = B - A$
4	3	adantl	$⊢ ((φ \land A \leq B) \land A < B) \to if (A < B, B - A, 0) = B - A$
5	2	recnd	$⊢ φ \to B \in ℂ$
6	5	subidd	$⊢ φ \to B - B = 0$
7	6	eqcomd	$⊢ φ \to 0 = B - B$
8	7	ad2antrr	$⊢ ((φ \land A \leq B) \land \neg A < B) \to 0 = B - B$
9		iffalse	$⊢ \neg A < B \to if (A < B, B - A, 0) = 0$
10	9	adantl	$⊢ ((φ \land A \leq B) \land \neg A < B) \to if (A < B, B - A, 0) = 0$
11		simpll	$⊢ ((φ \land A \leq B) \land \neg A < B) \to φ$
12	11 1	syl	$⊢ ((φ \land A \leq B) \land \neg A < B) \to A \in ℝ$
13	11 2	syl	$⊢ ((φ \land A \leq B) \land \neg A < B) \to B \in ℝ$
14		simpr	$⊢ (φ \land A \leq B) \to A \leq B$
15	14	adantr	$⊢ ((φ \land A \leq B) \land \neg A < B) \to A \leq B$
16		simpr	$⊢ ((φ \land A \leq B) \land \neg A < B) \to \neg A < B$
17	12 13 15 16	lenlteq	$⊢ ((φ \land A \leq B) \land \neg A < B) \to A = B$
18		oveq2	$⊢ A = B \to B - A = B - B$
19	18	adantl	$⊢ (φ \land A = B) \to B - A = B - B$
20	11 17 19	syl2anc	$⊢ ((φ \land A \leq B) \land \neg A < B) \to B - A = B - B$
21	8 10 20	3eqtr4d	$⊢ ((φ \land A \leq B) \land \neg A < B) \to if (A < B, B - A, 0) = B - A$
22	4 21	pm2.61dan	$⊢ (φ \land A \leq B) \to if (A < B, B - A, 0) = B - A$
23	22	eqcomd	$⊢ (φ \land A \leq B) \to B - A = if (A < B, B - A, 0)$
24	1	adantr	$⊢ (φ \land A \leq B) \to A \in ℝ$
25	2	adantr	$⊢ (φ \land A \leq B) \to B \in ℝ$
26		volioo	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to vol ((A, B)) = B - A$
27	24 25 14 26	syl3anc	$⊢ (φ \land A \leq B) \to vol ((A, B)) = B - A$
28		volico	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) = if (A < B, B - A, 0)$
29	1 2 28	syl2anc	$⊢ φ \to vol ([A, B)) = if (A < B, B - A, 0)$
30	29	adantr	$⊢ (φ \land A \leq B) \to vol ([A, B)) = if (A < B, B - A, 0)$
31	23 27 30	3eqtr4d	$⊢ (φ \land A \leq B) \to vol ((A, B)) = vol ([A, B))$
32		simpl	$⊢ (φ \land \neg A \leq B) \to φ$
33		simpr	$⊢ (φ \land \neg A \leq B) \to \neg A \leq B$
34	32 2	syl	$⊢ (φ \land \neg A \leq B) \to B \in ℝ$
35	32 1	syl	$⊢ (φ \land \neg A \leq B) \to A \in ℝ$
36	34 35	ltnled	$⊢ (φ \land \neg A \leq B) \to (B < A \leftrightarrow \neg A \leq B)$
37	33 36	mpbird	$⊢ (φ \land \neg A \leq B) \to B < A$
38	2	adantr	$⊢ (φ \land B < A) \to B \in ℝ$
39	1	adantr	$⊢ (φ \land B < A) \to A \in ℝ$
40		simpr	$⊢ (φ \land B < A) \to B < A$
41	38 39 40	ltled	$⊢ (φ \land B < A) \to B \leq A$
42	39	rexrd	$⊢ (φ \land B < A) \to A \in ℝ^{*}$
43	38	rexrd	$⊢ (φ \land B < A) \to B \in ℝ^{*}$
44		ioo0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) = \emptyset \leftrightarrow B \leq A)$
45	42 43 44	syl2anc	$⊢ (φ \land B < A) \to ((A, B) = \emptyset \leftrightarrow B \leq A)$
46	41 45	mpbird	$⊢ (φ \land B < A) \to (A, B) = \emptyset$
47		ico0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B) = \emptyset \leftrightarrow B \leq A)$
48	42 43 47	syl2anc	$⊢ (φ \land B < A) \to ([A, B) = \emptyset \leftrightarrow B \leq A)$
49	41 48	mpbird	$⊢ (φ \land B < A) \to [A, B) = \emptyset$
50	46 49	eqtr4d	$⊢ (φ \land B < A) \to (A, B) = [A, B)$
51	50	fveq2d	$⊢ (φ \land B < A) \to vol ((A, B)) = vol ([A, B))$
52	32 37 51	syl2anc	$⊢ (φ \land \neg A \leq B) \to vol ((A, B)) = vol ([A, B))$
53	31 52	pm2.61dan	$⊢ φ \to vol ((A, B)) = vol ([A, B))$

Metamath Proof Explorer

Theorem voliooico

Proof