Theorem nn0cni 9252

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

Syntax hints:   e. wcel 2164   CCcc 7870   NN0cn0 9240

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969  ax-rnegex 7981

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-sn 3624  df-int 3871  df-inn 8983  df-n0 9241

This theorem is referenced by:  nn0le2xi  9290  num0u  9458  num0h  9459  numsuc  9461  numsucc  9487  numma  9491  nummac  9492  numma2c  9493  numadd  9494  numaddc  9495  nummul1c  9496  nummul2c  9497  decrmanc  9504  decrmac  9505  decaddi  9507  decaddci  9508  decsubi  9510  decmul1  9511  decmulnc  9514  11multnc  9515  decmul10add  9516  6p5lem  9517  4t3lem  9544  7t3e21  9557  7t6e42  9560  8t3e24  9563  8t4e32  9564  8t8e64  9568  9t3e27  9570  9t4e36  9571  9t5e45  9572  9t6e54  9573  9t7e63  9574  9t11e99  9577  decbin0  9587  decbin2  9588  sq10  10783  3dec  10785  3dvdsdec  12006  3dvds2dec  12007  3lcm2e6  12298