Theorem xrmax2

Description: An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007)

	Ref	Expression
Assertion	xrmax2	|- ( ( A e. RR* /\ B e. RR* ) -> B <_ if ( A <_ B , B , A ) )

Proof

Step	Hyp	Ref	Expression
1		xrleid	|- ( B e. RR* -> B <_ B )
2	1	ad2antlr	|- ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> B <_ B )
3		iftrue	|- ( A <_ B -> if ( A <_ B , B , A ) = B )
4	3	adantl	|- ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> if ( A <_ B , B , A ) = B )
5	2 4	breqtrrd	|- ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> B <_ if ( A <_ B , B , A ) )
6		xrletri	|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B \/ B <_ A ) )
7	6	orcanai	|- ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> B <_ A )
8		iffalse	|- ( -. A <_ B -> if ( A <_ B , B , A ) = A )
9	8	adantl	|- ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> if ( A <_ B , B , A ) = A )
10	7 9	breqtrrd	|- ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> B <_ if ( A <_ B , B , A ) )
11	5 10	pm2.61dan	|- ( ( A e. RR* /\ B e. RR* ) -> B <_ if ( A <_ B , B , A ) )