Theorem xrltnle

Description: "Less than" expressed in terms of "less than or equal to", for extended reals. (Contributed by NM, 6-Feb-2007)

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

Proof

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