Theorem nn0cni 9554

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 9553	. 2 |- A e. RR
3	2	recni 8328	1 |- A e. CC

Syntax hints:   e. wcel 2209   CCcc 8167   NN0cn0 9542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4244  ax-cnex 8260  ax-resscn 8261  ax-1re 8263  ax-addrcl 8266  ax-rnegex 8278

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3711  df-int 3966  df-inn 9284  df-n0 9543

This theorem is referenced by:  nn0le2xi  9592  num0u  9766  num0h  9767  numsuc  9769  numsucc  9795  numma  9799  nummac  9800  numma2c  9801  numadd  9802  numaddc  9803  nummul1c  9804  nummul2c  9805  decrmanc  9812  decrmac  9813  decaddi  9815  decaddci  9816  decsubi  9818  decmul1  9819  decmulnc  9822  11multnc  9823  decmul10add  9824  6p5lem  9825  4t3lem  9852  7t3e21  9865  7t6e42  9868  8t3e24  9871  8t4e32  9872  8t8e64  9876  9t3e27  9878  9t4e36  9879  9t5e45  9880  9t6e54  9881  9t7e63  9882  9t11e99  9885  decbin0  9895  decbin2  9896  sq10  11128  3dec  11130  cats1fvn  11514  3dvdsdec  12610  3dvds2dec  12611  3lcm2e6  12916  dec5dvds  13169  dec5dvds2  13170  dec2nprm  13172  modxai  13173  mod2xi  13174  modsubi  13176  gcdi  13177  numexp0  13179  numexp1  13180  numexpp1  13181  numexp2x  13182  decsplit0b  13183  decsplit0  13184  decsplit1  13185  decsplit  13186  karatsuba  13187  2exp8  13192  ballotfilemth  13259