Theorem nn0cni 9188

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

Syntax hints:   e. wcel 2148   CCcc 7809   NN0cn0 9176

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 4122  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908  ax-rnegex 7920

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 2740  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-int 3846  df-inn 8920  df-n0 9177

This theorem is referenced by:  nn0le2xi  9226  num0u  9394  num0h  9395  numsuc  9397  numsucc  9423  numma  9427  nummac  9428  numma2c  9429  numadd  9430  numaddc  9431  nummul1c  9432  nummul2c  9433  decrmanc  9440  decrmac  9441  decaddi  9443  decaddci  9444  decsubi  9446  decmul1  9447  decmulnc  9450  11multnc  9451  decmul10add  9452  6p5lem  9453  4t3lem  9480  7t3e21  9493  7t6e42  9496  8t3e24  9499  8t4e32  9500  8t8e64  9504  9t3e27  9506  9t4e36  9507  9t5e45  9508  9t6e54  9509  9t7e63  9510  9t11e99  9513  decbin0  9523  decbin2  9524  sq10  10692  3dec  10694  3dvdsdec  11870  3dvds2dec  11871  3lcm2e6  12160