Metamath Proof Explorer

Theorem xrre

Description: A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006)

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

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( -oo < A /\ A <_ B ) ) -> -oo < A )
2 ltpnf 
 |-  ( B e. RR -> B < +oo )
3 2 adantl 
 |-  ( ( A e. RR* /\ B e. RR ) -> B < +oo )
4 rexr 
 |-  ( B e. RR -> B e. RR* )
5 pnfxr 
 |-  +oo e. RR*
6 xrlelttr 
 |-  ( ( A e. RR* /\ B e. RR* /\ +oo e. RR* ) -> ( ( A <_ B /\ B < +oo ) -> A < +oo ) )
7 5 6 mp3an3 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A <_ B /\ B < +oo ) -> A < +oo ) )
8 4 7 sylan2 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( A <_ B /\ B < +oo ) -> A < +oo ) )
9 3 8 mpan2d 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A <_ B -> A < +oo ) )
10 9 imp 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ A <_ B ) -> A < +oo )
11 10 adantrl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( -oo < A /\ A <_ B ) ) -> A < +oo )
12 xrrebnd 
 |-  ( A e. RR* -> ( A e. RR <-> ( -oo < A /\ A < +oo ) ) )
13 12 ad2antrr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( -oo < A /\ A <_ B ) ) -> ( A e. RR <-> ( -oo < A /\ A < +oo ) ) )
14 1 11 13 mpbir2and 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( -oo < A /\ A <_ B ) ) -> A e. RR )