Metamath Proof Explorer

Theorem 2resupmax

Description: The supremum of two real numbers is the maximum of these two numbers. (Contributed by AV, 8-Jun-2021)

Ref Expression
Assertion 2resupmax 
|- ( ( A e. RR /\ B e. RR ) -> sup ( { A , B } , RR , < ) = if ( A <_ B , B , A ) )

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 suppr 
 |-  ( ( < Or RR /\ A e. RR /\ B e. RR ) -> sup ( { A , B } , RR , < ) = if ( B < A , A , B ) )
3 1 2 mp3an1 
 |-  ( ( A e. RR /\ B e. RR ) -> sup ( { A , B } , RR , < ) = if ( B < A , A , B ) )
4 ifnot 
 |-  if ( -. B < A , B , A ) = if ( B < A , A , B )
5 lenlt 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
6 5 bicomd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -. B < A <-> A <_ B ) )
7 6 ifbid 
 |-  ( ( A e. RR /\ B e. RR ) -> if ( -. B < A , B , A ) = if ( A <_ B , B , A ) )
8 4 7 eqtr3id 
 |-  ( ( A e. RR /\ B e. RR ) -> if ( B < A , A , B ) = if ( A <_ B , B , A ) )
9 3 8 eqtrd 
 |-  ( ( A e. RR /\ B e. RR ) -> sup ( { A , B } , RR , < ) = if ( A <_ B , B , A ) )