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

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