Theorem nn0cni 9187

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

Syntax hints:   e. wcel 2148   CCcc 7808   NN0cn0 9175

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4121  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907  ax-rnegex 7919

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-int 3845  df-inn 8919  df-n0 9176

This theorem is referenced by:  nn0le2xi  9225  num0u  9393  num0h  9394  numsuc  9396  numsucc  9422  numma  9426  nummac  9427  numma2c  9428  numadd  9429  numaddc  9430  nummul1c  9431  nummul2c  9432  decrmanc  9439  decrmac  9440  decaddi  9442  decaddci  9443  decsubi  9445  decmul1  9446  decmulnc  9449  11multnc  9450  decmul10add  9451  6p5lem  9452  4t3lem  9479  7t3e21  9492  7t6e42  9495  8t3e24  9498  8t4e32  9499  8t8e64  9503  9t3e27  9505  9t4e36  9506  9t5e45  9507  9t6e54  9508  9t7e63  9509  9t11e99  9512  decbin0  9522  decbin2  9523  sq10  10691  3dec  10693  3dvdsdec  11869  3dvds2dec  11870  3lcm2e6  12159