Theorem nn0cni 9278

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

Syntax hints:   e. wcel 2167   CCcc 7894   NN0cn0 9266

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7987  ax-resscn 7988  ax-1re 7990  ax-addrcl 7993  ax-rnegex 8005

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-int 3876  df-inn 9008  df-n0 9267

This theorem is referenced by:  nn0le2xi  9316  num0u  9484  num0h  9485  numsuc  9487  numsucc  9513  numma  9517  nummac  9518  numma2c  9519  numadd  9520  numaddc  9521  nummul1c  9522  nummul2c  9523  decrmanc  9530  decrmac  9531  decaddi  9533  decaddci  9534  decsubi  9536  decmul1  9537  decmulnc  9540  11multnc  9541  decmul10add  9542  6p5lem  9543  4t3lem  9570  7t3e21  9583  7t6e42  9586  8t3e24  9589  8t4e32  9590  8t8e64  9594  9t3e27  9596  9t4e36  9597  9t5e45  9598  9t6e54  9599  9t7e63  9600  9t11e99  9603  decbin0  9613  decbin2  9614  sq10  10821  3dec  10823  3dvdsdec  12047  3dvds2dec  12048  3lcm2e6  12353  dec5dvds  12606  dec5dvds2  12607  dec2nprm  12609  modxai  12610  mod2xi  12611  modsubi  12613  gcdi  12614  numexp0  12616  numexp1  12617  numexpp1  12618  numexp2x  12619  decsplit0b  12620  decsplit0  12621  decsplit1  12622  decsplit  12623  karatsuba  12624  2exp8  12629