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

Metamath Proof Explorer

Theorem ovollecl

Description: If an outer volume is bounded above, then it is real. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion ovollecl ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → ( vol* ‘ 𝐴 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 ovolcl ⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) ∈ ℝ* )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → ( vol* ‘ 𝐴 ) ∈ ℝ* )
3 simp2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → 𝐵 ∈ ℝ )
4 ovolge0 ⊢ ( 𝐴 ⊆ ℝ → 0 ≤ ( vol* ‘ 𝐴 ) )
5 4 3ad2ant1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → 0 ≤ ( vol* ‘ 𝐴 ) )
6 simp3 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → ( vol* ‘ 𝐴 ) ≤ 𝐵 )
7 xrrege0 ⊢ ( ( ( ( vol* ‘ 𝐴 ) ∈ ℝ* ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ ( vol* ‘ 𝐴 ) ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
8 2 3 5 6 7 syl22anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( vol* ‘ 𝐴 ) ≤ 𝐵 ) → ( vol* ‘ 𝐴 ) ∈ ℝ )