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

Proof

Step	Hyp	Ref	Expression
1		iftrue	$$⊢A\le B\to if\left(A\le B,A,B\right)=A$$
2	1	adantl	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge A\le B\right)\to if\left(A\le B,A,B\right)=A$$
3		xrleid	$$⊢A\in {ℝ}^{*}\to A\le A$$
4	3	ad2antrr	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge A\le B\right)\to A\le A$$
5	2 4	eqbrtrd	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge A\le B\right)\to if\left(A\le B,A,B\right)\le A$$
6		iffalse	$$⊢\neg A\le B\to if\left(A\le B,A,B\right)=B$$
7	6	adantl	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge \neg A\le B\right)\to if\left(A\le B,A,B\right)=B$$
8		xrletri	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\le B\vee B\le A\right)$$
9	8	orcanai	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge \neg A\le B\right)\to B\le A$$
10	7 9	eqbrtrd	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge \neg A\le B\right)\to if\left(A\le B,A,B\right)\le A$$
11	5 10	pm2.61dan	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to if\left(A\le B,A,B\right)\le A$$