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

Proof

Step	Hyp	Ref	Expression
1		xrmin1	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 )
2	1	3adant1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 )
3		simp1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → 𝐴 ∈ ℝ^* )
4		ifcl	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∈ ℝ^* )
5	4	3adant1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∈ ℝ^* )
6		simp2	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → 𝐵 ∈ ℝ^* )
7		xrltletr	⊢ ( ( 𝐴 ∈ ℝ^* ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ( 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 ) → 𝐴 < 𝐵 ) )
8	3 5 6 7	syl3anc	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐵 ) → 𝐴 < 𝐵 ) )
9	2 8	mpan2d	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) → 𝐴 < 𝐵 ) )
10		xrmin2	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 )
11	10	3adant1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 )
12		xrltletr	⊢ ( ( 𝐴 ∈ ℝ^* ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 ) → 𝐴 < 𝐶 ) )
13	5 12	syld3an2	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ≤ 𝐶 ) → 𝐴 < 𝐶 ) )
14	11 13	mpan2d	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) → 𝐴 < 𝐶 ) )
15	9 14	jcad	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) → ( 𝐴 < 𝐵 ∧ 𝐴 < 𝐶 ) ) )
16		breq2	⊢ ( 𝐵 = if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) → ( 𝐴 < 𝐵 ↔ 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ) )
17		breq2	⊢ ( 𝐶 = if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) → ( 𝐴 < 𝐶 ↔ 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ) )
18	16 17	ifboth	⊢ ( ( 𝐴 < 𝐵 ∧ 𝐴 < 𝐶 ) → 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) )
19	15 18	impbid1	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝐴 < if ( 𝐵 ≤ 𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴 < 𝐵 ∧ 𝐴 < 𝐶 ) ) )