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	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → 𝐵 ≤ if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		xrleid	⊢ ( 𝐵 ∈ ℝ* → 𝐵 ≤ 𝐵 )
2	1	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ≤ 𝐵 )
3		iftrue	⊢ ( 𝐴 ≤ 𝐵 → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = 𝐵 )
4	3	adantl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = 𝐵 )
5	2 4	breqtrrd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ≤ if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) )
6		xrletri	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴 ) )
7	6	orcanai	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → 𝐵 ≤ 𝐴 )
8		iffalse	⊢ ( ¬ 𝐴 ≤ 𝐵 → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = 𝐴 )
9	8	adantl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = 𝐴 )
10	7 9	breqtrrd	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ¬ 𝐴 ≤ 𝐵 ) → 𝐵 ≤ if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) )
11	5 10	pm2.61dan	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → 𝐵 ≤ if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) )