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

Metamath Proof Explorer

Theorem rpge0

Description: A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008)

		Ref	Expression
	Assertion	rpge0	$⊢ A \in ℝ^{+} \to 0 \leq A$

Step	Hyp	Ref	Expression
1		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
2		rpgt0	$⊢ A \in ℝ^{+} \to 0 < A$
3		0re	$⊢ 0 \in ℝ$
4		ltle	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 < A \to 0 \leq A)$
5	3 4	mpan	$⊢ A \in ℝ \to (0 < A \to 0 \leq A)$
6	1 2 5	sylc	$⊢ A \in ℝ^{+} \to 0 \leq A$