This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lenlt

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

Ref Expression
Assertion lenlt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ ¬ B < A

Proof

Step Hyp Ref Expression
1 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
2 rexr ⊢ B ∈ ℝ → B ∈ ℝ *
3 xrlenlt ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ ¬ B < A
4 1 2 3 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ ¬ B < A