Theorem nn0cn 9412

Description: A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0cn	|- ( A e. NN0 -> A e. CC )

Proof of Theorem nn0cn

Step	Hyp	Ref	Expression
1		nn0sscn 9407	. 2 |- NN0 C_ CC
2	1	sseli 3223	1 |- ( A e. NN0 -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8030   NN0cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-int 3929  df-inn 9144  df-n0 9403

This theorem is referenced by:  nn0nnaddcl  9433  elnn0nn  9444  difgtsumgt  9549  nn0n0n1ge2  9550  uzaddcl  9820  fzctr  10368  nn0split  10371  elfzoext  10437  zpnn0elfzo1  10453  ubmelm1fzo  10471  subfzo0  10488  modqmuladdnn0  10630  addmodidr  10635  modfzo0difsn  10657  nn0ennn  10695  expadd  10843  expmul  10846  bernneq  10922  bernneq2  10923  faclbnd  11003  faclbnd6  11006  bccmpl  11016  bcn0  11017  bcnn  11019  bcnp1n  11021  bcn2  11026  bcp1m1  11027  bcpasc  11028  bcn2p1  11032  hashfzo0  11087  hashfz0  11089  ccatalpha  11190  ccatws1lenp1bg  11212  ccatw2s1leng  11215  swrdfv2  11244  swrdspsleq  11248  swrdlsw  11250  pfxmpt  11261  pfxswrd  11287  wrdind  11303  wrd2ind  11304  pfxccatin12lem4  11307  pfxccatin12lem1  11309  pfxccatin12lem2  11312  pfxccatin12  11314  swrdccat3blem  11320  fisum0diag2  12009  hashiun  12040  binom1dif  12049  bcxmas  12051  geolim  12073  efaddlem  12236  efexp  12244  eftlub  12252  demoivreALT  12336  nn0ob  12470  modremain  12491  mulgcdr  12590  nn0seqcvgd  12614  modprmn0modprm0  12830  coprimeprodsq  12831  coprimeprodsq2  12832  pcexp  12883  dvdsprmpweqle  12911  difsqpwdvds  12912  znnen  13020  ennnfonelemp1  13028  mulgneg2  13744  cnfldmulg  14592  nn0subm  14599  rpcxpmul2  15639  0sgmppw  15719  2lgslem1c  15821  2lgslem3a  15824  2lgslem3b  15825  2lgslem3c  15826  2lgslem3d  15827  2lgslem3a1  15828  2lgslem3b1  15829  2lgslem3c1  15830  2lgslem3d1  15831  wlklenvclwlk  16226  clwwlknonex2lem2  16291