Theorem nn0cn 10830

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

Assertion

Ref	Expression
nn0cn

Proof of Theorem nn0cn

Step	Hyp	Ref	Expression
1		nn0sscn 10825	. 2
2	1	sseli 3499	1

Syntax hints:  ->wi 4  e.wcel 1818  cc 9511  cn0 10820

This theorem is referenced by:  nn0nnaddcl  10852  elnn0nn  10863  nn0sub  10871  nn0n0n1ge2  10884  uzaddcl  11166  fzctr  11816  nn0split  11819  zpnn0elfzo1  11889  ubmelm1fzo  11908  quoremnn0ALT  11984  addmodid  12036  nn0ennn  12089  expadd  12208  expmul  12211  bernneq  12292  bernneq2  12293  faclbnd  12368  faclbnd4lem3  12373  faclbnd4lem4  12374  faclbnd6  12377  bccmpl  12387  bcn0  12388  bcnn  12390  bcnp1n  12392  bcn2  12397  bcp1m1  12398  bcpasc  12399  bcn2p1  12403  hashfzo0  12488  hashfz0  12490  hashxplem  12491  brfi1indlem  12531  lswccatn0lsw  12607  lswccat0lsw  12608  ccatw2s1len  12629  ccatw2s1p2  12641  addlenrevswrd  12661  swrdspsleq  12673  swrdlsw  12677  swrd0swrd  12686  ccats1swrdeq  12694  wrdind  12702  wrd2ind  12703  swrdccatin12lem1  12709  swrdccatin12lem2b  12711  swrdccatin12lem2  12714  swrdccatin12  12716  swrdccat3blem  12720  repswswrd  12756  repswrevw  12758  2cshw  12781  2cshwcshw  12793  cshwcshid  12795  swrds2  12883  swrd2lsw  12890  iseraltlem2  13505  fsum0diag2  13598  hashiun  13636  ackbijnn  13640  binom1dif  13645  bcxmas  13647  geolim  13679  geomulcvg  13685  efaddlem  13828  efexp  13836  eftlub  13844  demoivreALT  13936  divalglem4  14054  mulgcdr  14186  nn0seqcvgd  14199  modprmn0modprm0  14332  coprimeprodsq  14333  coprimeprodsq2  14334  pcexp  14383  ramub1lem1  14544  mulgneg2  16169  mndodcongi  16567  oddvdsnn0  16568  sylow1lem1  16618  efgsrel  16752  srgbinomlem4  17194  psrbagconf1o  18026  psrass1lem  18029  psrlidm  18056  psrlidmOLD  18057  psrass1  18060  psrcom  18064  mplsubrglem  18100  mplsubrglemOLD  18101  mplmonmul  18126  psropprmul  18279  coe1sclmul  18323  coe1sclmul2  18325  cnfldmulg  18450  nn0subm  18473  nn0srg  18486  dvnadd  22332  ply1divex  22537  elqaalem2  22716  geolim3  22735  dvradcnv  22816  pserdv2  22825  logtayllem  23040  logtayl  23041  cxpmul2  23070  atantayl3  23270  leibpilem2  23272  leibpi  23273  log2cnv  23275  chpp1  23429  0sgmppw  23473  logexprlim  23500  dchrhash  23546  bcctr  23550  bcmono  23552  bcmax  23553  bcp1ctr  23554  dchrisumlem1  23674  ostth2lem2  23819  cusgrasizeinds  24476  wlklenvm1  24532  fargshiftfo  24638  wwlknimp  24687  wlkiswwlk1  24690  wlklniswwlkn2  24700  wwlknred  24723  wwlknext  24724  wwlknredwwlkn  24726  wwlkextwrd  24728  wwlkextinj  24730  wwlkextproplem2  24742  wwlkextproplem3  24743  clwlkisclwwlklem2a1  24779  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwlkisclwwlklem0  24788  wwlkext2clwwlk  24803  wlklenvclwlk  24839  rusgranumwlks  24956  rusgranumwlk  24957  usgreghash2spot  25069  frgregordn0  25070  extwwlkfablem2  25078  numclwwlkovf2ex  25086  numclwwlk1  25098  numclwwlk3  25109  numclwwlk7  25114  gxnn0mul  25279  ipasslem1  25746  ipasslem2  25747  archirngz  27733  dmgmaddn0  28565  subfacval2  28631  relexpadd  29061  risefacval2  29132  fallfacval2  29133  risefaccl  29137  fallfaccl  29138  fallrisefac  29147  risefacp1  29151  fallfacp1  29152  fallfacfac  29167  faclimlem1  29168  bpolysum  29815  fsumkthpow  29818  bpoly4  29821  fsumcube  29822  heiborlem4  30310  heiborlem6  30312  pell14qrgt0  30795  pell14qrdich  30805  pell1qrge1  30806  2nn0ind  30881  jm2.17a  30898  jm2.18  30930  jm2.19lem3  30933  proot1ex  31161  bcc0  31245  dvradcnv2  31252  binomcxplemrat  31255  binomcxplemnotnn0  31261  fperiodmullem  31503  m1expeven  31585  stoweidlem10  31792  stoweidlem17  31799  stoweidlem26  31808  stirlinglem5  31860  stirlinglem7  31862  etransclem23  32040  subsubelfzo0  32338  ply1mulgsumlem1  32986  ply1mulgsumlem2  32987  dpfrac1  33166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-om 6701  df-recs 7061  df-rdg 7095  df-nn 10562  df-n0 10821