Theorem nn0cni 9342

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

Syntax hints:   e. wcel 2178   CCcc 7958   NN0cn0 9330

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178  ax-cnex 8051  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057  ax-rnegex 8069

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-sn 3649  df-int 3900  df-inn 9072  df-n0 9331

This theorem is referenced by:  nn0le2xi  9380  num0u  9549  num0h  9550  numsuc  9552  numsucc  9578  numma  9582  nummac  9583  numma2c  9584  numadd  9585  numaddc  9586  nummul1c  9587  nummul2c  9588  decrmanc  9595  decrmac  9596  decaddi  9598  decaddci  9599  decsubi  9601  decmul1  9602  decmulnc  9605  11multnc  9606  decmul10add  9607  6p5lem  9608  4t3lem  9635  7t3e21  9648  7t6e42  9651  8t3e24  9654  8t4e32  9655  8t8e64  9659  9t3e27  9661  9t4e36  9662  9t5e45  9663  9t6e54  9664  9t7e63  9665  9t11e99  9668  decbin0  9678  decbin2  9679  sq10  10894  3dec  10896  3dvdsdec  12291  3dvds2dec  12292  3lcm2e6  12597  dec5dvds  12850  dec5dvds2  12851  dec2nprm  12853  modxai  12854  mod2xi  12855  modsubi  12857  gcdi  12858  numexp0  12860  numexp1  12861  numexpp1  12862  numexp2x  12863  decsplit0b  12864  decsplit0  12865  decsplit1  12866  decsplit  12867  karatsuba  12868  2exp8  12873