Theorem nn0cn 12428

Description: A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0cn	⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ)

Proof of Theorem nn0cn

Step	Hyp	Ref	Expression
1		nn0sscn 12423	. 2 ⊢ ℕ0 ⊆ ℂ
2	1	sseli 3939	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11042  ℕ₀cn0 12418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-i2m1 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  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 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163  df-n0 12419

This theorem is referenced by:  nn0nnaddcl  12449  elnn0nn  12460  nn0sub  12468  difgtsumgt  12471  nn0le2x  12472  nn0n0n1ge2  12486  uzaddcl  12839  fzctr  13577  nn0split  13580  elfzoext  13659  zpnn0elfzo1  13676  ubmelm1fzo  13700  subfzo0  13726  quoremnn0ALT  13795  modmuladdnn0  13856  addmodidr  13861  modfzo0difsn  13884  nn0ennn  13920  expadd  14045  expmul  14048  bernneq  14170  bernneq2  14171  faclbnd  14231  faclbnd4lem3  14236  faclbnd4lem4  14237  faclbnd6  14240  bccmpl  14250  bcn0  14251  bcnn  14253  bcnp1n  14255  bcn2  14260  bcp1m1  14261  bcpasc  14262  bcn2p1  14266  hashfzo0  14371  hashfz0  14373  hashxplem  14374  hashdifsnp1  14447  ccatalpha  14534  ccatws1lenp1b  14562  ccatw2s1len  14566  swrdfv2  14602  swrdspsleq  14606  swrdlsw  14608  pfxmpt  14619  addlenrevpfx  14631  pfxswrd  14647  wrdind  14663  wrd2ind  14664  pfxccatin12lem4  14667  pfxccatin12lem1  14669  pfxccatin12lem2  14672  pfxccatin12  14674  swrdccat3blem  14680  repswswrd  14725  repswrevw  14728  cshwidxmodr  14745  2cshw  14754  2cshwcshw  14767  cshwcshid  14769  swrds2  14882  swrd2lsw  14894  iseraltlem2  15625  fsum0diag2  15725  hashiun  15764  ackbijnn  15770  binom1dif  15775  bcxmas  15777  geolim  15812  geomulcvg  15818  risefacval2  15952  fallfacval2  15953  risefaccl  15957  fallfaccl  15958  fallrisefac  15967  risefacp1  15971  fallfacp1  15972  fallfacfac  15987  bpolysum  15995  fsumkthpow  15998  bpoly4  16001  fsumcube  16002  efaddlem  16035  efexp  16045  eftlub  16053  demoivreALT  16145  nn0ob  16330  divalglem4  16342  modremain  16354  mulgcdr  16496  nn0rppwr  16507  nn0seqcvgd  16516  modprmn0modprm0  16754  coprimeprodsq  16755  coprimeprodsq2  16756  pcexp  16806  dvdsprmpweqle  16833  difsqpwdvds  16834  ramub1lem1  16973  prmop1  16985  smndex2dlinvh  18826  mulgneg2  19022  mndodcongi  19457  oddvdsnn0  19458  sylow1lem1  19512  efgsrel  19648  fincygsubgodd  20028  srgbinomlem4  20149  cnfldmulg  21345  nn0subm  21364  nn0srg  21379  psrbagconf1o  21871  psrass1lem  21874  psrlidm  21904  psrass1  21906  psrcom  21910  mplsubrglem  21946  mplmonmul  21976  psdmul  22086  psdmvr  22089  psropprmul  22155  coe1sclmul  22201  coe1sclmul2  22203  dvnadd  25864  ply1divex  26075  elqaalem2  26261  geolim3  26280  dvradcnv  26363  pserdv2  26373  logtayllem  26601  logtayl  26602  cxpmul2  26631  atantayl3  26882  leibpilem2  26884  leibpi  26885  log2cnv  26887  dmgmaddn0  26966  chpp1  27098  0sgmppw  27142  logexprlim  27169  dchrhash  27215  bcctr  27219  bcmono  27221  bcmax  27222  bcp1ctr  27223  2lgslem1c  27337  2lgslem3a  27340  2lgslem3b  27341  2lgslem3c  27342  2lgslem3d  27343  2lgslem3a1  27344  2lgslem3b1  27345  2lgslem3c1  27346  2lgslem3d1  27347  2sqreultlem  27391  2sqreulem2  27396  dchrisumlem1  27433  ostth2lem2  27578  wlklenvclwlk  29634  upgrwlkdvdelem  29716  wwlknp  29823  wwlknlsw  29827  wlkiswwlks1  29847  wlklnwwlkln2lem  29862  wlknwwlksnbij  29868  wwlksnred  29872  wwlksnext  29873  wwlksnredwwlkn  29875  wwlksnextwrd  29877  wwlksnextinj  29879  wwlksnextproplem2  29890  wwlksnextproplem3  29891  wspthsnwspthsnon  29896  clwlkclwwlklem2a1  29971  clwlkclwwlklem2a4  29976  clwlkclwwlklem2a  29977  clwlkclwwlklem2  29979  clwlkclwwlklem3  29980  wwlksext2clwwlk  30036  clwwlknonex2lem2  30087  eucrctshift  30222  eucrct2eupth  30224  numclwwlk2lem1lem  30321  numclwwlk1  30340  numclwwlk7  30370  ipasslem1  30810  ipasslem2  30811  dpfrac1  32862  archirngz  33158  nn0constr  33744  pthhashvtx  35108  subfacval2  35167  bccolsum  35719  faclimlem1  35723  poimirlem28  37635  heiborlem4  37801  heiborlem6  37803  lcmineqlem3  42012  facp2  42124  sticksstones7  42133  oddnumth  42292  nicomachus  42293  sumcubes  42294  pell14qrgt0  42840  pell14qrdich  42850  pell1qrge1  42851  2nn0ind  42927  jm2.17a  42942  jm2.18  42970  jm2.19lem3  42973  proot1ex  43178  bcc0  44322  dvradcnv2  44329  binomcxplemrat  44332  binomcxplemnotnn0  44338  fperiodmullem  45294  stoweidlem10  46001  stoweidlem17  46008  stoweidlem26  46017  stirlinglem5  46069  stirlinglem7  46071  etransclem23  46248  cjnpoly  46883  subsubelfzo0  47320  fargshiftfo  47436  fmtnodvds  47538  goldbachthlem1  47539  fmtnofac2lem  47562  fmtnofac1  47564  nn0onn0exALTV  47693  nn0enn0exALTV  47694  isubgr3stgrlem2  47959  nn0mnd  48160  ply1mulgsumlem1  48368  ply1mulgsumlem2  48369  nn0onn0ex  48505  nn0enn0ex  48506  fllog2  48550  dignn0fr  48583  digexp  48589  0dig2nn0e  48594  0dig2nn0o  48595  dignn0ehalf  48599  nn0mulfsum  48606  nn0mullong  48607  itcovalpclem1  48652  itcovalpclem2  48653  itcovalt2lem2lem2  48656  ackval1  48663  ackval2  48664  ackval3  48665