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