MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0cn Structured version   Unicode version

Theorem nn0cn 10585
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
StepHypRef Expression
1 nn0sscn 10580 . 2  |-  NN0  C_  CC
21sseli 3349 1  |-  ( A  e.  NN0  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   CCcc 9276   NN0cn0 10575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-i2m1 9346  ax-1ne0 9347  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-om 6476  df-recs 6828  df-rdg 6862  df-nn 10319  df-n0 10576
This theorem is referenced by:  nn0nnaddcl  10607  elnn0nn  10618  nn0sub  10626  nn0n0n1ge2  10639  uzaddcl  10907  fzctr  11525  ubmelm1fzo  11619  quoremnn0ALT  11692  addmodid  11744  nn0ennn  11797  expadd  11902  expmul  11905  bernneq  11986  bernneq2  11987  faclbnd  12062  faclbnd4lem3  12067  faclbnd4lem4  12068  faclbnd6  12071  bccmpl  12081  bcn0  12082  bcnn  12084  bcnp1n  12086  bcn2  12091  bcp1m1  12092  bcpasc  12093  bcn2p1  12097  hashfzo0  12187  hashfz0  12189  hashxplem  12191  hashfzdm  12198  fz0hash  12199  brfi1indlem  12214  lswccatn0lsw  12283  lswccat0lsw  12284  addlenrevswrd  12326  swrdspsleq  12338  swrdlsw  12342  swrd0swrd  12351  ccats1swrdeq  12359  wrdind  12367  wrd2ind  12368  swrdccatin12lem1  12371  swrdccatin12lem2b  12373  swrdccatin12lem2  12376  swrdccatin12  12378  swrdccat3blem  12382  repswswrd  12418  repswrevw  12420  2cshw  12443  swrds2  12541  swrd2lsw  12548  iseraltlem2  13156  fsum0diag2  13246  hashiun  13281  ackbijnn  13287  binom1dif  13292  bcxmas  13294  geolim  13326  geomulcvg  13332  efaddlem  13374  efexp  13381  eftlub  13389  demoivreALT  13481  divalglem4  13596  mulgcdr  13728  nn0seqcvgd  13741  modprmn0modprm0  13871  coprimeprodsq  13872  coprimeprodsq2  13873  pcexp  13922  ramub1lem1  14083  mulgneg2  15647  mndodcongi  16039  oddvdsnn0  16040  sylow1lem1  16090  efgsrel  16224  srgbinomlem4  16631  psrbagconf1o  17434  psrass1lem  17437  psrlidm  17464  psrlidmOLD  17465  psrass1  17468  psrcom  17471  mplsubrglem  17507  mplsubrglemOLD  17508  mplmonmul  17533  psropprmul  17647  coe1sclmul  17689  coe1sclmul2  17691  cnfldmulg  17748  nn0subm  17768  nn0srg  17781  dvnadd  21303  ply1divex  21551  elqaalem2  21729  geolim3  21748  dvradcnv  21829  pserdv2  21838  logtayllem  22047  logtayl  22048  cxpmul2  22077  atantayl3  22277  leibpilem2  22279  leibpi  22280  log2cnv  22282  chpp1  22436  0sgmppw  22480  logexprlim  22507  dchrhash  22553  bcctr  22557  bcmono  22559  bcmax  22560  bcp1ctr  22561  dchrisumlem1  22681  ostth2lem2  22826  cusgrasizeinds  23303  fargshiftfo  23443  gxnn0mul  23683  ipasslem1  24150  ipasslem2  24151  archirngz  26123  eulerpartlemb  26665  dmgmaddn0  26923  subfacval2  26989  relexpadd  27253  risefacval2  27426  fallfacval2  27427  risefaccl  27431  fallfaccl  27432  fallrisefac  27441  risefacp1  27445  fallfacp1  27446  fallfacfac  27461  faclimlem1  27462  bpolysum  28109  fsumkthpow  28112  bpoly4  28115  fsumcube  28116  heiborlem4  28622  heiborlem6  28624  pell14qrgt0  29109  pell14qrdich  29119  pell1qrge1  29120  2nn0ind  29195  jm2.17a  29212  jm2.18  29246  jm2.19lem3  29249  proot1ex  29478  m1expeven  29681  stoweidlem10  29714  stoweidlem17  29721  stoweidlem26  29730  stirlinglem5  29782  stirlinglem7  29784  subsubelfzo0  30119  elfzom1elfzo  30126  zpnn0elfzo1  30131  ccatw2s1len  30177  ccatw2s1p2  30179  wlklenfislenpm1  30193  wwlknimp  30230  wlkiswwlk1  30233  wlklniswwlkn2  30243  wwlknred  30264  wwlknext  30265  wwlknredwwlkn  30267  wwlkextwrd  30269  wwlkextinj  30271  clwlkisclwwlklem2a1  30350  clwlkisclwwlklem2a4  30355  clwlkisclwwlklem2a  30356  clwlkisclwwlklem1  30358  clwlkisclwwlklem0  30359  wwlkext2clwwlk  30374  erclwwlksym0  30387  cshwlemma1  30398  wlkp1lenfislenp  30421  wwlkextproplem2  30470  wwlkextproplem3  30471  rusgranumwlks  30483  rusgranumwlk  30484  usgreghash2spot  30571  frgregordn0  30572  extwwlkfablem2  30580  numclwwlkovf2ex  30588  numclwwlk1  30600  numclwwlk3  30611  numclwwlk7  30616  dpfrac1  30931
  Copyright terms: Public domain W3C validator