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

Theorem nn0cn 10589
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 10584 . 2  |-  NN0  C_  CC
21sseli 3352 1  |-  ( A  e.  NN0  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   CCcc 9280   NN0cn0 10579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-i2m1 9350  ax-1ne0 9351  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ov 6094  df-om 6477  df-recs 6832  df-rdg 6866  df-nn 10323  df-n0 10580
This theorem is referenced by:  nn0nnaddcl  10611  elnn0nn  10622  nn0sub  10630  nn0n0n1ge2  10643  uzaddcl  10911  fzctr  11529  ubmelm1fzo  11623  quoremnn0ALT  11696  addmodid  11748  nn0ennn  11801  expadd  11906  expmul  11909  bernneq  11990  bernneq2  11991  faclbnd  12066  faclbnd4lem3  12071  faclbnd4lem4  12072  faclbnd6  12075  bccmpl  12085  bcn0  12086  bcnn  12088  bcnp1n  12090  bcn2  12095  bcp1m1  12096  bcpasc  12097  bcn2p1  12101  hashfzo0  12191  hashfz0  12193  hashxplem  12195  hashfzdm  12202  fz0hash  12203  brfi1indlem  12218  lswccatn0lsw  12287  lswccat0lsw  12288  addlenrevswrd  12330  swrdspsleq  12342  swrdlsw  12346  swrd0swrd  12355  ccats1swrdeq  12363  wrdind  12371  wrd2ind  12372  swrdccatin12lem1  12375  swrdccatin12lem2b  12377  swrdccatin12lem2  12380  swrdccatin12  12382  swrdccat3blem  12386  repswswrd  12422  repswrevw  12424  2cshw  12447  swrds2  12545  swrd2lsw  12552  iseraltlem2  13160  fsum0diag2  13250  hashiun  13285  ackbijnn  13291  binom1dif  13296  bcxmas  13298  geolim  13330  geomulcvg  13336  efaddlem  13378  efexp  13385  eftlub  13393  demoivreALT  13485  divalglem4  13600  mulgcdr  13732  nn0seqcvgd  13745  modprmn0modprm0  13875  coprimeprodsq  13876  coprimeprodsq2  13877  pcexp  13926  ramub1lem1  14087  mulgneg2  15654  mndodcongi  16046  oddvdsnn0  16047  sylow1lem1  16097  efgsrel  16231  srgbinomlem4  16641  psrbagconf1o  17444  psrass1lem  17447  psrlidm  17474  psrlidmOLD  17475  psrass1  17478  psrcom  17481  mplsubrglem  17517  mplsubrglemOLD  17518  mplmonmul  17543  psropprmul  17693  coe1sclmul  17735  coe1sclmul2  17737  cnfldmulg  17848  nn0subm  17868  nn0srg  17881  dvnadd  21403  ply1divex  21608  elqaalem2  21786  geolim3  21805  dvradcnv  21886  pserdv2  21895  logtayllem  22104  logtayl  22105  cxpmul2  22134  atantayl3  22334  leibpilem2  22336  leibpi  22337  log2cnv  22339  chpp1  22493  0sgmppw  22537  logexprlim  22564  dchrhash  22610  bcctr  22614  bcmono  22616  bcmax  22617  bcp1ctr  22618  dchrisumlem1  22738  ostth2lem2  22883  cusgrasizeinds  23384  fargshiftfo  23524  gxnn0mul  23764  ipasslem1  24231  ipasslem2  24232  archirngz  26206  dmgmaddn0  27009  subfacval2  27075  relexpadd  27340  risefacval2  27513  fallfacval2  27514  risefaccl  27518  fallfaccl  27519  fallrisefac  27528  risefacp1  27532  fallfacp1  27533  fallfacfac  27548  faclimlem1  27549  bpolysum  28196  fsumkthpow  28199  bpoly4  28202  fsumcube  28203  heiborlem4  28713  heiborlem6  28715  pell14qrgt0  29200  pell14qrdich  29210  pell1qrge1  29211  2nn0ind  29286  jm2.17a  29303  jm2.18  29337  jm2.19lem3  29340  proot1ex  29569  m1expeven  29772  stoweidlem10  29805  stoweidlem17  29812  stoweidlem26  29821  stirlinglem5  29873  stirlinglem7  29875  subsubelfzo0  30210  elfzom1elfzo  30217  zpnn0elfzo1  30222  ccatw2s1len  30268  ccatw2s1p2  30270  wlklenfislenpm1  30284  wwlknimp  30321  wlkiswwlk1  30324  wlklniswwlkn2  30334  wwlknred  30355  wwlknext  30356  wwlknredwwlkn  30358  wwlkextwrd  30360  wwlkextinj  30362  clwlkisclwwlklem2a1  30441  clwlkisclwwlklem2a4  30446  clwlkisclwwlklem2a  30447  clwlkisclwwlklem1  30449  clwlkisclwwlklem0  30450  wwlkext2clwwlk  30465  erclwwlksym0  30478  cshwlemma1  30489  wlkp1lenfislenp  30512  wwlkextproplem2  30561  wwlkextproplem3  30562  rusgranumwlks  30574  rusgranumwlk  30575  usgreghash2spot  30662  frgregordn0  30663  extwwlkfablem2  30671  numclwwlkovf2ex  30679  numclwwlk1  30691  numclwwlk3  30702  numclwwlk7  30707  ply1mulgsumlem1  30844  ply1mulgsumlem2  30845  dpfrac1  31107
  Copyright terms: Public domain W3C validator