# Metamath Proof Explorer

## Theorem ioovolcl

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

Ref Expression
Assertion ioovolcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to vol\left(\left({A},{B}\right)\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 ioombl ${⊢}\left({A},{B}\right)\in \mathrm{dom}vol$
2 mblvol ${⊢}\left({A},{B}\right)\in \mathrm{dom}vol\to vol\left(\left({A},{B}\right)\right)={vol}^{*}\left(\left({A},{B}\right)\right)$
3 1 2 mp1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to vol\left(\left({A},{B}\right)\right)={vol}^{*}\left(\left({A},{B}\right)\right)$
4 ltle ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\right)\to \left({B}<{A}\to {B}\le {A}\right)$
5 4 ancoms ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({B}<{A}\to {B}\le {A}\right)$
6 5 imdistani ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {B}<{A}\right)\to \left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {B}\le {A}\right)$
7 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
8 rexr ${⊢}{B}\in ℝ\to {B}\in {ℝ}^{*}$
9 ioo0 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({A},{B}\right)=\varnothing ↔{B}\le {A}\right)$
10 7 8 9 syl2an ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\left({A},{B}\right)=\varnothing ↔{B}\le {A}\right)$
11 10 biimpar ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {B}\le {A}\right)\to \left({A},{B}\right)=\varnothing$
12 fveq2 ${⊢}\left({A},{B}\right)=\varnothing \to {vol}^{*}\left(\left({A},{B}\right)\right)={vol}^{*}\left(\varnothing \right)$
13 ovol0 ${⊢}{vol}^{*}\left(\varnothing \right)=0$
14 12 13 eqtrdi ${⊢}\left({A},{B}\right)=\varnothing \to {vol}^{*}\left(\left({A},{B}\right)\right)=0$
15 0re ${⊢}0\in ℝ$
16 14 15 eqeltrdi ${⊢}\left({A},{B}\right)=\varnothing \to {vol}^{*}\left(\left({A},{B}\right)\right)\in ℝ$
17 6 11 16 3syl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {B}<{A}\right)\to {vol}^{*}\left(\left({A},{B}\right)\right)\in ℝ$
18 ovolioo ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to {vol}^{*}\left(\left({A},{B}\right)\right)={B}-{A}$
19 18 3expa ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\le {B}\right)\to {vol}^{*}\left(\left({A},{B}\right)\right)={B}-{A}$
20 resubcl ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\right)\to {B}-{A}\in ℝ$
21 20 ancoms ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {B}-{A}\in ℝ$
22 21 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\le {B}\right)\to {B}-{A}\in ℝ$
23 19 22 eqeltrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\le {B}\right)\to {vol}^{*}\left(\left({A},{B}\right)\right)\in ℝ$
24 simpr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {B}\in ℝ$
25 simpl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}\in ℝ$
26 17 23 24 25 ltlecasei ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {vol}^{*}\left(\left({A},{B}\right)\right)\in ℝ$
27 3 26 eqeltrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to vol\left(\left({A},{B}\right)\right)\in ℝ$