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

Metamath Proof Explorer

Theorem xrmin1

Description: The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007)

Ref Expression
Assertion xrmin1 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → if ( 𝐴 ≤ 𝐵 , 𝐴 , 𝐵 ) ≤ 𝐴 )

Proof

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