Theorem nn0cn 12459

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  ℕ₀cn0 12449

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-i2m1 11143

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194  df-n0 12450

This theorem is referenced by:  nn0nnaddcl  12480  elnn0nn  12491  nn0sub  12499  difgtsumgt  12502  nn0le2x  12503  nn0n0n1ge2  12517  uzaddcl  12870  fzctr  13608  nn0split  13611  elfzoext  13690  zpnn0elfzo1  13707  ubmelm1fzo  13731  subfzo0  13757  quoremnn0ALT  13826  modmuladdnn0  13887  addmodidr  13892  modfzo0difsn  13915  nn0ennn  13951  expadd  14076  expmul  14079  bernneq  14201  bernneq2  14202  faclbnd  14262  faclbnd4lem3  14267  faclbnd4lem4  14268  faclbnd6  14271  bccmpl  14281  bcn0  14282  bcnn  14284  bcnp1n  14286  bcn2  14291  bcp1m1  14292  bcpasc  14293  bcn2p1  14297  hashfzo0  14402  hashfz0  14404  hashxplem  14405  hashdifsnp1  14478  ccatalpha  14565  ccatws1lenp1b  14593  ccatw2s1len  14597  swrdfv2  14633  swrdspsleq  14637  swrdlsw  14639  pfxmpt  14650  addlenrevpfx  14662  pfxswrd  14678  wrdind  14694  wrd2ind  14695  pfxccatin12lem4  14698  pfxccatin12lem1  14700  pfxccatin12lem2  14703  pfxccatin12  14705  swrdccat3blem  14711  repswswrd  14756  repswrevw  14759  cshwidxmodr  14776  2cshw  14785  2cshwcshw  14798  cshwcshid  14800  swrds2  14913  swrd2lsw  14925  iseraltlem2  15656  fsum0diag2  15756  hashiun  15795  ackbijnn  15801  binom1dif  15806  bcxmas  15808  geolim  15843  geomulcvg  15849  risefacval2  15983  fallfacval2  15984  risefaccl  15988  fallfaccl  15989  fallrisefac  15998  risefacp1  16002  fallfacp1  16003  fallfacfac  16018  bpolysum  16026  fsumkthpow  16029  bpoly4  16032  fsumcube  16033  efaddlem  16066  efexp  16076  eftlub  16084  demoivreALT  16176  nn0ob  16361  divalglem4  16373  modremain  16385  mulgcdr  16527  nn0rppwr  16538  nn0seqcvgd  16547  modprmn0modprm0  16785  coprimeprodsq  16786  coprimeprodsq2  16787  pcexp  16837  dvdsprmpweqle  16864  difsqpwdvds  16865  ramub1lem1  17004  prmop1  17016  smndex2dlinvh  18851  mulgneg2  19047  mndodcongi  19480  oddvdsnn0  19481  sylow1lem1  19535  efgsrel  19671  fincygsubgodd  20051  srgbinomlem4  20145  cnfldmulg  21322  nn0subm  21346  nn0srg  21361  psrbagconf1o  21845  psrass1lem  21848  psrlidm  21878  psrass1  21880  psrcom  21884  mplsubrglem  21920  mplmonmul  21950  psdmul  22060  psdmvr  22063  psropprmul  22129  coe1sclmul  22175  coe1sclmul2  22177  dvnadd  25838  ply1divex  26049  elqaalem2  26235  geolim3  26254  dvradcnv  26337  pserdv2  26347  logtayllem  26575  logtayl  26576  cxpmul2  26605  atantayl3  26856  leibpilem2  26858  leibpi  26859  log2cnv  26861  dmgmaddn0  26940  chpp1  27072  0sgmppw  27116  logexprlim  27143  dchrhash  27189  bcctr  27193  bcmono  27195  bcmax  27196  bcp1ctr  27197  2lgslem1c  27311  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgslem3a1  27318  2lgslem3b1  27319  2lgslem3c1  27320  2lgslem3d1  27321  2sqreultlem  27365  2sqreulem2  27370  dchrisumlem1  27407  ostth2lem2  27552  wlklenvclwlk  29590  upgrwlkdvdelem  29673  wwlknp  29780  wwlknlsw  29784  wlkiswwlks1  29804  wlklnwwlkln2lem  29819  wlknwwlksnbij  29825  wwlksnred  29829  wwlksnext  29830  wwlksnredwwlkn  29832  wwlksnextwrd  29834  wwlksnextinj  29836  wwlksnextproplem2  29847  wwlksnextproplem3  29848  wspthsnwspthsnon  29853  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlklem3  29937  wwlksext2clwwlk  29993  clwwlknonex2lem2  30044  eucrctshift  30179  eucrct2eupth  30181  numclwwlk2lem1lem  30278  numclwwlk1  30297  numclwwlk7  30327  ipasslem1  30767  ipasslem2  30768  dpfrac1  32819  archirngz  33150  nn0constr  33758  pthhashvtx  35122  subfacval2  35181  bccolsum  35733  faclimlem1  35737  poimirlem28  37649  heiborlem4  37815  heiborlem6  37817  lcmineqlem3  42026  facp2  42138  sticksstones7  42147  oddnumth  42306  nicomachus  42307  sumcubes  42308  pell14qrgt0  42854  pell14qrdich  42864  pell1qrge1  42865  2nn0ind  42941  jm2.17a  42956  jm2.18  42984  jm2.19lem3  42987  proot1ex  43192  bcc0  44336  dvradcnv2  44343  binomcxplemrat  44346  binomcxplemnotnn0  44352  fperiodmullem  45308  stoweidlem10  46015  stoweidlem17  46022  stoweidlem26  46031  stirlinglem5  46083  stirlinglem7  46085  etransclem23  46262  subsubelfzo0  47331  fargshiftfo  47447  fmtnodvds  47549  goldbachthlem1  47550  fmtnofac2lem  47573  fmtnofac1  47575  nn0onn0exALTV  47704  nn0enn0exALTV  47705  isubgr3stgrlem2  47970  nn0mnd  48171  ply1mulgsumlem1  48379  ply1mulgsumlem2  48380  nn0onn0ex  48516  nn0enn0ex  48517  fllog2  48561  dignn0fr  48594  digexp  48600  0dig2nn0e  48605  0dig2nn0o  48606  dignn0ehalf  48610  nn0mulfsum  48617  nn0mullong  48618  itcovalpclem1  48663  itcovalpclem2  48664  itcovalt2lem2lem2  48667  ackval1  48674  ackval2  48675  ackval3  48676