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

Theorem nn0cn 10805
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 10800 . 2  |-  NN0  C_  CC
21sseli 3500 1  |-  ( A  e.  NN0  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   CCcc 9490   NN0cn0 10795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-i2m1 9560  ax-1ne0 9561  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-om 6685  df-recs 7042  df-rdg 7076  df-nn 10537  df-n0 10796
This theorem is referenced by:  nn0nnaddcl  10827  elnn0nn  10838  nn0sub  10846  nn0n0n1ge2  10859  uzaddcl  11137  fzctr  11784  nn0split  11787  zpnn0elfzo1  11857  ubmelm1fzo  11876  quoremnn0ALT  11952  addmodid  12004  nn0ennn  12057  expadd  12176  expmul  12179  bernneq  12260  bernneq2  12261  faclbnd  12336  faclbnd4lem3  12341  faclbnd4lem4  12342  faclbnd6  12345  bccmpl  12355  bcn0  12356  bcnn  12358  bcnp1n  12360  bcn2  12365  bcp1m1  12366  bcpasc  12367  bcn2p1  12371  hashfzo0  12453  hashfz0  12455  hashxplem  12457  hashfzdm  12464  fz0hash  12465  brfi1indlem  12497  lswccatn0lsw  12571  lswccat0lsw  12572  ccatw2s1len  12592  ccatw2s1p2  12604  addlenrevswrd  12624  swrdspsleq  12636  swrdlsw  12640  swrd0swrd  12649  ccats1swrdeq  12657  wrdind  12665  wrd2ind  12666  swrdccatin12lem1  12672  swrdccatin12lem2b  12674  swrdccatin12lem2  12677  swrdccatin12  12679  swrdccat3blem  12683  repswswrd  12719  repswrevw  12721  2cshw  12744  2cshwcshw  12756  cshwcshid  12758  swrds2  12846  swrd2lsw  12853  iseraltlem2  13468  fsum0diag2  13561  hashiun  13599  ackbijnn  13603  binom1dif  13608  bcxmas  13610  geolim  13642  geomulcvg  13648  efaddlem  13690  efexp  13697  eftlub  13705  demoivreALT  13797  divalglem4  13913  mulgcdr  14045  nn0seqcvgd  14058  modprmn0modprm0  14191  coprimeprodsq  14192  coprimeprodsq2  14193  pcexp  14242  ramub1lem1  14403  mulgneg2  15979  mndodcongi  16373  oddvdsnn0  16374  sylow1lem1  16424  efgsrel  16558  srgbinomlem4  16996  psrbagconf1o  17825  psrass1lem  17828  psrlidm  17855  psrlidmOLD  17856  psrass1  17859  psrcom  17863  mplsubrglem  17899  mplsubrglemOLD  17900  mplmonmul  17925  psropprmul  18078  coe1sclmul  18122  coe1sclmul2  18124  cnfldmulg  18249  nn0subm  18269  nn0srg  18282  dvnadd  22095  ply1divex  22300  elqaalem2  22478  geolim3  22497  dvradcnv  22578  pserdv2  22587  logtayllem  22796  logtayl  22797  cxpmul2  22826  atantayl3  23026  leibpilem2  23028  leibpi  23029  log2cnv  23031  chpp1  23185  0sgmppw  23229  logexprlim  23256  dchrhash  23302  bcctr  23306  bcmono  23308  bcmax  23309  bcp1ctr  23310  dchrisumlem1  23430  ostth2lem2  23575  cusgrasizeinds  24180  wlklenvm1  24236  fargshiftfo  24342  wwlknimp  24391  wlkiswwlk1  24394  wlklniswwlkn2  24404  wwlknred  24427  wwlknext  24428  wwlknredwwlkn  24430  wwlkextwrd  24432  wwlkextinj  24434  wwlkextproplem2  24446  wwlkextproplem3  24447  clwlkisclwwlklem2a1  24483  clwlkisclwwlklem2a4  24488  clwlkisclwwlklem2a  24489  clwlkisclwwlklem1  24491  clwlkisclwwlklem0  24492  wwlkext2clwwlk  24507  wlklenvclwlk  24543  rusgranumwlks  24660  rusgranumwlk  24661  usgreghash2spot  24774  frgregordn0  24775  extwwlkfablem2  24783  numclwwlkovf2ex  24791  numclwwlk1  24803  numclwwlk3  24814  numclwwlk7  24819  gxnn0mul  24983  ipasslem1  25450  ipasslem2  25451  archirngz  27423  dmgmaddn0  28233  subfacval2  28299  relexpadd  28564  risefacval2  28737  fallfacval2  28738  risefaccl  28742  fallfaccl  28743  fallrisefac  28752  risefacp1  28756  fallfacp1  28757  fallfacfac  28772  faclimlem1  28773  bpolysum  29420  fsumkthpow  29423  bpoly4  29426  fsumcube  29427  heiborlem4  29941  heiborlem6  29943  pell14qrgt0  30427  pell14qrdich  30437  pell1qrge1  30438  2nn0ind  30513  jm2.17a  30530  jm2.18  30562  jm2.19lem3  30565  proot1ex  30794  fzisoeu  31105  fperiodmullem  31108  m1expeven  31169  stoweidlem10  31338  stoweidlem17  31345  stoweidlem26  31354  stirlinglem5  31406  stirlinglem7  31408  fourierdlem54  31489  subsubelfzo0  31833  ply1mulgsumlem1  32085  ply1mulgsumlem2  32086  dpfrac1  32265
  Copyright terms: Public domain W3C validator