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

Proof

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