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

Proof

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