Theorem nn0cn 12452

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  ℕ₀cn0 12442

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-i2m1 11136

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-n0 12443

This theorem is referenced by:  nn0nnaddcl  12473  elnn0nn  12484  nn0sub  12492  difgtsumgt  12495  nn0le2x  12496  nn0n0n1ge2  12510  uzaddcl  12863  fzctr  13601  nn0split  13604  elfzoext  13683  zpnn0elfzo1  13700  ubmelm1fzo  13724  subfzo0  13750  quoremnn0ALT  13819  modmuladdnn0  13880  addmodidr  13885  modfzo0difsn  13908  nn0ennn  13944  expadd  14069  expmul  14072  bernneq  14194  bernneq2  14195  faclbnd  14255  faclbnd4lem3  14260  faclbnd4lem4  14261  faclbnd6  14264  bccmpl  14274  bcn0  14275  bcnn  14277  bcnp1n  14279  bcn2  14284  bcp1m1  14285  bcpasc  14286  bcn2p1  14290  hashfzo0  14395  hashfz0  14397  hashxplem  14398  hashdifsnp1  14471  ccatalpha  14558  ccatws1lenp1b  14586  ccatw2s1len  14590  swrdfv2  14626  swrdspsleq  14630  swrdlsw  14632  pfxmpt  14643  addlenrevpfx  14655  pfxswrd  14671  wrdind  14687  wrd2ind  14688  pfxccatin12lem4  14691  pfxccatin12lem1  14693  pfxccatin12lem2  14696  pfxccatin12  14698  swrdccat3blem  14704  repswswrd  14749  repswrevw  14752  cshwidxmodr  14769  2cshw  14778  2cshwcshw  14791  cshwcshid  14793  swrds2  14906  swrd2lsw  14918  iseraltlem2  15649  fsum0diag2  15749  hashiun  15788  ackbijnn  15794  binom1dif  15799  bcxmas  15801  geolim  15836  geomulcvg  15842  risefacval2  15976  fallfacval2  15977  risefaccl  15981  fallfaccl  15982  fallrisefac  15991  risefacp1  15995  fallfacp1  15996  fallfacfac  16011  bpolysum  16019  fsumkthpow  16022  bpoly4  16025  fsumcube  16026  efaddlem  16059  efexp  16069  eftlub  16077  demoivreALT  16169  nn0ob  16354  divalglem4  16366  modremain  16378  mulgcdr  16520  nn0rppwr  16531  nn0seqcvgd  16540  modprmn0modprm0  16778  coprimeprodsq  16779  coprimeprodsq2  16780  pcexp  16830  dvdsprmpweqle  16857  difsqpwdvds  16858  ramub1lem1  16997  prmop1  17009  smndex2dlinvh  18844  mulgneg2  19040  mndodcongi  19473  oddvdsnn0  19474  sylow1lem1  19528  efgsrel  19664  fincygsubgodd  20044  srgbinomlem4  20138  cnfldmulg  21315  nn0subm  21339  nn0srg  21354  psrbagconf1o  21838  psrass1lem  21841  psrlidm  21871  psrass1  21873  psrcom  21877  mplsubrglem  21913  mplmonmul  21943  psdmul  22053  psdmvr  22056  psropprmul  22122  coe1sclmul  22168  coe1sclmul2  22170  dvnadd  25831  ply1divex  26042  elqaalem2  26228  geolim3  26247  dvradcnv  26330  pserdv2  26340  logtayllem  26568  logtayl  26569  cxpmul2  26598  atantayl3  26849  leibpilem2  26851  leibpi  26852  log2cnv  26854  dmgmaddn0  26933  chpp1  27065  0sgmppw  27109  logexprlim  27136  dchrhash  27182  bcctr  27186  bcmono  27188  bcmax  27189  bcp1ctr  27190  2lgslem1c  27304  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgslem3a1  27311  2lgslem3b1  27312  2lgslem3c1  27313  2lgslem3d1  27314  2sqreultlem  27358  2sqreulem2  27363  dchrisumlem1  27400  ostth2lem2  27545  wlklenvclwlk  29583  upgrwlkdvdelem  29666  wwlknp  29773  wwlknlsw  29777  wlkiswwlks1  29797  wlklnwwlkln2lem  29812  wlknwwlksnbij  29818  wwlksnred  29822  wwlksnext  29823  wwlksnredwwlkn  29825  wwlksnextwrd  29827  wwlksnextinj  29829  wwlksnextproplem2  29840  wwlksnextproplem3  29841  wspthsnwspthsnon  29846  clwlkclwwlklem2a1  29921  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwlkclwwlklem3  29930  wwlksext2clwwlk  29986  clwwlknonex2lem2  30037  eucrctshift  30172  eucrct2eupth  30174  numclwwlk2lem1lem  30271  numclwwlk1  30290  numclwwlk7  30320  ipasslem1  30760  ipasslem2  30761  dpfrac1  32812  archirngz  33143  nn0constr  33751  pthhashvtx  35115  subfacval2  35174  bccolsum  35726  faclimlem1  35730  poimirlem28  37642  heiborlem4  37808  heiborlem6  37810  lcmineqlem3  42019  facp2  42131  sticksstones7  42140  oddnumth  42299  nicomachus  42300  sumcubes  42301  pell14qrgt0  42847  pell14qrdich  42857  pell1qrge1  42858  2nn0ind  42934  jm2.17a  42949  jm2.18  42977  jm2.19lem3  42980  proot1ex  43185  bcc0  44329  dvradcnv2  44336  binomcxplemrat  44339  binomcxplemnotnn0  44345  fperiodmullem  45301  stoweidlem10  46008  stoweidlem17  46015  stoweidlem26  46024  stirlinglem5  46076  stirlinglem7  46078  etransclem23  46255  cjnpoly  46890  subsubelfzo0  47327  fargshiftfo  47443  fmtnodvds  47545  goldbachthlem1  47546  fmtnofac2lem  47569  fmtnofac1  47571  nn0onn0exALTV  47700  nn0enn0exALTV  47701  isubgr3stgrlem2  47966  nn0mnd  48167  ply1mulgsumlem1  48375  ply1mulgsumlem2  48376  nn0onn0ex  48512  nn0enn0ex  48513  fllog2  48557  dignn0fr  48590  digexp  48596  0dig2nn0e  48601  0dig2nn0o  48602  dignn0ehalf  48606  nn0mulfsum  48613  nn0mullong  48614  itcovalpclem1  48659  itcovalpclem2  48660  itcovalt2lem2lem2  48663  ackval1  48670  ackval2  48671  ackval3  48672