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 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A≤ifB≤CBC↔A≤B∧A≤C

Proof

Step Hyp Ref Expression
1 xrmin1 ⊢B∈ℝ*∧C∈ℝ*→ifB≤CBC≤B
2 1 3adant1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→ifB≤CBC≤B
3 simp1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A∈ℝ*
4 ifcl ⊢B∈ℝ*∧C∈ℝ*→ifB≤CBC∈ℝ*
5 4 3adant1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→ifB≤CBC∈ℝ*
6 simp2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→B∈ℝ*
7 xrletr ⊢A∈ℝ*∧ifB≤CBC∈ℝ*∧B∈ℝ*→A≤ifB≤CBC∧ifB≤CBC≤B→A≤B
8 3 5 6 7 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A≤ifB≤CBC∧ifB≤CBC≤B→A≤B
9 2 8 mpan2d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A≤ifB≤CBC→A≤B
10 xrmin2 ⊢B∈ℝ*∧C∈ℝ*→ifB≤CBC≤C
11 10 3adant1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→ifB≤CBC≤C
12 xrletr ⊢A∈ℝ*∧ifB≤CBC∈ℝ*∧C∈ℝ*→A≤ifB≤CBC∧ifB≤CBC≤C→A≤C
13 5 12 syld3an2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A≤ifB≤CBC∧ifB≤CBC≤C→A≤C
14 11 13 mpan2d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A≤ifB≤CBC→A≤C
15 9 14 jcad ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A≤ifB≤CBC→A≤B∧A≤C
16 breq2 ⊢B=ifB≤CBC→A≤B↔A≤ifB≤CBC
17 breq2 ⊢C=ifB≤CBC→A≤C↔A≤ifB≤CBC
18 16 17 ifboth ⊢A≤B∧A≤C→A≤ifB≤CBC
19 15 18 impbid1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A≤ifB≤CBC↔A≤B∧A≤C