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

Metamath Proof Explorer

Theorem xeqlelt

Description: Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017)

Ref Expression
Assertion xeqlelt ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A = B ↔ A ≤ B ∧ ¬ A < B

Proof

Step Hyp Ref Expression
1 xrletri3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A = B ↔ A ≤ B ∧ B ≤ A
2 xrlenlt ⊢ B ∈ ℝ * ∧ A ∈ ℝ * → B ≤ A ↔ ¬ A < B
3 2 ancoms ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B ≤ A ↔ ¬ A < B
4 3 anbi2d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ∧ B ≤ A ↔ A ≤ B ∧ ¬ A < B
5 1 4 bitrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A = B ↔ A ≤ B ∧ ¬ A < B