Metamath Proof Explorer

Theorem ioovolcl

Description: An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Assertion ioovolcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → vol ⁡ A B ∈ ℝ

Proof

Step Hyp Ref Expression
1 ioombl ⊢ A B ∈ dom ⁡ vol
2 mblvol ⊢ A B ∈ dom ⁡ vol → vol ⁡ A B = vol * ⁡ A B
3 1 2 mp1i ⊢ A ∈ ℝ ∧ B ∈ ℝ → vol ⁡ A B = vol * ⁡ A B
4 ltle ⊢ B ∈ ℝ ∧ A ∈ ℝ → B < A → B ≤ A
5 4 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B < A → B ≤ A
6 5 imdistani ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B < A → A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A
7 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
8 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
9 ioo0 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A B = ∅ ↔ B ≤ A
10 7 8 9 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B = ∅ ↔ B ≤ A
11 10 biimpar ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A → A B = ∅
12 fveq2 ⊢ A B = ∅ → vol * ⁡ A B = vol * ⁡ ∅
13 ovol0 ⊢ vol * ⁡ ∅ = 0
14 12 13 eqtrdi ⊢ A B = ∅ → vol * ⁡ A B = 0
15 0re ⊢ 0 ∈ ℝ
16 14 15 eqeltrdi ⊢ A B = ∅ → vol * ⁡ A B ∈ ℝ
17 6 11 16 3syl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B < A → vol * ⁡ A B ∈ ℝ
18 ovolioo ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → vol * ⁡ A B = B − A
19 18 3expa ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → vol * ⁡ A B = B − A
20 resubcl ⊢ B ∈ ℝ ∧ A ∈ ℝ → B − A ∈ ℝ
21 20 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A ∈ ℝ
22 21 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B − A ∈ ℝ
23 19 22 eqeltrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → vol * ⁡ A B ∈ ℝ
24 simpr ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ∈ ℝ
25 simpl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℝ
26 17 23 24 25 ltlecasei ⊢ A ∈ ℝ ∧ B ∈ ℝ → vol * ⁡ A B ∈ ℝ
27 3 26 eqeltrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → vol ⁡ A B ∈ ℝ