This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )