Theorem nn0cn 12609

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

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

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 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-mulcl 11255  ax-i2m1 11261

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  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 7421  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-nn 12329  df-n0 12600

This theorem is used by:  nn0nnaddcl  12630  elnn0nn  12641  nn0sub  12649  difgtsumgt  12652  nn0le2x  12653  nn0n0n1ge2  12667  uzaddcl  13024  fzctr  13767  nn0split  13770  elfzoext  13850  zpnn0elfzo1  13867  ubmelm1fzo  13891  subfzo0  13921  quoremnn0ALT  13990  modmuladdnn0  14051  addmodidr  14056  modfzo0difsn  14079  nn0ennn  14115  expadd  14240  expmul  14243  bernneq  14366  bernneq2  14367  faclbnd  14427  faclbnd4lem3  14432  faclbnd4lem4  14433  faclbnd6  14436  bccmpl  14446  bcn0  14447  bcnn  14449  bcnp1n  14451  bcn2  14456  bcp1m1  14457  bcpasc  14458  bcn2p1  14462  hashfzo0  14568  hashfz0  14570  hashxplem  14571  hashdifsnp1  14644  ccatalpha  14733  ccatws1lenp1b  14762  ccatw2s1len  14766  swrdfv2  14804  swrdspsleq  14808  swrdlsw  14810  pfxmpt  14821  pfxswrd  14848  wrdind  14864  wrd2ind  14865  pfxccatin12lem4  14868  pfxccatin12lem1  14870  pfxccatin12lem2  14873  pfxccatin12  14875  swrdccat3blem  14881  repswswrd  14928  repswrevw  14931  cshwidxmodr  14948  2cshw  14957  2cshwcshw  14969  cshwcshid  14971  swrds2  15084  swrd2lsw  15098  iseraltlem2  15843  fsum0diag2  15942  hashiun  15982  ackbijnn  15990  binom1dif  15995  bcxmas  15997  geolim  16032  geomulcvg  16038  risefacval2  16170  fallfacval2  16171  risefaccl  16175  fallfaccl  16176  fallrisefac  16185  risefacp1  16188  fallfacp1  16189  fallfacfac  16204  bpolysum  16212  fsumkthpow  16215  bpoly4  16218  fsumcube  16219  efaddlem  16252  efexp  16262  eftlub  16270  demoivreALT  16362  nn0ob  16547  divalglem4  16559  modremain  16571  mulgcdr  16716  nn0rppwr  16728  nn0seqcvgd  16738  modprmn0modprm0  16978  coprimeprodsq  16979  coprimeprodsq2  16980  pcexp  17030  dvdsprmpweqle  17057  difsqpwdvds  17058  ramub1lem1  17197  prmop1  17209  chnccat  18793  smndex2dlinvh  19109  mulgneg2  19311  mndodcongi  19750  oddvdsnn0  19751  sylow1lem1  19805  efgsrel  19941  fincygsubgodd  20321  srgbinomlem4  20448  cnfldmulg  21703  nn0subm  21721  nn0srg  21736  psrbagconf1o  22230  psrass1lem  22234  psrlidm  22262  psrass1  22264  psrcom  22268  mplsubrglem  22304  mplmonmul  22338  psdmul  22480  psdmvr  22483  psropprmul  22548  coe1sclmul  22594  coe1sclmul2  22596  dvnadd  26242  ply1divex  26448  elqaalem2  26636  geolim3  26659  dvradcnv  26741  pserdv2  26750  logtayllem  26980  logtayl  26981  cxpmul2  27010  atantayl3  27260  leibpilem2  27262  leibpi  27263  log2cnv  27265  dmgmaddn0  27343  chpp1  27475  0sgmppw  27518  logexprlim  27545  dchrhash  27591  bcctr  27595  bcmono  27597  bcmax  27598  bcp1ctr  27599  2lgslem1c  27713  2lgslem3a  27716  2lgslem3b  27717  2lgslem3c  27718  2lgslem3d  27719  2lgslem3a1  27720  2lgslem3b1  27721  2lgslem3c1  27722  2lgslem3d1  27723  2sqreultlem  27767  2sqreulem2  27772  dchrisumlem1  27809  ostth2lem2  27954  wlklenvclwlk  30227  pthhashvtx  30308  upgrwlkdvdelem  30315  wwlknp  30425  wwlknlsw  30429  wlkiswwlks1  30449  wlklnwwlkln2lem  30464  wlknwwlksnbij  30470  wwlksnred  30474  wwlksnext  30475  wwlksnredwwlkn  30477  wwlksnextwrd  30479  wwlksnextinj  30481  wwlksnextproplem2  30492  wwlksnextproplem3  30493  wspthsnwspthsnon  30498  clwlkclwwlklem2a1  30576  clwlkclwwlklem2a4  30581  clwlkclwwlklem2a  30582  clwlkclwwlklem2  30584  clwlkclwwlklem3  30585  wwlksext2clwwlk  30641  clwwlknonex2lem2  30692  eucrctshift  30837  eucrct2eupth  30839  numclwwlk2lem1lem  30936  numclwwlk1  30955  numclwwlk7  30985  ipasslem1  31426  ipasslem2  31427  dpfrac1  33451  archirngz  33743  psrmonmul  34175  nn0constr  34386  subfacval2  35931  bccolsum  36483  faclimlem1  36487  poimirlem28  38546  heiborlem4  38728  heiborlem6  38730  lcmineqlem3  43061  facp2  43173  sticksstones7  43182  oddnumth  43348  nicomachus  43349  sumcubes  43350  pell14qrgt0  43845  pell14qrdich  43855  pell1qrge1  43856  2nn0ind  43931  jm2.17a  43946  jm2.18  43974  jm2.19lem3  43977  proot1ex  44182  bcc0  45309  dvradcnv2  45316  binomcxplemrat  45319  binomcxplemnotnn0  45325  fperiodmullem  46288  stoweidlem10  46989  stoweidlem17  46996  stoweidlem26  47005  stirlinglem5  47057  stirlinglem7  47059  etransclem23  47236  cjnpoly  47908  subsubelfzo0  48366  fargshiftfo  48493  fmtnodvds  48598  goldbachthlem1  48599  fmtnofac2lem  48622  fmtnofac1  48624  nn0onn0exALTV  48766  nn0enn0exALTV  48767  isubgr3stgrlem2  49034  nn0mnd  49245  ply1mulgsumlem1  49467  ply1mulgsumlem2  49468  nn0onn0ex  49604  nn0enn0ex  49605  fllog2  49649  dignn0fr  49682  digexp  49688  0dig2nn0e  49693  0dig2nn0o  49694  dignn0ehalf  49698  nn0mulfsum  49705  nn0mullong  49706  itcovalpclem1  49751  itcovalpclem2  49752  itcovalt2lem2lem2  49755  ackval1  49762  ackval2  49763  ackval3  49764