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

Ref | Expression | ||
---|---|---|---|

Hypothesis | nn0rei.1 | $${\u22a2}{A}\in {\mathbb{N}}_{0}$$ | |

Assertion | nn0rei | $${\u22a2}{A}\in \mathbb{R}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | nn0rei.1 | $${\u22a2}{A}\in {\mathbb{N}}_{0}$$ | |

2 | nn0ssre | $${\u22a2}{\mathbb{N}}_{0}\subseteq \mathbb{R}$$ | |

3 | 2 1 | sselii | $${\u22a2}{A}\in \mathbb{R}$$ |