voliccico

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

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

Proof

Step	Hyp	Ref	Expression
1		voliccico.1	$⊢ φ \to A \in ℝ$
2		voliccico.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		volicc	$⊢ (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		simpr	$⊢ (φ \land B < A) \to B < A$
39	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
40	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
41		icc0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$
42	39 40 41	syl2anc	$⊢ φ \to ([A, B] = \emptyset \leftrightarrow B < A)$
43	42	adantr	$⊢ (φ \land B < A) \to ([A, B] = \emptyset \leftrightarrow B < A)$
44	38 43	mpbird	$⊢ (φ \land B < A) \to [A, B] = \emptyset$
45	2	adantr	$⊢ (φ \land B < A) \to B \in ℝ$
46	1	adantr	$⊢ (φ \land B < A) \to A \in ℝ$
47	45 46 38	ltled	$⊢ (φ \land B < A) \to B \leq A$
48	46	rexrd	$⊢ (φ \land B < A) \to A \in ℝ^{*}$
49	45	rexrd	$⊢ (φ \land B < A) \to B \in ℝ^{*}$
50		ico0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B) = \emptyset \leftrightarrow B \leq A)$
51	48 49 50	syl2anc	$⊢ (φ \land B < A) \to ([A, B) = \emptyset \leftrightarrow B \leq A)$
52	47 51	mpbird	$⊢ (φ \land B < A) \to [A, B) = \emptyset$
53	44 52	eqtr4d	$⊢ (φ \land B < A) \to [A, B] = [A, B)$
54	53	fveq2d	$⊢ (φ \land B < A) \to vol ([A, B]) = vol ([A, B))$
55	32 37 54	syl2anc	$⊢ (φ \land \neg A \leq B) \to vol ([A, B]) = vol ([A, B))$
56	31 55	pm2.61dan	$⊢ φ \to vol ([A, B]) = vol ([A, B))$

Metamath Proof Explorer

Theorem voliccico

Proof