Metamath Proof Explorer


Theorem xrltne

Description: 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006)

Ref Expression
Assertion xrltne ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐵𝐴 )

Proof

Step Hyp Ref Expression
1 orc ( 𝐴 < 𝐵 → ( 𝐴 < 𝐵𝐵 < 𝐴 ) )
2 xrltso < Or ℝ*
3 sotrieq ( ( < Or ℝ* ∧ ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴 < 𝐵𝐵 < 𝐴 ) ) )
4 2 3 mpan ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴 < 𝐵𝐵 < 𝐴 ) ) )
5 4 necon2abid ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 < 𝐵𝐵 < 𝐴 ) ↔ 𝐴𝐵 ) )
6 1 5 syl5ib ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵𝐴𝐵 ) )
7 6 3impia ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐴𝐵 )
8 7 necomd ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐵𝐴 )