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 
|- ( ( A C_ RR /\ B e. RR /\ ( vol* ` A ) <_ B ) -> ( vol* ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 ovolcl 
 |-  ( A C_ RR -> ( vol* ` A ) e. RR* )
2 1 3ad2ant1 
 |-  ( ( A C_ RR /\ B e. RR /\ ( vol* ` A ) <_ B ) -> ( vol* ` A ) e. RR* )
3 simp2 
 |-  ( ( A C_ RR /\ B e. RR /\ ( vol* ` A ) <_ B ) -> B e. RR )
4 ovolge0 
 |-  ( A C_ RR -> 0 <_ ( vol* ` A ) )
5 4 3ad2ant1 
 |-  ( ( A C_ RR /\ B e. RR /\ ( vol* ` A ) <_ B ) -> 0 <_ ( vol* ` A ) )
6 simp3 
 |-  ( ( A C_ RR /\ B e. RR /\ ( vol* ` A ) <_ B ) -> ( vol* ` A ) <_ B )
7 xrrege0 
 |-  ( ( ( ( vol* ` A ) e. RR* /\ B e. RR ) /\ ( 0 <_ ( vol* ` A ) /\ ( vol* ` A ) <_ B ) ) -> ( vol* ` A ) e. RR )
8 2 3 5 6 7 syl22anc 
 |-  ( ( A C_ RR /\ B e. RR /\ ( vol* ` A ) <_ B ) -> ( vol* ` A ) e. RR )