Theorem xrmin1

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

Proof

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