Metamath Proof Explorer
Description: "Less than" expressed in terms of "less than or equal to", for extended
reals. (Contributed by NM, 6Feb2007)


Ref 
Expression 

Assertion 
xrltnle 
⊢ ( ( 𝐴 ∈ ℝ^{*} ∧ 𝐵 ∈ ℝ^{*} ) → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

xrlenlt 
⊢ ( ( 𝐵 ∈ ℝ^{*} ∧ 𝐴 ∈ ℝ^{*} ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) ) 
2 
1

con2bid 
⊢ ( ( 𝐵 ∈ ℝ^{*} ∧ 𝐴 ∈ ℝ^{*} ) → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) ) 
3 
2

ancoms 
⊢ ( ( 𝐴 ∈ ℝ^{*} ∧ 𝐵 ∈ ℝ^{*} ) → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) ) 