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 )