Metamath Proof Explorer

Theorem xrre3

Description: A way of proving that an extended real is real. (Contributed by FL, 29-May-2014)

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

Proof

Step Hyp Ref Expression
1 mnflt 
 |-  ( B e. RR -> -oo < B )
2 1 adantl 
 |-  ( ( A e. RR* /\ B e. RR ) -> -oo < B )
3 mnfxr 
 |-  -oo e. RR*
4 rexr 
 |-  ( B e. RR -> B e. RR* )
5 4 adantl 
 |-  ( ( A e. RR* /\ B e. RR ) -> B e. RR* )
6 simpl 
 |-  ( ( A e. RR* /\ B e. RR ) -> A e. RR* )
7 xrltletr 
 |-  ( ( -oo e. RR* /\ B e. RR* /\ A e. RR* ) -> ( ( -oo < B /\ B <_ A ) -> -oo < A ) )
8 3 5 6 7 mp3an2i 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( -oo < B /\ B <_ A ) -> -oo < A ) )
9 2 8 mpand 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( B <_ A -> -oo < A ) )
10 9 imp 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ B <_ A ) -> -oo < A )
11 10 adantrr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( B <_ A /\ A < +oo ) ) -> -oo < A )
12 simprr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( B <_ A /\ A < +oo ) ) -> A < +oo )
13 xrrebnd 
 |-  ( A e. RR* -> ( A e. RR <-> ( -oo < A /\ A < +oo ) ) )
14 13 ad2antrr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( B <_ A /\ A < +oo ) ) -> ( A e. RR <-> ( -oo < A /\ A < +oo ) ) )
15 11 12 14 mpbir2and 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( B <_ A /\ A < +oo ) ) -> A e. RR )