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 B sup A B < = if A B B A

Proof

Step Hyp Ref Expression
1 ltso < Or
2 suppr < Or A B sup A B < = if B < A A B
3 1 2 mp3an1 A B sup A B < = if B < A A B
4 ifnot if ¬ B < A B A = if B < A A B
5 lenlt A B A B ¬ B < A
6 5 bicomd A B ¬ B < A A B
7 6 ifbid A B if ¬ B < A B A = if A B B A
8 4 7 eqtr3id A B if B < A A B = if A B B A
9 3 8 eqtrd A B sup A B < = if A B B A