Theorem nn0cn 12534

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 12529	. 2 ⊢ ℕ0 ⊆ ℂ
2	1	sseli 3975	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2099  ℂcc 11156  ℕ₀cn0 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433  ax-un 7746  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-mulcl 11220  ax-i2m1 11226

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-om 7877  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-nn 12265  df-n0 12525

This theorem is referenced by:  nn0nnaddcl  12555  elnn0nn  12566  nn0sub  12574  difgtsumgt  12577  nn0n0n1ge2  12591  uzaddcl  12940  fzctr  13667  nn0split  13670  elfzoext  13743  zpnn0elfzo1  13760  ubmelm1fzo  13783  subfzo0  13809  quoremnn0ALT  13877  modmuladdnn0  13935  addmodidr  13940  modfzo0difsn  13963  nn0ennn  13999  expadd  14124  expmul  14127  bernneq  14246  bernneq2  14247  faclbnd  14307  faclbnd4lem3  14312  faclbnd4lem4  14313  faclbnd6  14316  bccmpl  14326  bcn0  14327  bcnn  14329  bcnp1n  14331  bcn2  14336  bcp1m1  14337  bcpasc  14338  bcn2p1  14342  hashfzo0  14447  hashfz0  14449  hashxplem  14450  hashdifsnp1  14515  ccatalpha  14601  ccatws1lenp1b  14629  ccatw2s1len  14633  swrdfv2  14669  swrdspsleq  14673  swrdlsw  14675  pfxmpt  14686  addlenrevpfx  14698  pfxswrd  14714  wrdind  14730  wrd2ind  14731  pfxccatin12lem4  14734  pfxccatin12lem1  14736  pfxccatin12lem2  14739  pfxccatin12  14741  swrdccat3blem  14747  repswswrd  14792  repswrevw  14795  cshwidxmodr  14812  2cshw  14821  2cshwcshw  14834  cshwcshid  14836  swrds2  14949  swrd2lsw  14961  iseraltlem2  15687  fsum0diag2  15787  hashiun  15826  ackbijnn  15832  binom1dif  15837  bcxmas  15839  geolim  15874  geomulcvg  15880  risefacval2  16012  fallfacval2  16013  risefaccl  16017  fallfaccl  16018  fallrisefac  16027  risefacp1  16031  fallfacp1  16032  fallfacfac  16047  bpolysum  16055  fsumkthpow  16058  bpoly4  16061  fsumcube  16062  efaddlem  16095  efexp  16103  eftlub  16111  demoivreALT  16203  nn0ob  16386  divalglem4  16398  modremain  16410  mulgcdr  16551  nn0rppwr  16562  nn0seqcvgd  16571  modprmn0modprm0  16809  coprimeprodsq  16810  coprimeprodsq2  16811  pcexp  16861  dvdsprmpweqle  16888  difsqpwdvds  16889  ramub1lem1  17028  prmop1  17040  smndex2dlinvh  18907  mulgneg2  19102  mndodcongi  19541  oddvdsnn0  19542  sylow1lem1  19596  efgsrel  19732  fincygsubgodd  20112  srgbinomlem4  20212  cnfldmulg  21395  nn0subm  21419  nn0srg  21434  psrbagconf1o  21934  psrbagconf1oOLD  21935  psrass1lemOLD  21938  psrass1lem  21941  psrlidm  21971  psrass1  21973  psrcom  21977  mplsubrglem  22013  mplmonmul  22043  psdmul  22160  psropprmul  22227  coe1sclmul  22273  coe1sclmul2  22275  dvnadd  25950  ply1divex  26164  elqaalem2  26348  geolim3  26367  dvradcnv  26450  pserdv2  26460  logtayllem  26686  logtayl  26687  cxpmul2  26716  atantayl3  26967  leibpilem2  26969  leibpi  26970  log2cnv  26972  dmgmaddn0  27051  chpp1  27183  0sgmppw  27227  logexprlim  27254  dchrhash  27300  bcctr  27304  bcmono  27306  bcmax  27307  bcp1ctr  27308  2lgslem1c  27422  2lgslem3a  27425  2lgslem3b  27426  2lgslem3c  27427  2lgslem3d  27428  2lgslem3a1  27429  2lgslem3b1  27430  2lgslem3c1  27431  2lgslem3d1  27432  2sqreultlem  27476  2sqreulem2  27481  dchrisumlem1  27518  ostth2lem2  27663  wlklenvclwlk  29592  upgrwlkdvdelem  29673  wwlknp  29777  wwlknlsw  29781  wlkiswwlks1  29801  wlklnwwlkln2lem  29816  wlknwwlksnbij  29822  wwlksnred  29826  wwlksnext  29827  wwlksnredwwlkn  29829  wwlksnextwrd  29831  wwlksnextinj  29833  wwlksnextproplem2  29844  wwlksnextproplem3  29845  wspthsnwspthsnon  29850  clwlkclwwlklem2a1  29925  clwlkclwwlklem2a4  29930  clwlkclwwlklem2a  29931  clwlkclwwlklem2  29933  clwlkclwwlklem3  29934  wwlksext2clwwlk  29990  clwwlknonex2lem2  30041  eucrctshift  30176  eucrct2eupth  30178  numclwwlk2lem1lem  30275  numclwwlk1  30294  numclwwlk7  30324  ipasslem1  30764  ipasslem2  30765  dpfrac1  32753  archirngz  33054  pthhashvtx  34955  subfacval2  35015  bccolsum  35561  faclimlem1  35565  poimirlem28  37349  heiborlem4  37515  heiborlem6  37517  lcmineqlem3  41730  facp2  41841  sticksstones7  41850  fac2xp3  41925  factwoffsmonot  41928  oddnumth  42110  nicomachus  42111  sumcubes  42112  pell14qrgt0  42516  pell14qrdich  42526  pell1qrge1  42527  2nn0ind  42603  jm2.17a  42618  jm2.18  42646  jm2.19lem3  42649  proot1ex  42861  bcc0  44014  dvradcnv2  44021  binomcxplemrat  44024  binomcxplemnotnn0  44030  fperiodmullem  44918  stoweidlem10  45631  stoweidlem17  45638  stoweidlem26  45647  stirlinglem5  45699  stirlinglem7  45701  etransclem23  45878  subsubelfzo0  46939  fargshiftfo  47014  fmtnodvds  47116  goldbachthlem1  47117  fmtnofac2lem  47140  fmtnofac1  47142  nn0onn0exALTV  47271  nn0enn0exALTV  47272  nn0mnd  47556  ply1mulgsumlem1  47769  ply1mulgsumlem2  47770  nn0onn0ex  47911  nn0enn0ex  47912  fllog2  47956  dignn0fr  47989  digexp  47995  0dig2nn0e  48000  0dig2nn0o  48001  dignn0ehalf  48005  nn0mulfsum  48012  nn0mullong  48013  itcovalpclem1  48058  itcovalpclem2  48059  itcovalt2lem2lem2  48062  ackval1  48069  ackval2  48070  ackval3  48071