Metamath Proof Explorer

Theorem xrmaxlt

Description: Two ways of saying the maximum of two extended reals is less than a third. (Contributed by NM, 7-Feb-2007)

Ref Expression
Assertion xrmaxlt ⊢ 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 xrlelttr ⊢ 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 xrlelttr ⊢ 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