Metamath Proof Explorer

Theorem xrltmin

Description: Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007)

Ref Expression
Assertion xrltmin ⊢ 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 xrltletr ⊢ 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 xrltletr ⊢ 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