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

Metamath Proof Explorer

Theorem xrmax2

Description: An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007)

Ref Expression
Assertion xrmax2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B ≤ if A ≤ B B A

Proof

Step Hyp Ref Expression
1 xrleid ⊢ B ∈ ℝ * → B ≤ B
2 1 ad2antlr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → B ≤ B
3 iftrue ⊢ A ≤ B → if A ≤ B B A = B
4 3 adantl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → if A ≤ B B A = B
5 2 4 breqtrrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → B ≤ if A ≤ B B A
6 xrletri ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ∨ B ≤ A
7 6 orcanai ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ ¬ A ≤ B → B ≤ A
8 iffalse ⊢ ¬ A ≤ B → if A ≤ B B A = A
9 8 adantl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ ¬ A ≤ B → if A ≤ B B A = A
10 7 9 breqtrrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ ¬ A ≤ B → B ≤ if A ≤ B B A
11 5 10 pm2.61dan ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B ≤ if A ≤ B B A