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

Metamath Proof Explorer

Theorem xrmaxlt

Proof