Metamath Proof Explorer

Theorem xrmaxle

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

Ref Expression
Assertion xrmaxle ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→ifA≤BBA≤C↔A≤C∧B≤C

Proof

Step Hyp Ref Expression
1 xrmax1 ⊢A∈ℝ*∧B∈ℝ*→A≤ifA≤BBA
2 1 3adant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A≤ifA≤BBA
3 ifcl ⊢B∈ℝ*∧A∈ℝ*→ifA≤BBA∈ℝ*
4 3 ancoms ⊢A∈ℝ*∧B∈ℝ*→ifA≤BBA∈ℝ*
5 4 3adant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→ifA≤BBA∈ℝ*
6 xrletr ⊢A∈ℝ*∧ifA≤BBA∈ℝ*∧C∈ℝ*→A≤ifA≤BBA∧ifA≤BBA≤C→A≤C
7 5 6 syld3an2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→A≤ifA≤BBA∧ifA≤BBA≤C→A≤C
8 2 7 mpand ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→ifA≤BBA≤C→A≤C
9 xrmax2 ⊢A∈ℝ*∧B∈ℝ*→B≤ifA≤BBA
10 9 3adant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→B≤ifA≤BBA
11 simp2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→B∈ℝ*
12 simp3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→C∈ℝ*
13 xrletr ⊢B∈ℝ*∧ifA≤BBA∈ℝ*∧C∈ℝ*→B≤ifA≤BBA∧ifA≤BBA≤C→B≤C
14 11 5 12 13 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→B≤ifA≤BBA∧ifA≤BBA≤C→B≤C
15 10 14 mpand ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→ifA≤BBA≤C→B≤C
16 8 15 jcad ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→ifA≤BBA≤C→A≤C∧B≤C
17 breq1 ⊢B=ifA≤BBA→B≤C↔ifA≤BBA≤C
18 breq1 ⊢A=ifA≤BBA→A≤C↔ifA≤BBA≤C
19 17 18 ifboth ⊢B≤C∧A≤C→ifA≤BBA≤C
20 19 ancoms ⊢A≤C∧B≤C→ifA≤BBA≤C
21 16 20 impbid1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*→ifA≤BBA≤C↔A≤C∧B≤C