Theorem xrmin2

Description: The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007)

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

Proof

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