Metamath Proof Explorer

Theorem volicorege0

Description: The Lebesgue measure of a left-closed right-open interval with real bounds, is a nonnegative real number. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Assertion volicorege0 
|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) e. ( 0 [,) +oo ) )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( ( A e. RR /\ B e. RR ) -> 0 e. RR )
2 1 rexrd 
 |-  ( ( A e. RR /\ B e. RR ) -> 0 e. RR* )
3 pnfxr 
 |-  +oo e. RR*
4 3 a1i 
 |-  ( ( A e. RR /\ B e. RR ) -> +oo e. RR* )
5 volicore 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) e. RR )
6 5 rexrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) e. RR* )
7 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
8 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
9 8 rexrd 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR* )
10 icombl 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) e. dom vol )
11 7 9 10 syl2anc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,) B ) e. dom vol )
12 volge0 
 |-  ( ( A [,) B ) e. dom vol -> 0 <_ ( vol ` ( A [,) B ) ) )
13 11 12 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> 0 <_ ( vol ` ( A [,) B ) ) )
14 5 ltpnfd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) < +oo )
15 2 4 6 13 14 elicod 
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) e. ( 0 [,) +oo ) )