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

Metamath Proof Explorer

Theorem nn0rp0

Description: A nonnegative integer is a nonnegative real number. (Contributed by AV, 24-May-2020)

		Ref	Expression
	Assertion	nn0rp0	$⊢ N \in ℕ_{0} \to N \in [0, +∞)$

Step	Hyp	Ref	Expression
1		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
2		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
3		elrege0	$⊢ N \in [0, +∞) \leftrightarrow (N \in ℝ \land 0 \leq N)$
4	1 2 3	sylanbrc	$⊢ N \in ℕ_{0} \to N \in [0, +∞)$