xrltne

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

		Ref	Expression
	Assertion	xrltne	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to B \neq A$

Step	Hyp	Ref	Expression
1		orc	$⊢ A < B \to (A < B \lor B < A)$
2		xrltso	$⊢ < Or ℝ^{*}$
3		sotrieq	$⊢ (< Or ℝ^{} \land (A \in ℝ^{} \land B \in ℝ^{*})) \to (A = B \leftrightarrow \neg (A < B \lor B < A))$
4	2 3	mpan	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A = B \leftrightarrow \neg (A < B \lor B < A))$
5	4	necon2abid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A < B \lor B < A) \leftrightarrow A \neq B)$
6	1 5	imbitrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to A \neq B)$
7	6	3impia	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to A \neq B$
8	7	necomd	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to B \neq A$

Metamath Proof Explorer