Metamath Proof Explorer


Theorem ltmin

Description: Two ways of saying a number is less than the minimum of two others. (Contributed by NM, 1-Sep-2006)

Ref Expression
Assertion ltmin ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴 < 𝐵𝐴 < 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 rexr ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
2 rexr ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
3 rexr ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ* )
4 xrltmin ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐴 < if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴 < 𝐵𝐴 < 𝐶 ) ) )
5 1 2 3 4 syl3an ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < if ( 𝐵𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴 < 𝐵𝐴 < 𝐶 ) ) )