Theorem nn0cn 12536

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  ℕ₀cn0 12526

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-i2m1 11223

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267  df-n0 12527

This theorem is referenced by:  nn0nnaddcl  12557  elnn0nn  12568  nn0sub  12576  difgtsumgt  12579  nn0le2x  12580  nn0n0n1ge2  12594  uzaddcl  12946  fzctr  13680  nn0split  13683  elfzoext  13761  zpnn0elfzo1  13778  ubmelm1fzo  13802  subfzo0  13828  quoremnn0ALT  13897  modmuladdnn0  13956  addmodidr  13961  modfzo0difsn  13984  nn0ennn  14020  expadd  14145  expmul  14148  bernneq  14268  bernneq2  14269  faclbnd  14329  faclbnd4lem3  14334  faclbnd4lem4  14335  faclbnd6  14338  bccmpl  14348  bcn0  14349  bcnn  14351  bcnp1n  14353  bcn2  14358  bcp1m1  14359  bcpasc  14360  bcn2p1  14364  hashfzo0  14469  hashfz0  14471  hashxplem  14472  hashdifsnp1  14545  ccatalpha  14631  ccatws1lenp1b  14659  ccatw2s1len  14663  swrdfv2  14699  swrdspsleq  14703  swrdlsw  14705  pfxmpt  14716  addlenrevpfx  14728  pfxswrd  14744  wrdind  14760  wrd2ind  14761  pfxccatin12lem4  14764  pfxccatin12lem1  14766  pfxccatin12lem2  14769  pfxccatin12  14771  swrdccat3blem  14777  repswswrd  14822  repswrevw  14825  cshwidxmodr  14842  2cshw  14851  2cshwcshw  14864  cshwcshid  14866  swrds2  14979  swrd2lsw  14991  iseraltlem2  15719  fsum0diag2  15819  hashiun  15858  ackbijnn  15864  binom1dif  15869  bcxmas  15871  geolim  15906  geomulcvg  15912  risefacval2  16046  fallfacval2  16047  risefaccl  16051  fallfaccl  16052  fallrisefac  16061  risefacp1  16065  fallfacp1  16066  fallfacfac  16081  bpolysum  16089  fsumkthpow  16092  bpoly4  16095  fsumcube  16096  efaddlem  16129  efexp  16137  eftlub  16145  demoivreALT  16237  nn0ob  16421  divalglem4  16433  modremain  16445  mulgcdr  16587  nn0rppwr  16598  nn0seqcvgd  16607  modprmn0modprm0  16845  coprimeprodsq  16846  coprimeprodsq2  16847  pcexp  16897  dvdsprmpweqle  16924  difsqpwdvds  16925  ramub1lem1  17064  prmop1  17076  smndex2dlinvh  18930  mulgneg2  19126  mndodcongi  19561  oddvdsnn0  19562  sylow1lem1  19616  efgsrel  19752  fincygsubgodd  20132  srgbinomlem4  20226  cnfldmulg  21416  nn0subm  21440  nn0srg  21455  psrbagconf1o  21949  psrass1lem  21952  psrlidm  21982  psrass1  21984  psrcom  21988  mplsubrglem  22024  mplmonmul  22054  psdmul  22170  psdmvr  22173  psropprmul  22239  coe1sclmul  22285  coe1sclmul2  22287  dvnadd  25965  ply1divex  26176  elqaalem2  26362  geolim3  26381  dvradcnv  26464  pserdv2  26474  logtayllem  26701  logtayl  26702  cxpmul2  26731  atantayl3  26982  leibpilem2  26984  leibpi  26985  log2cnv  26987  dmgmaddn0  27066  chpp1  27198  0sgmppw  27242  logexprlim  27269  dchrhash  27315  bcctr  27319  bcmono  27321  bcmax  27322  bcp1ctr  27323  2lgslem1c  27437  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2lgslem3a1  27444  2lgslem3b1  27445  2lgslem3c1  27446  2lgslem3d1  27447  2sqreultlem  27491  2sqreulem2  27496  dchrisumlem1  27533  ostth2lem2  27678  wlklenvclwlk  29673  upgrwlkdvdelem  29756  wwlknp  29863  wwlknlsw  29867  wlkiswwlks1  29887  wlklnwwlkln2lem  29902  wlknwwlksnbij  29908  wwlksnred  29912  wwlksnext  29913  wwlksnredwwlkn  29915  wwlksnextwrd  29917  wwlksnextinj  29919  wwlksnextproplem2  29930  wwlksnextproplem3  29931  wspthsnwspthsnon  29936  clwlkclwwlklem2a1  30011  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwlkclwwlklem3  30020  wwlksext2clwwlk  30076  clwwlknonex2lem2  30127  eucrctshift  30262  eucrct2eupth  30264  numclwwlk2lem1lem  30361  numclwwlk1  30380  numclwwlk7  30410  ipasslem1  30850  ipasslem2  30851  dpfrac1  32874  archirngz  33196  pthhashvtx  35133  subfacval2  35192  bccolsum  35739  faclimlem1  35743  poimirlem28  37655  heiborlem4  37821  heiborlem6  37823  lcmineqlem3  42032  facp2  42144  sticksstones7  42153  fac2xp3  42240  factwoffsmonot  42243  oddnumth  42345  nicomachus  42346  sumcubes  42347  pell14qrgt0  42870  pell14qrdich  42880  pell1qrge1  42881  2nn0ind  42957  jm2.17a  42972  jm2.18  43000  jm2.19lem3  43003  proot1ex  43208  bcc0  44359  dvradcnv2  44366  binomcxplemrat  44369  binomcxplemnotnn0  44375  fperiodmullem  45315  stoweidlem10  46025  stoweidlem17  46032  stoweidlem26  46041  stirlinglem5  46093  stirlinglem7  46095  etransclem23  46272  subsubelfzo0  47338  fargshiftfo  47429  fmtnodvds  47531  goldbachthlem1  47532  fmtnofac2lem  47555  fmtnofac1  47557  nn0onn0exALTV  47686  nn0enn0exALTV  47687  isubgr3stgrlem2  47934  nn0mnd  48095  ply1mulgsumlem1  48303  ply1mulgsumlem2  48304  nn0onn0ex  48444  nn0enn0ex  48445  fllog2  48489  dignn0fr  48522  digexp  48528  0dig2nn0e  48533  0dig2nn0o  48534  dignn0ehalf  48538  nn0mulfsum  48545  nn0mullong  48546  itcovalpclem1  48591  itcovalpclem2  48592  itcovalt2lem2lem2  48595  ackval1  48602  ackval2  48603  ackval3  48604