Theorem nn0cn 12542

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11126  ℕ₀cn0 12532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-mulcl 11190  ax-i2m1 11196

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-nn 12262  df-n0 12533

This theorem is used by:  nn0nnaddcl  12563  elnn0nn  12574  nn0sub  12582  difgtsumgt  12585  nn0le2x  12586  nn0n0n1ge2  12600  uzaddcl  12957  fzctr  13699  nn0split  13702  elfzoext  13782  zpnn0elfzo1  13799  ubmelm1fzo  13823  subfzo0  13853  quoremnn0ALT  13922  modmuladdnn0  13983  addmodidr  13988  modfzo0difsn  14011  nn0ennn  14047  expadd  14172  expmul  14175  bernneq  14297  bernneq2  14298  faclbnd  14358  faclbnd4lem3  14363  faclbnd4lem4  14364  faclbnd6  14367  bccmpl  14377  bcn0  14378  bcnn  14380  bcnp1n  14382  bcn2  14387  bcp1m1  14388  bcpasc  14389  bcn2p1  14393  hashfzo0  14499  hashfz0  14501  hashxplem  14502  hashdifsnp1  14575  ccatalpha  14664  ccatws1lenp1b  14693  ccatw2s1len  14697  swrdfv2  14735  swrdspsleq  14739  swrdlsw  14741  pfxmpt  14752  pfxswrd  14779  wrdind  14795  wrd2ind  14796  pfxccatin12lem4  14799  pfxccatin12lem1  14801  pfxccatin12lem2  14804  pfxccatin12  14806  swrdccat3blem  14812  repswswrd  14859  repswrevw  14862  cshwidxmodr  14879  2cshw  14888  2cshwcshw  14900  cshwcshid  14902  swrds2  15015  swrd2lsw  15029  iseraltlem2  15774  fsum0diag2  15873  hashiun  15913  ackbijnn  15921  binom1dif  15926  bcxmas  15928  geolim  15963  geomulcvg  15969  risefacval2  16103  fallfacval2  16104  risefaccl  16108  fallfaccl  16109  fallrisefac  16118  risefacp1  16121  fallfacp1  16122  fallfacfac  16137  bpolysum  16145  fsumkthpow  16148  bpoly4  16151  fsumcube  16152  efaddlem  16185  efexp  16195  eftlub  16203  demoivreALT  16295  nn0ob  16480  divalglem4  16492  modremain  16504  mulgcdr  16646  nn0rppwr  16657  nn0seqcvgd  16666  modprmn0modprm0  16905  coprimeprodsq  16906  coprimeprodsq2  16907  pcexp  16957  dvdsprmpweqle  16984  difsqpwdvds  16985  ramub1lem1  17124  prmop1  17136  chnccat  18720  smndex2dlinvh  19035  mulgneg2  19237  mndodcongi  19676  oddvdsnn0  19677  sylow1lem1  19731  efgsrel  19867  fincygsubgodd  20247  srgbinomlem4  20374  cnfldmulg  21623  nn0subm  21641  nn0srg  21656  psrbagconf1o  22150  psrass1lem  22154  psrlidm  22182  psrass1  22184  psrcom  22188  mplsubrglem  22224  mplmonmul  22258  psdmul  22400  psdmvr  22403  psropprmul  22468  coe1sclmul  22514  coe1sclmul2  22516  dvnadd  26163  ply1divex  26369  elqaalem2  26559  geolim3  26582  dvradcnv  26664  pserdv2  26673  logtayllem  26904  logtayl  26905  cxpmul2  26934  atantayl3  27184  leibpilem2  27186  leibpi  27187  log2cnv  27189  dmgmaddn0  27267  chpp1  27399  0sgmppw  27442  logexprlim  27469  dchrhash  27515  bcctr  27519  bcmono  27521  bcmax  27522  bcp1ctr  27523  2lgslem1c  27637  2lgslem3a  27640  2lgslem3b  27641  2lgslem3c  27642  2lgslem3d  27643  2lgslem3a1  27644  2lgslem3b1  27645  2lgslem3c1  27646  2lgslem3d1  27647  2sqreultlem  27691  2sqreulem2  27696  dchrisumlem1  27733  ostth2lem2  27878  wlklenvclwlk  30121  pthhashvtx  30202  upgrwlkdvdelem  30209  wwlknp  30319  wwlknlsw  30323  wlkiswwlks1  30343  wlklnwwlkln2lem  30358  wlknwwlksnbij  30364  wwlksnred  30368  wwlksnext  30369  wwlksnredwwlkn  30371  wwlksnextwrd  30373  wwlksnextinj  30375  wwlksnextproplem2  30386  wwlksnextproplem3  30387  wspthsnwspthsnon  30392  clwlkclwwlklem2a1  30470  clwlkclwwlklem2a4  30475  clwlkclwwlklem2a  30476  clwlkclwwlklem2  30478  clwlkclwwlklem3  30479  wwlksext2clwwlk  30535  clwwlknonex2lem2  30586  eucrctshift  30731  eucrct2eupth  30733  numclwwlk2lem1lem  30830  numclwwlk1  30849  numclwwlk7  30879  ipasslem1  31320  ipasslem2  31321  dpfrac1  33345  archirngz  33637  psrmonmul  34068  nn0constr  34279  subfacval2  35774  bccolsum  36326  faclimlem1  36330  poimirlem28  38405  heiborlem4  38572  heiborlem6  38574  lcmineqlem3  42905  facp2  43017  sticksstones7  43026  oddnumth  43194  nicomachus  43195  sumcubes  43196  pell14qrgt0  43708  pell14qrdich  43718  pell1qrge1  43719  2nn0ind  43794  jm2.17a  43809  jm2.18  43837  jm2.19lem3  43840  proot1ex  44045  bcc0  45172  dvradcnv2  45179  binomcxplemrat  45182  binomcxplemnotnn0  45188  fperiodmullem  46144  stoweidlem10  46846  stoweidlem17  46853  stoweidlem26  46862  stirlinglem5  46914  stirlinglem7  46916  etransclem23  47093  cjnpoly  47765  subsubelfzo0  48223  fargshiftfo  48350  fmtnodvds  48455  goldbachthlem1  48456  fmtnofac2lem  48479  fmtnofac1  48481  nn0onn0exALTV  48623  nn0enn0exALTV  48624  isubgr3stgrlem2  48891  nn0mnd  49102  ply1mulgsumlem1  49324  ply1mulgsumlem2  49325  nn0onn0ex  49461  nn0enn0ex  49462  fllog2  49506  dignn0fr  49539  digexp  49545  0dig2nn0e  49550  0dig2nn0o  49551  dignn0ehalf  49555  nn0mulfsum  49562  nn0mullong  49563  itcovalpclem1  49608  itcovalpclem2  49609  itcovalt2lem2lem2  49612  ackval1  49619  ackval2  49620  ackval3  49621