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⁡AB∈ℝ

Proof

Step Hyp Ref Expression
1 ioombl ⊢AB∈dom⁡vol
2 mblvol ⊢AB∈dom⁡vol→vol⁡AB=vol*⁡AB
3 1 2 mp1i ⊢A∈ℝ∧B∈ℝ→vol⁡AB=vol*⁡AB
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∈ℝ*→AB=∅↔B≤A
10 7 8 9 syl2an ⊢A∈ℝ∧B∈ℝ→AB=∅↔B≤A
11 10 biimpar ⊢A∈ℝ∧B∈ℝ∧B≤A→AB=∅
12 fveq2 ⊢AB=∅→vol*⁡AB=vol*⁡∅
13 ovol0 ⊢vol*⁡∅=0
14 12 13 eqtrdi ⊢AB=∅→vol*⁡AB=0
15 0re ⊢0∈ℝ
16 14 15 eqeltrdi ⊢AB=∅→vol*⁡AB∈ℝ
17 6 11 16 3syl ⊢A∈ℝ∧B∈ℝ∧B<A→vol*⁡AB∈ℝ
18 ovolioo ⊢A∈ℝ∧B∈ℝ∧A≤B→vol*⁡AB=B−A
19 18 3expa ⊢A∈ℝ∧B∈ℝ∧A≤B→vol*⁡AB=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*⁡AB∈ℝ
24 simpr ⊢A∈ℝ∧B∈ℝ→B∈ℝ
25 simpl ⊢A∈ℝ∧B∈ℝ→A∈ℝ
26 17 23 24 25 ltlecasei ⊢A∈ℝ∧B∈ℝ→vol*⁡AB∈ℝ
27 3 26 eqeltrd ⊢A∈ℝ∧B∈ℝ→vol⁡AB∈ℝ