**Description:** A nonnegative integer is a complex number. (Contributed by Mario
Carneiro, 27-May-2016)

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

Hypothesis | nn0red.1 | $${\u22a2}{\phi}\to {A}\in {\mathbb{N}}_{0}$$ | |

Assertion | nn0cnd | $${\u22a2}{\phi}\to {A}\in \u2102$$ |

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

1 | nn0red.1 | $${\u22a2}{\phi}\to {A}\in {\mathbb{N}}_{0}$$ | |

2 | 1 | nn0red | $${\u22a2}{\phi}\to {A}\in \mathbb{R}$$ |

3 | 2 | recnd | $${\u22a2}{\phi}\to {A}\in \u2102$$ |