This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )