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	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ ¬ 𝐴 < 𝐵 ) ) )

Proof

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