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 ( 𝐴𝐵 , 𝐴 , 𝐵 ) ≤ 𝐴 )