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	$$⊢\neg A\le B\to if\left(A\le B,A,B\right)=B$$
3	2	breq1d	$$⊢\neg A\le B\to \left(if\left(A\le B,A,B\right)\le B\leftrightarrow B\le B\right)$$
4	1 3	syl5ibrcom	$$⊢B\in {ℝ}^{*}\to \left(\neg 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$$