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

Metamath Proof Explorer

Theorem xrleid

Description: 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007)

		Ref	Expression
	Assertion	xrleid	$⊢ A \in ℝ^{*} \to A \leq A$

Step	Hyp	Ref	Expression
1		eqid	$⊢ A = A$
2	1	olci	$⊢ (A < A \lor A = A)$
3		xrleloe	$⊢ (A \in ℝ^{} \land A \in ℝ^{}) \to (A \leq A \leftrightarrow (A < A \lor A = A))$
4	2 3	mpbiri	$⊢ (A \in ℝ^{} \land A \in ℝ^{}) \to A \leq A$
5	4	anidms	$⊢ A \in ℝ^{*} \to A \leq A$