Metamath Proof Explorer

Theorem xrre2

Description: An extended real between two others is real. (Contributed by NM, 6-Feb-2007)

Ref Expression
Assertion xrre2 
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B e. RR )

Proof

Step Hyp Ref Expression
1 mnfle 
 |-  ( A e. RR* -> -oo <_ A )
2 1 adantr 
 |-  ( ( A e. RR* /\ B e. RR* ) -> -oo <_ A )
3 mnfxr 
 |-  -oo e. RR*
4 xrlelttr 
 |-  ( ( -oo e. RR* /\ A e. RR* /\ B e. RR* ) -> ( ( -oo <_ A /\ A < B ) -> -oo < B ) )
5 3 4 mp3an1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( -oo <_ A /\ A < B ) -> -oo < B ) )
6 2 5 mpand 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> -oo < B ) )
7 6 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A < B -> -oo < B ) )
8 pnfge 
 |-  ( C e. RR* -> C <_ +oo )
9 8 adantl 
 |-  ( ( B e. RR* /\ C e. RR* ) -> C <_ +oo )
10 pnfxr 
 |-  +oo e. RR*
11 xrltletr 
 |-  ( ( B e. RR* /\ C e. RR* /\ +oo e. RR* ) -> ( ( B < C /\ C <_ +oo ) -> B < +oo ) )
12 10 11 mp3an3 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( ( B < C /\ C <_ +oo ) -> B < +oo ) )
13 9 12 mpan2d 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B < C -> B < +oo ) )
14 13 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B < C -> B < +oo ) )
15 7 14 anim12d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B < C ) -> ( -oo < B /\ B < +oo ) ) )
16 xrrebnd 
 |-  ( B e. RR* -> ( B e. RR <-> ( -oo < B /\ B < +oo ) ) )
17 16 3ad2ant2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B e. RR <-> ( -oo < B /\ B < +oo ) ) )
18 15 17 sylibrd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B < C ) -> B e. RR ) )
19 18 imp 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B e. RR )