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

Theorem nn0cn 12424
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 12419 . 2 0 ⊆ ℂ
21sseli 3941 1 (𝐴 ∈ ℕ0𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cc 11050  0cn0 12414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-mulcl 11114  ax-i2m1 11120
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-nn 12155  df-n0 12415
This theorem is referenced by:  nn0nnaddcl  12445  elnn0nn  12456  nn0sub  12464  difgtsumgt  12467  nn0n0n1ge2  12481  uzaddcl  12830  fzctr  13554  nn0split  13557  elfzoext  13630  zpnn0elfzo1  13647  ubmelm1fzo  13669  subfzo0  13695  quoremnn0ALT  13763  modmuladdnn0  13821  addmodidr  13826  modfzo0difsn  13849  nn0ennn  13885  expadd  14011  expmul  14014  bernneq  14133  bernneq2  14134  faclbnd  14191  faclbnd4lem3  14196  faclbnd4lem4  14197  faclbnd6  14200  bccmpl  14210  bcn0  14211  bcnn  14213  bcnp1n  14215  bcn2  14220  bcp1m1  14221  bcpasc  14222  bcn2p1  14226  hashfzo0  14331  hashfz0  14333  hashxplem  14334  hashdifsnp1  14396  ccatalpha  14482  ccatws1lenp1b  14510  ccatw2s1len  14514  swrdfv2  14550  swrdspsleq  14554  swrdlsw  14556  pfxmpt  14567  addlenrevpfx  14579  pfxswrd  14595  wrdind  14611  wrd2ind  14612  pfxccatin12lem4  14615  pfxccatin12lem1  14617  pfxccatin12lem2  14620  pfxccatin12  14622  swrdccat3blem  14628  repswswrd  14673  repswrevw  14676  cshwidxmodr  14693  2cshw  14702  2cshwcshw  14715  cshwcshid  14717  swrds2  14830  swrd2lsw  14842  iseraltlem2  15568  fsum0diag2  15669  hashiun  15708  ackbijnn  15714  binom1dif  15719  bcxmas  15721  geolim  15756  geomulcvg  15762  risefacval2  15894  fallfacval2  15895  risefaccl  15899  fallfaccl  15900  fallrisefac  15909  risefacp1  15913  fallfacp1  15914  fallfacfac  15929  bpolysum  15937  fsumkthpow  15940  bpoly4  15943  fsumcube  15944  efaddlem  15976  efexp  15984  eftlub  15992  demoivreALT  16084  nn0ob  16267  divalglem4  16279  modremain  16291  mulgcdr  16432  nn0seqcvgd  16447  modprmn0modprm0  16680  coprimeprodsq  16681  coprimeprodsq2  16682  pcexp  16732  dvdsprmpweqle  16759  difsqpwdvds  16760  ramub1lem1  16899  prmop1  16911  smndex2dlinvh  18728  mulgneg2  18911  mndodcongi  19326  oddvdsnn0  19327  sylow1lem1  19381  efgsrel  19517  fincygsubgodd  19892  srgbinomlem4  19961  cnfldmulg  20832  nn0subm  20855  nn0srg  20870  psrbagconf1o  21341  psrbagconf1oOLD  21342  psrass1lemOLD  21345  psrass1lem  21348  psrlidm  21375  psrass1  21377  psrcom  21381  mplsubrglem  21413  mplmonmul  21440  psropprmul  21612  coe1sclmul  21656  coe1sclmul2  21658  dvnadd  25296  ply1divex  25504  elqaalem2  25683  geolim3  25702  dvradcnv  25783  pserdv2  25792  logtayllem  26017  logtayl  26018  cxpmul2  26047  atantayl3  26292  leibpilem2  26294  leibpi  26295  log2cnv  26297  dmgmaddn0  26375  chpp1  26507  0sgmppw  26549  logexprlim  26576  dchrhash  26622  bcctr  26626  bcmono  26628  bcmax  26629  bcp1ctr  26630  2lgslem1c  26744  2lgslem3a  26747  2lgslem3b  26748  2lgslem3c  26749  2lgslem3d  26750  2lgslem3a1  26751  2lgslem3b1  26752  2lgslem3c1  26753  2lgslem3d1  26754  2sqreultlem  26798  2sqreulem2  26803  dchrisumlem1  26840  ostth2lem2  26985  wlklenvclwlk  28606  upgrwlkdvdelem  28687  wwlknp  28791  wwlknlsw  28795  wlkiswwlks1  28815  wlklnwwlkln2lem  28830  wlknwwlksnbij  28836  wwlksnred  28840  wwlksnext  28841  wwlksnredwwlkn  28843  wwlksnextwrd  28845  wwlksnextinj  28847  wwlksnextproplem2  28858  wwlksnextproplem3  28859  wspthsnwspthsnon  28864  clwlkclwwlklem2a1  28939  clwlkclwwlklem2a4  28944  clwlkclwwlklem2a  28945  clwlkclwwlklem2  28947  clwlkclwwlklem3  28948  wwlksext2clwwlk  29004  clwwlknonex2lem2  29055  eucrctshift  29190  eucrct2eupth  29192  numclwwlk2lem1lem  29289  numclwwlk1  29308  numclwwlk7  29338  ipasslem1  29776  ipasslem2  29777  dpfrac1  31751  archirngz  32028  pthhashvtx  33724  subfacval2  33784  bccolsum  34315  faclimlem1  34319  poimirlem28  36109  heiborlem4  36276  heiborlem6  36278  lcmineqlem3  40491  facp2  40554  sticksstones7  40563  fac2xp3  40615  factwoffsmonot  40618  nn0rppwr  40822  pell14qrgt0  41185  pell14qrdich  41195  pell1qrge1  41196  2nn0ind  41272  jm2.17a  41287  jm2.18  41315  jm2.19lem3  41318  proot1ex  41531  bcc0  42627  dvradcnv2  42634  binomcxplemrat  42637  binomcxplemnotnn0  42643  fperiodmullem  43544  stoweidlem10  44258  stoweidlem17  44265  stoweidlem26  44274  stirlinglem5  44326  stirlinglem7  44328  etransclem23  44505  subsubelfzo0  45565  fargshiftfo  45641  fmtnodvds  45743  goldbachthlem1  45744  fmtnofac2lem  45767  fmtnofac1  45769  nn0onn0exALTV  45898  nn0enn0exALTV  45899  nn0mnd  46120  ply1mulgsumlem1  46474  ply1mulgsumlem2  46475  nn0onn0ex  46616  nn0enn0ex  46617  fllog2  46661  dignn0fr  46694  digexp  46700  0dig2nn0e  46705  0dig2nn0o  46706  dignn0ehalf  46710  nn0mulfsum  46717  nn0mullong  46718  itcovalpclem1  46763  itcovalpclem2  46764  itcovalt2lem2lem2  46767  ackval1  46774  ackval2  46775  ackval3  46776
  Copyright terms: Public domain W3C validator