# 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 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to if\left({A}\le {B},{A},{B}\right)\le {B}$

### Proof

Step Hyp Ref Expression
1 xrleid ${⊢}{B}\in {ℝ}^{*}\to {B}\le {B}$
2 iffalse ${⊢}¬{A}\le {B}\to if\left({A}\le {B},{A},{B}\right)={B}$
3 2 breq1d ${⊢}¬{A}\le {B}\to \left(if\left({A}\le {B},{A},{B}\right)\le {B}↔{B}\le {B}\right)$
4 1 3 syl5ibrcom ${⊢}{B}\in {ℝ}^{*}\to \left(¬{A}\le {B}\to if\left({A}\le {B},{A},{B}\right)\le {B}\right)$
5 iftrue ${⊢}{A}\le {B}\to if\left({A}\le {B},{A},{B}\right)={A}$
6 id ${⊢}{A}\le {B}\to {A}\le {B}$
7 5 6 eqbrtrd ${⊢}{A}\le {B}\to if\left({A}\le {B},{A},{B}\right)\le {B}$
8 4 7 pm2.61d2 ${⊢}{B}\in {ℝ}^{*}\to if\left({A}\le {B},{A},{B}\right)\le {B}$
9 8 adantl ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to if\left({A}\le {B},{A},{B}\right)\le {B}$