Theorem ioovolcl

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

	Ref	Expression
Assertion	ioovolcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )

Proof

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