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	imbitrid	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → 𝐴 ≠ 𝐵 ) )
7	6	3impia	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐴 ≠ 𝐵 )
8	7	necomd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → 𝐵 ≠ 𝐴 )