Theorem nn0cn 11302

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 11297	. 2 |- NN0 C_ CC
2	1	sseli 3599	1 |- ( A e. NN0 -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1990   CCcc 9934   NN0cn0 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-nn 11021  df-n0 11293

This theorem is referenced by:  nn0nnaddcl  11324  elnn0nn  11335  nn0sub  11343  difgtsumgt  11346  nn0n0n1ge2  11358  uzaddcl  11744  fzctr  12451  nn0split  12454  elfzoext  12524  zpnn0elfzo1  12541  ubmelm1fzo  12564  subfzo0  12590  quoremnn0ALT  12656  modmuladdnn0  12714  addmodidr  12719  modfzo0difsn  12742  nn0ennn  12778  expadd  12902  expmul  12905  bernneq  12990  bernneq2  12991  faclbnd  13077  faclbnd4lem3  13082  faclbnd4lem4  13083  faclbnd6  13086  bccmpl  13096  bcn0  13097  bcnn  13099  bcnp1n  13101  bcn2  13106  bcp1m1  13107  bcpasc  13108  bcn2p1  13112  hashfzo0  13217  hashfz0  13219  hashxplem  13220  brfi1indlem  13278  ccatalpha  13375  ccatw2s1len  13402  addlenrevswrd  13437  swrdfv2  13446  swrdspsleq  13449  swrdlsw  13452  swrd0swrd  13461  ccats1swrdeq  13469  wrdind  13476  wrd2ind  13477  swrdccatin12lem1  13484  swrdccatin12lem2b  13486  swrdccatin12lem2  13489  swrdccatin12  13491  swrdccat3blem  13495  repswswrd  13531  repswrevw  13533  cshwidxmodr  13550  2cshw  13559  2cshwcshw  13571  cshwcshid  13573  swrds2  13685  swrd2lsw  13695  iseraltlem2  14413  fsum0diag2  14515  hashiun  14554  ackbijnn  14560  binom1dif  14565  bcxmas  14567  geolim  14601  geomulcvg  14607  risefacval2  14741  fallfacval2  14742  risefaccl  14746  fallfaccl  14747  fallrisefac  14756  risefacp1  14760  fallfacp1  14761  fallfacfac  14776  bpolysum  14784  fsumkthpow  14787  bpoly4  14790  fsumcube  14791  efaddlem  14823  efexp  14831  eftlub  14839  demoivreALT  14931  nn0ob  15100  divalglem4  15119  modremain  15132  mulgcdr  15267  nn0seqcvgd  15283  modprmn0modprm0  15512  coprimeprodsq  15513  coprimeprodsq2  15514  pcexp  15564  dvdsprmpweqle  15590  difsqpwdvds  15591  ramub1lem1  15730  prmop1  15742  mulgneg2  17575  mndodcongi  17962  oddvdsnn0  17963  sylow1lem1  18013  efgsrel  18147  srgbinomlem4  18543  psrbagconf1o  19374  psrass1lem  19377  psrlidm  19403  psrass1  19405  psrcom  19409  mplsubrglem  19439  mplmonmul  19464  psropprmul  19608  coe1sclmul  19652  coe1sclmul2  19654  cnfldmulg  19778  nn0subm  19801  nn0srg  19816  dvnadd  23692  ply1divex  23896  elqaalem2  24075  geolim3  24094  dvradcnv  24175  pserdv2  24184  logtayllem  24405  logtayl  24406  cxpmul2  24435  atantayl3  24666  leibpilem2  24668  leibpi  24669  log2cnv  24671  dmgmaddn0  24749  chpp1  24881  0sgmppw  24923  logexprlim  24950  dchrhash  24996  bcctr  25000  bcmono  25002  bcmax  25003  bcp1ctr  25004  2lgslem1c  25118  2lgslem3a  25121  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2lgslem3a1  25125  2lgslem3b1  25126  2lgslem3c1  25127  2lgslem3d1  25128  dchrisumlem1  25178  ostth2lem2  25323  wlklenvclwlk  26551  upgrwlkdvdelem  26632  wwlknp  26734  wlkiswwlks1  26753  wlklnwwlkln2lem  26768  wwlksnred  26787  wwlksnext  26788  wwlksnredwwlkn  26790  wwlksnextwrd  26792  wwlksnextinj  26794  wwlksnextproplem2  26805  wwlksnextproplem3  26806  wspthsnwspthsnon  26811  clwlkclwwlklem2a1  26893  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwlkclwwlklem3  26902  wwlksext2clwwlk  26924  eucrctshift  27103  eucrct2eupth  27105  clwwlkextfrlem1  27208  numclwwlkovf2exlem2  27212  numclwwlk1  27231  numclwwlk7  27249  ipasslem1  27686  ipasslem2  27687  dpfrac1  29599  dpfrac1OLD  29600  archirngz  29743  subfacval2  31169  bccolsum  31625  faclimlem1  31629  poimirlem28  33437  heiborlem4  33613  heiborlem6  33615  pell14qrgt0  37423  pell14qrdich  37433  pell1qrge1  37434  2nn0ind  37510  jm2.17a  37527  jm2.18  37555  jm2.19lem3  37558  proot1ex  37779  bcc0  38539  dvradcnv2  38546  binomcxplemrat  38549  binomcxplemnotnn0  38555  fperiodmullem  39517  stoweidlem10  40227  stoweidlem17  40234  stoweidlem26  40243  stirlinglem5  40295  stirlinglem7  40297  etransclem23  40474  subsubelfzo0  41336  fargshiftfo  41378  pfxmpt  41387  addlenrevpfx  41397  pfxccatin12lem1  41423  pfxccatin12lem2  41424  pfxccatin12  41425  fmtnodvds  41456  goldbachthlem1  41457  fmtnofac2lem  41480  fmtnofac1  41482  nn0onn0exALTV  41609  nn0enn0exALTV  41610  ply1mulgsumlem1  42174  ply1mulgsumlem2  42175  nn0onn0ex  42318  nn0enn0ex  42319  fllog2  42362  dignn0fr  42395  digexp  42401  0dig2nn0e  42406  0dig2nn0o  42407  dignn0ehalf  42411  nn0mulfsum  42418  nn0mullong  42419