Metamath Proof Explorer

Theorem xrrege0

Description: A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xrrege0 
|- ( ( ( A e. RR* /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> A e. RR )

Proof

Step Hyp Ref Expression
1 ge0gtmnf 
 |-  ( ( A e. RR* /\ 0 <_ A ) -> -oo < A )
2 1 ad2ant2r 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> -oo < A )
3 simprr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> A <_ B )
4 2 3 jca 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> ( -oo < A /\ A <_ B ) )
5 xrre 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( -oo < A /\ A <_ B ) ) -> A e. RR )
6 4 5 syldan 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> A e. RR )