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

Theorem nn0cn 12419
Description: A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nn0cn (𝐴 ∈ ℕ0𝐴 ∈ ℂ)

Proof of Theorem nn0cn
StepHypRef Expression
1 nn0sscn 12414 . 2 0 ⊆ ℂ
21sseli 3938 1 (𝐴 ∈ ℕ0𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  cc 11045  0cn0 12409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5254  ax-nul 5261  ax-pr 5382  ax-un 7668  ax-1cn 11105  ax-icn 11106  ax-addcl 11107  ax-mulcl 11109  ax-i2m1 11115
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7356  df-om 7799  df-2nd 7918  df-frecs 8208  df-wrecs 8239  df-recs 8313  df-rdg 8352  df-nn 12150  df-n0 12410
This theorem is referenced by:  nn0nnaddcl  12440  elnn0nn  12451  nn0sub  12459  difgtsumgt  12462  nn0n0n1ge2  12476  uzaddcl  12821  fzctr  13545  nn0split  13548  elfzoext  13621  zpnn0elfzo1  13638  ubmelm1fzo  13660  subfzo0  13686  quoremnn0ALT  13754  modmuladdnn0  13812  addmodidr  13817  modfzo0difsn  13840  nn0ennn  13876  expadd  14002  expmul  14005  bernneq  14124  bernneq2  14125  faclbnd  14182  faclbnd4lem3  14187  faclbnd4lem4  14188  faclbnd6  14191  bccmpl  14201  bcn0  14202  bcnn  14204  bcnp1n  14206  bcn2  14211  bcp1m1  14212  bcpasc  14213  bcn2p1  14217  hashfzo0  14322  hashfz0  14324  hashxplem  14325  hashdifsnp1  14387  ccatalpha  14473  ccatws1lenp1b  14501  ccatw2s1len  14505  swrdfv2  14541  swrdspsleq  14545  swrdlsw  14547  pfxmpt  14558  addlenrevpfx  14570  pfxswrd  14586  wrdind  14602  wrd2ind  14603  pfxccatin12lem4  14606  pfxccatin12lem1  14608  pfxccatin12lem2  14611  pfxccatin12  14613  swrdccat3blem  14619  repswswrd  14664  repswrevw  14667  cshwidxmodr  14684  2cshw  14693  2cshwcshw  14706  cshwcshid  14708  swrds2  14821  swrd2lsw  14833  iseraltlem2  15559  fsum0diag2  15660  hashiun  15699  ackbijnn  15705  binom1dif  15710  bcxmas  15712  geolim  15747  geomulcvg  15753  risefacval2  15885  fallfacval2  15886  risefaccl  15890  fallfaccl  15891  fallrisefac  15900  risefacp1  15904  fallfacp1  15905  fallfacfac  15920  bpolysum  15928  fsumkthpow  15931  bpoly4  15934  fsumcube  15935  efaddlem  15967  efexp  15975  eftlub  15983  demoivreALT  16075  nn0ob  16258  divalglem4  16270  modremain  16282  mulgcdr  16423  nn0seqcvgd  16438  modprmn0modprm0  16671  coprimeprodsq  16672  coprimeprodsq2  16673  pcexp  16723  dvdsprmpweqle  16750  difsqpwdvds  16751  ramub1lem1  16890  prmop1  16902  smndex2dlinvh  18719  mulgneg2  18901  mndodcongi  19316  oddvdsnn0  19317  sylow1lem1  19371  efgsrel  19507  fincygsubgodd  19882  srgbinomlem4  19946  cnfldmulg  20814  nn0subm  20837  nn0srg  20852  psrbagconf1o  21323  psrbagconf1oOLD  21324  psrass1lemOLD  21327  psrass1lem  21330  psrlidm  21356  psrass1  21358  psrcom  21362  mplsubrglem  21394  mplmonmul  21421  psropprmul  21593  coe1sclmul  21637  coe1sclmul2  21639  dvnadd  25277  ply1divex  25485  elqaalem2  25664  geolim3  25683  dvradcnv  25764  pserdv2  25773  logtayllem  25998  logtayl  25999  cxpmul2  26028  atantayl3  26273  leibpilem2  26275  leibpi  26276  log2cnv  26278  dmgmaddn0  26356  chpp1  26488  0sgmppw  26530  logexprlim  26557  dchrhash  26603  bcctr  26607  bcmono  26609  bcmax  26610  bcp1ctr  26611  2lgslem1c  26725  2lgslem3a  26728  2lgslem3b  26729  2lgslem3c  26730  2lgslem3d  26731  2lgslem3a1  26732  2lgslem3b1  26733  2lgslem3c1  26734  2lgslem3d1  26735  2sqreultlem  26779  2sqreulem2  26784  dchrisumlem1  26821  ostth2lem2  26966  wlklenvclwlk  28489  upgrwlkdvdelem  28570  wwlknp  28674  wwlknlsw  28678  wlkiswwlks1  28698  wlklnwwlkln2lem  28713  wlknwwlksnbij  28719  wwlksnred  28723  wwlksnext  28724  wwlksnredwwlkn  28726  wwlksnextwrd  28728  wwlksnextinj  28730  wwlksnextproplem2  28741  wwlksnextproplem3  28742  wspthsnwspthsnon  28747  clwlkclwwlklem2a1  28822  clwlkclwwlklem2a4  28827  clwlkclwwlklem2a  28828  clwlkclwwlklem2  28830  clwlkclwwlklem3  28831  wwlksext2clwwlk  28887  clwwlknonex2lem2  28938  eucrctshift  29073  eucrct2eupth  29075  numclwwlk2lem1lem  29172  numclwwlk1  29191  numclwwlk7  29221  ipasslem1  29659  ipasslem2  29660  dpfrac1  31631  archirngz  31908  pthhashvtx  33590  subfacval2  33650  bccolsum  34182  faclimlem1  34186  poimirlem28  36073  heiborlem4  36240  heiborlem6  36242  lcmineqlem3  40455  facp2  40518  sticksstones7  40527  fac2xp3  40579  factwoffsmonot  40582  nn0rppwr  40757  pell14qrgt0  41120  pell14qrdich  41130  pell1qrge1  41131  2nn0ind  41207  jm2.17a  41222  jm2.18  41250  jm2.19lem3  41253  proot1ex  41466  bcc0  42562  dvradcnv2  42569  binomcxplemrat  42572  binomcxplemnotnn0  42578  fperiodmullem  43473  stoweidlem10  44183  stoweidlem17  44190  stoweidlem26  44199  stirlinglem5  44251  stirlinglem7  44253  etransclem23  44430  subsubelfzo0  45490  fargshiftfo  45566  fmtnodvds  45668  goldbachthlem1  45669  fmtnofac2lem  45692  fmtnofac1  45694  nn0onn0exALTV  45823  nn0enn0exALTV  45824  nn0mnd  46045  ply1mulgsumlem1  46399  ply1mulgsumlem2  46400  nn0onn0ex  46541  nn0enn0ex  46542  fllog2  46586  dignn0fr  46619  digexp  46625  0dig2nn0e  46630  0dig2nn0o  46631  dignn0ehalf  46635  nn0mulfsum  46642  nn0mullong  46643  itcovalpclem1  46688  itcovalpclem2  46689  itcovalt2lem2lem2  46692  ackval1  46699  ackval2  46700  ackval3  46701
  Copyright terms: Public domain W3C validator