Metamath Proof Explorer


Theorem nn0rei

Description: A nonnegative integer is a real number. (Contributed by NM, 14-May-2003)

Ref Expression
Hypothesis nn0rei.1 A 0
Assertion nn0rei A

Proof

Step Hyp Ref Expression
1 nn0rei.1 A 0
2 nn0ssre 0
3 2 1 sselii A