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

Proof

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