Theorem xrmaxeq

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

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

Proof

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