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 ≤ if B ≤ C B C ↔ A ≤ B ∧ A ≤ C

Proof

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