Theorem xrmineq

Description: The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015)

	Ref	Expression
Assertion	xrmineq	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge B\le A\right)\to if\left(A\le B,A,B\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		ifid	$$⊢if\left(A\le B,B,B\right)=B$$
2		xrletri3	$$⊢\left(B\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(B=A\leftrightarrow \left(B\le A\wedge A\le B\right)\right)$$
3	2	ancoms	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B=A\leftrightarrow \left(B\le A\wedge A\le B\right)\right)$$
4	3	biimpar	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge \left(B\le A\wedge A\le B\right)\right)\to B=A$$
5	4	anassrs	$$⊢\left(\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge B\le A\right)\wedge A\le B\right)\to B=A$$
6	5	ifeq1da	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge B\le A\right)\to if\left(A\le B,B,B\right)=if\left(A\le B,A,B\right)$$
7	6	3impa	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge B\le A\right)\to if\left(A\le B,B,B\right)=if\left(A\le B,A,B\right)$$
8	1 7	syl5reqr	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge B\le A\right)\to if\left(A\le B,A,B\right)=B$$