Theorem xrmax2

Description: An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007)

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

Proof

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