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 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → 𝐵 ≤ if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) )

Proof

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