Metamath Proof Explorer


Theorem xrlemin

Description: Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion xrlemin ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴𝐵𝐴𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 xrmin1 ( ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 )
2 1 3adant1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 )
3 simp1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → 𝐴 ∈ ℝ* )
4 ifcl ( ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ∈ ℝ* )
5 4 3adant1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ∈ ℝ* )
6 simp2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → 𝐵 ∈ ℝ* )
7 xrletr ( ( 𝐴 ∈ ℝ* ∧ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 ) → 𝐴𝐵 ) )
8 3 5 6 7 syl3anc ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( ( 𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 ) → 𝐴𝐵 ) )
9 2 8 mpan2d ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) → 𝐴𝐵 ) )
10 xrmin2 ( ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 )
11 10 3adant1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 )
12 xrletr ( ( 𝐴 ∈ ℝ* ∧ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ∈ ℝ*𝐶 ∈ ℝ* ) → ( ( 𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 ) → 𝐴𝐶 ) )
13 5 12 syld3an2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( ( 𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 ) → 𝐴𝐶 ) )
14 11 13 mpan2d ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) → 𝐴𝐶 ) )
15 9 14 jcad ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) → ( 𝐴𝐵𝐴𝐶 ) ) )
16 breq2 ( 𝐵 = if ( 𝐵𝐶 , 𝐵 , 𝐶 ) → ( 𝐴𝐵𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ) )
17 breq2 ( 𝐶 = if ( 𝐵𝐶 , 𝐵 , 𝐶 ) → ( 𝐴𝐶𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ) )
18 16 17 ifboth ( ( 𝐴𝐵𝐴𝐶 ) → 𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) )
19 15 18 impbid1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐴 ≤ if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴𝐵𝐴𝐶 ) ) )