Theorem iccvolcl

Description: A closed real interval has finite volume. (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Assertion	iccvolcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ )

Proof

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