Theorem lenlt

Description: 'Less than or equal to' expressed in terms of 'less than'. (Contributed by NM, 13-May-1999)

	Ref	Expression
Assertion	lenlt	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
2		rexr	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
3		xrlenlt	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )