Theorem xrmax1

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	xrmax1	|- ( ( A e. RR* /\ B e. RR* ) -> A <_ if ( A <_ B , B , A ) )

Proof

Step	Hyp	Ref	Expression
1		xrleid	|- ( A e. RR* -> A <_ A )
2		iffalse	|- ( -. A <_ B -> if ( A <_ B , B , A ) = A )
3	2	breq2d	|- ( -. A <_ B -> ( A <_ if ( A <_ B , B , A ) <-> A <_ A ) )
4	1 3	syl5ibrcom	|- ( A e. RR* -> ( -. A <_ B -> A <_ if ( A <_ B , B , A ) ) )
5		id	|- ( A <_ B -> A <_ B )
6		iftrue	|- ( A <_ B -> if ( A <_ B , B , A ) = B )
7	5 6	breqtrrd	|- ( A <_ B -> A <_ if ( A <_ B , B , A ) )
8	4 7	pm2.61d2	|- ( A e. RR* -> A <_ if ( A <_ B , B , A ) )
9	8	adantr	|- ( ( A e. RR* /\ B e. RR* ) -> A <_ if ( A <_ B , B , A ) )