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

Metamath Proof Explorer

Theorem xrmaxeq

Description: The maximum of two extended reals is equal to the first if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 xrletri3 
 |-  ( ( B e. RR* /\ A e. RR* ) -> ( B = A <-> ( B <_ A /\ A <_ B ) ) )
2 1 ancoms 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( B = A <-> ( B <_ A /\ A <_ B ) ) )
3 2 biimpar 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( B <_ A /\ A <_ B ) ) -> B = A )
4 3 anassrs 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ B <_ A ) /\ A <_ B ) -> B = A )
5 4 ifeq1da 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ B <_ A ) -> if ( A <_ B , B , A ) = if ( A <_ B , A , A ) )
6 5 3impa 
 |-  ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , B , A ) = if ( A <_ B , A , A ) )
7 ifid 
 |-  if ( A <_ B , A , A ) = A
8 6 7 eqtrdi 
 |-  ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> if ( A <_ B , B , A ) = A )