Theorem nn0cni 9108

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

Hypothesis

Ref	Expression
nn0re.1	|- A e. NN0

Assertion

Ref	Expression
nn0cni	|- A e. CC

Proof of Theorem nn0cni

Step	Hyp	Ref	Expression
1		nn0re.1	. . 3 |- A e. NN0
2	1	nn0rei 9107	. 2 |- A e. RR
3	2	recni 7893	1 |- A e. CC

Syntax hints:   e. wcel 2128   CCcc 7733   NN0cn0 9096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-sep 4085  ax-cnex 7826  ax-resscn 7827  ax-1re 7829  ax-addrcl 7832  ax-rnegex 7844

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-sn 3567  df-int 3810  df-inn 8840  df-n0 9097

This theorem is referenced by:  nn0le2xi  9146  num0u  9311  num0h  9312  numsuc  9314  numsucc  9340  numma  9344  nummac  9345  numma2c  9346  numadd  9347  numaddc  9348  nummul1c  9349  nummul2c  9350  decrmanc  9357  decrmac  9358  decaddi  9360  decaddci  9361  decsubi  9363  decmul1  9364  decmulnc  9367  11multnc  9368  decmul10add  9369  6p5lem  9370  4t3lem  9397  7t3e21  9410  7t6e42  9413  8t3e24  9416  8t4e32  9417  8t8e64  9421  9t3e27  9423  9t4e36  9424  9t5e45  9425  9t6e54  9426  9t7e63  9427  9t11e99  9430  decbin0  9440  decbin2  9441  sq10  10598  3dec  10600  3dvdsdec  11769  3dvds2dec  11770  3lcm2e6  12051