Metamath Proof Explorer

Theorem 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 ⊢ φ → A ∈ ℝ
sublevolico.b ⊢ φ → B ∈ ℝ
Assertion sublevolico ⊢ φ → B − A ≤ vol ⁡ A B

Proof

Step Hyp Ref Expression
1 sublevolico.a ⊢ φ → A ∈ ℝ
2 sublevolico.b ⊢ φ → B ∈ ℝ
3 2 1 resubcld ⊢ φ → B − A ∈ ℝ
4 eqidd ⊢ φ → B − A = B − A
5 3 4 eqled ⊢ φ → B − A ≤ B − A
6 5 adantr ⊢ φ ∧ A < B → B − A ≤ B − A
7 volico ⊢ A ∈ ℝ ∧ B ∈ ℝ → vol ⁡ A B = if A < B B − A 0
8 1 2 7 syl2anc ⊢ φ → vol ⁡ A B = if A < B B − A 0
9 8 adantr ⊢ φ ∧ A < B → vol ⁡ A B = if A < B B − A 0
10 iftrue ⊢ A < B → if A < B B − A 0 = B − A
11 10 adantl ⊢ φ ∧ A < B → if A < B B − A 0 = B − A
12 9 11 eqtr2d ⊢ φ ∧ A < B → B − A = vol ⁡ A B
13 6 12 breqtrd ⊢ φ ∧ A < B → B − A ≤ vol ⁡ A B
14 simpr ⊢ φ ∧ ¬ A < B → ¬ A < B
15 2 1 lenltd ⊢ φ → B ≤ A ↔ ¬ A < B
16 15 adantr ⊢ φ ∧ ¬ A < B → B ≤ A ↔ ¬ A < B
17 14 16 mpbird ⊢ φ ∧ ¬ A < B → B ≤ A
18 2 adantr ⊢ φ ∧ ¬ A < B → B ∈ ℝ
19 1 adantr ⊢ φ ∧ ¬ A < B → A ∈ ℝ
20 18 19 suble0d ⊢ φ ∧ ¬ A < B → B − A ≤ 0 ↔ B ≤ A
21 17 20 mpbird ⊢ φ ∧ ¬ A < B → B − A ≤ 0
22 8 adantr ⊢ φ ∧ ¬ A < B → vol ⁡ A B = if A < B B − A 0
23 iffalse ⊢ ¬ A < B → if A < B B − A 0 = 0
24 23 adantl ⊢ φ ∧ ¬ A < B → if A < B B − A 0 = 0
25 22 24 eqtr2d ⊢ φ ∧ ¬ A < B → 0 = vol ⁡ A B
26 21 25 breqtrd ⊢ φ ∧ ¬ A < B → B − A ≤ vol ⁡ A B
27 13 26 pm2.61dan ⊢ φ → B − A ≤ vol ⁡ A B