Metamath Proof Explorer

Theorem xrletr

Description: Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006)

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

Proof

Step Hyp Ref Expression
1 xrleloe 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B <_ C <-> ( B < C \/ B = C ) ) )
2 1 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B <_ C <-> ( B < C \/ B = C ) ) )
3 2 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( B <_ C <-> ( B < C \/ B = C ) ) )
4 xrlelttr 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A <_ B /\ B < C ) -> A < C ) )
5 xrltle 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A < C -> A <_ C ) )
6 5 3adant2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A < C -> A <_ C ) )
7 4 6 syld 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A <_ B /\ B < C ) -> A <_ C ) )
8 7 expdimp 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( B < C -> A <_ C ) )
9 breq2 
 |-  ( B = C -> ( A <_ B <-> A <_ C ) )
10 9 biimpcd 
 |-  ( A <_ B -> ( B = C -> A <_ C ) )
11 10 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( B = C -> A <_ C ) )
12 8 11 jaod 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( ( B < C \/ B = C ) -> A <_ C ) )
13 3 12 sylbid 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( B <_ C -> A <_ C ) )
14 13 expimpd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )