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

Metamath Proof Explorer

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 ) )