This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrltle

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

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

Step	Hyp	Ref	Expression
1		orc	$⊢ A < B \to (A < B \lor A = B)$
2		xrleloe	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \leftrightarrow (A < B \lor A = B))$
3	1 2	imbitrrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to A \leq B)$