sublevolico

Description: The Lebesgue measure of a left-closed, right-open interval is greater than or equal to the difference of the two bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	sublevolico.a	$⊢ φ \to A \in ℝ$
	sublevolico.b	$⊢ φ \to B \in ℝ$
Assertion	sublevolico	$⊢ φ \to B - A \leq vol ([A, B))$

Proof

Step	Hyp	Ref	Expression
1		sublevolico.a	$⊢ φ \to A \in ℝ$
2		sublevolico.b	$⊢ φ \to B \in ℝ$
3	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
4		eqidd	$⊢ φ \to B - A = B - A$
5	3 4	eqled	$⊢ φ \to B - A \leq B - A$
6	5	adantr	$⊢ (φ \land A < B) \to B - A \leq B - A$
7		volico	$⊢ (A \in ℝ \land B \in ℝ) \to vol ([A, B)) = if (A < B, B - A, 0)$
8	1 2 7	syl2anc	$⊢ φ \to vol ([A, B)) = if (A < B, B - A, 0)$
9	8	adantr	$⊢ (φ \land A < B) \to vol ([A, B)) = if (A < B, B - A, 0)$
10		iftrue	$⊢ A < B \to if (A < B, B - A, 0) = B - A$
11	10	adantl	$⊢ (φ \land A < B) \to if (A < B, B - A, 0) = B - A$
12	9 11	eqtr2d	$⊢ (φ \land A < B) \to B - A = vol ([A, B))$
13	6 12	breqtrd	$⊢ (φ \land A < B) \to B - A \leq vol ([A, B))$
14		simpr	$⊢ (φ \land \neg A < B) \to \neg A < B$
15	2 1	lenltd	$⊢ φ \to (B \leq A \leftrightarrow \neg A < B)$
16	15	adantr	$⊢ (φ \land \neg A < B) \to (B \leq A \leftrightarrow \neg A < B)$
17	14 16	mpbird	$⊢ (φ \land \neg A < B) \to B \leq A$
18	2	adantr	$⊢ (φ \land \neg A < B) \to B \in ℝ$
19	1	adantr	$⊢ (φ \land \neg A < B) \to A \in ℝ$
20	18 19	suble0d	$⊢ (φ \land \neg A < B) \to (B - A \leq 0 \leftrightarrow B \leq A)$
21	17 20	mpbird	$⊢ (φ \land \neg A < B) \to B - A \leq 0$
22	8	adantr	$⊢ (φ \land \neg A < B) \to vol ([A, B)) = if (A < B, B - A, 0)$
23		iffalse	$⊢ \neg A < B \to if (A < B, B - A, 0) = 0$
24	23	adantl	$⊢ (φ \land \neg A < B) \to if (A < B, B - A, 0) = 0$
25	22 24	eqtr2d	$⊢ (φ \land \neg A < B) \to 0 = vol ([A, B))$
26	21 25	breqtrd	$⊢ (φ \land \neg A < B) \to B - A \leq vol ([A, B))$
27	13 26	pm2.61dan	$⊢ φ \to B - A \leq vol ([A, B))$

Metamath Proof Explorer

Theorem sublevolico

Proof