Theorem xrltletr

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

	Ref	Expression
Assertion	xrltletr	|- ( ( 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		xrlttr	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B < C ) -> A < C ) )
4	3	expcomd	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B < C -> ( A < B -> A < C ) ) )
5		breq2	|- ( B = C -> ( A < B <-> A < C ) )
6	5	biimpd	|- ( B = C -> ( A < B -> A < C ) )
7	6	a1i	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B = C -> ( A < B -> A < C ) ) )
8	4 7	jaod	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( B < C \/ B = C ) -> ( A < B -> A < C ) ) )
9	2 8	sylbid	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B <_ C -> ( A < B -> A < C ) ) )
10	9	impcomd	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B <_ C ) -> A < C ) )