Metamath Proof Explorer


Theorem xrmin2

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

Proof

Step Hyp Ref Expression
1 xrleid ( 𝐵 ∈ ℝ*𝐵𝐵 )
2 iffalse ( ¬ 𝐴𝐵 → if ( 𝐴𝐵 , 𝐴 , 𝐵 ) = 𝐵 )
3 2 breq1d ( ¬ 𝐴𝐵 → ( if ( 𝐴𝐵 , 𝐴 , 𝐵 ) ≤ 𝐵𝐵𝐵 ) )
4 1 3 syl5ibrcom ( 𝐵 ∈ ℝ* → ( ¬ 𝐴𝐵 → if ( 𝐴𝐵 , 𝐴 , 𝐵 ) ≤ 𝐵 ) )
5 iftrue ( 𝐴𝐵 → if ( 𝐴𝐵 , 𝐴 , 𝐵 ) = 𝐴 )
6 id ( 𝐴𝐵𝐴𝐵 )
7 5 6 eqbrtrd ( 𝐴𝐵 → if ( 𝐴𝐵 , 𝐴 , 𝐵 ) ≤ 𝐵 )
8 4 7 pm2.61d2 ( 𝐵 ∈ ℝ* → if ( 𝐴𝐵 , 𝐴 , 𝐵 ) ≤ 𝐵 )
9 8 adantl ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → if ( 𝐴𝐵 , 𝐴 , 𝐵 ) ≤ 𝐵 )