Theorem nn0cn 12391

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 11004  ℕ₀cn0 12381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-i2m1 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12126  df-n0 12382

This theorem is referenced by:  nn0nnaddcl  12412  elnn0nn  12423  nn0sub  12431  difgtsumgt  12434  nn0le2x  12435  nn0n0n1ge2  12449  uzaddcl  12802  fzctr  13540  nn0split  13543  elfzoext  13622  zpnn0elfzo1  13639  ubmelm1fzo  13663  subfzo0  13692  quoremnn0ALT  13761  modmuladdnn0  13822  addmodidr  13827  modfzo0difsn  13850  nn0ennn  13886  expadd  14011  expmul  14014  bernneq  14136  bernneq2  14137  faclbnd  14197  faclbnd4lem3  14202  faclbnd4lem4  14203  faclbnd6  14206  bccmpl  14216  bcn0  14217  bcnn  14219  bcnp1n  14221  bcn2  14226  bcp1m1  14227  bcpasc  14228  bcn2p1  14232  hashfzo0  14337  hashfz0  14339  hashxplem  14340  hashdifsnp1  14413  ccatalpha  14501  ccatws1lenp1b  14529  ccatw2s1len  14533  swrdfv2  14569  swrdspsleq  14573  swrdlsw  14575  pfxmpt  14586  pfxswrd  14613  wrdind  14629  wrd2ind  14630  pfxccatin12lem4  14633  pfxccatin12lem1  14635  pfxccatin12lem2  14638  pfxccatin12  14640  swrdccat3blem  14646  repswswrd  14691  repswrevw  14694  cshwidxmodr  14711  2cshw  14720  2cshwcshw  14732  cshwcshid  14734  swrds2  14847  swrd2lsw  14859  iseraltlem2  15590  fsum0diag2  15690  hashiun  15729  ackbijnn  15735  binom1dif  15740  bcxmas  15742  geolim  15777  geomulcvg  15783  risefacval2  15917  fallfacval2  15918  risefaccl  15922  fallfaccl  15923  fallrisefac  15932  risefacp1  15936  fallfacp1  15937  fallfacfac  15952  bpolysum  15960  fsumkthpow  15963  bpoly4  15966  fsumcube  15967  efaddlem  16000  efexp  16010  eftlub  16018  demoivreALT  16110  nn0ob  16295  divalglem4  16307  modremain  16319  mulgcdr  16461  nn0rppwr  16472  nn0seqcvgd  16481  modprmn0modprm0  16719  coprimeprodsq  16720  coprimeprodsq2  16721  pcexp  16771  dvdsprmpweqle  16798  difsqpwdvds  16799  ramub1lem1  16938  prmop1  16950  chnccat  18532  smndex2dlinvh  18825  mulgneg2  19021  mndodcongi  19455  oddvdsnn0  19456  sylow1lem1  19510  efgsrel  19646  fincygsubgodd  20026  srgbinomlem4  20147  cnfldmulg  21340  nn0subm  21359  nn0srg  21374  psrbagconf1o  21866  psrass1lem  21869  psrlidm  21899  psrass1  21901  psrcom  21905  mplsubrglem  21941  mplmonmul  21971  psdmul  22081  psdmvr  22084  psropprmul  22150  coe1sclmul  22196  coe1sclmul2  22198  dvnadd  25858  ply1divex  26069  elqaalem2  26255  geolim3  26274  dvradcnv  26357  pserdv2  26367  logtayllem  26595  logtayl  26596  cxpmul2  26625  atantayl3  26876  leibpilem2  26878  leibpi  26879  log2cnv  26881  dmgmaddn0  26960  chpp1  27092  0sgmppw  27136  logexprlim  27163  dchrhash  27209  bcctr  27213  bcmono  27215  bcmax  27216  bcp1ctr  27217  2lgslem1c  27331  2lgslem3a  27334  2lgslem3b  27335  2lgslem3c  27336  2lgslem3d  27337  2lgslem3a1  27338  2lgslem3b1  27339  2lgslem3c1  27340  2lgslem3d1  27341  2sqreultlem  27385  2sqreulem2  27390  dchrisumlem1  27427  ostth2lem2  27572  wlklenvclwlk  29632  upgrwlkdvdelem  29714  wwlknp  29821  wwlknlsw  29825  wlkiswwlks1  29845  wlklnwwlkln2lem  29860  wlknwwlksnbij  29866  wwlksnred  29870  wwlksnext  29871  wwlksnredwwlkn  29873  wwlksnextwrd  29875  wwlksnextinj  29877  wwlksnextproplem2  29888  wwlksnextproplem3  29889  wspthsnwspthsnon  29894  clwlkclwwlklem2a1  29972  clwlkclwwlklem2a4  29977  clwlkclwwlklem2a  29978  clwlkclwwlklem2  29980  clwlkclwwlklem3  29981  wwlksext2clwwlk  30037  clwwlknonex2lem2  30088  eucrctshift  30223  eucrct2eupth  30225  numclwwlk2lem1lem  30322  numclwwlk1  30341  numclwwlk7  30371  ipasslem1  30811  ipasslem2  30812  dpfrac1  32872  archirngz  33158  nn0constr  33774  pthhashvtx  35172  subfacval2  35231  bccolsum  35783  faclimlem1  35787  poimirlem28  37696  heiborlem4  37862  heiborlem6  37864  lcmineqlem3  42072  facp2  42184  sticksstones7  42193  oddnumth  42352  nicomachus  42353  sumcubes  42354  pell14qrgt0  42900  pell14qrdich  42910  pell1qrge1  42911  2nn0ind  42986  jm2.17a  43001  jm2.18  43029  jm2.19lem3  43032  proot1ex  43237  bcc0  44381  dvradcnv2  44388  binomcxplemrat  44391  binomcxplemnotnn0  44397  fperiodmullem  45352  stoweidlem10  46056  stoweidlem17  46063  stoweidlem26  46072  stirlinglem5  46124  stirlinglem7  46126  etransclem23  46303  cjnpoly  46928  subsubelfzo0  47365  fargshiftfo  47481  fmtnodvds  47583  goldbachthlem1  47584  fmtnofac2lem  47607  fmtnofac1  47609  nn0onn0exALTV  47738  nn0enn0exALTV  47739  isubgr3stgrlem2  48006  nn0mnd  48218  ply1mulgsumlem1  48426  ply1mulgsumlem2  48427  nn0onn0ex  48563  nn0enn0ex  48564  fllog2  48608  dignn0fr  48641  digexp  48647  0dig2nn0e  48652  0dig2nn0o  48653  dignn0ehalf  48657  nn0mulfsum  48664  nn0mullong  48665  itcovalpclem1  48710  itcovalpclem2  48711  itcovalt2lem2lem2  48714  ackval1  48721  ackval2  48722  ackval3  48723