Theorem nn0cn 12538

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

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

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-mulcl 11186  ax-i2m1 11192

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-nn 12258  df-n0 12529

This theorem is used by:  nn0nnaddcl  12559  elnn0nn  12570  nn0sub  12578  difgtsumgt  12581  nn0le2x  12582  nn0n0n1ge2  12596  uzaddcl  12953  fzctr  13695  nn0split  13698  elfzoext  13778  zpnn0elfzo1  13795  ubmelm1fzo  13819  subfzo0  13849  quoremnn0ALT  13918  modmuladdnn0  13979  addmodidr  13984  modfzo0difsn  14007  nn0ennn  14043  expadd  14168  expmul  14171  bernneq  14293  bernneq2  14294  faclbnd  14354  faclbnd4lem3  14359  faclbnd4lem4  14360  faclbnd6  14363  bccmpl  14373  bcn0  14374  bcnn  14376  bcnp1n  14378  bcn2  14383  bcp1m1  14384  bcpasc  14385  bcn2p1  14389  hashfzo0  14495  hashfz0  14497  hashxplem  14498  hashdifsnp1  14571  ccatalpha  14660  ccatws1lenp1b  14689  ccatw2s1len  14693  swrdfv2  14731  swrdspsleq  14735  swrdlsw  14737  pfxmpt  14748  pfxswrd  14775  wrdind  14791  wrd2ind  14792  pfxccatin12lem4  14795  pfxccatin12lem1  14797  pfxccatin12lem2  14800  pfxccatin12  14802  swrdccat3blem  14808  repswswrd  14855  repswrevw  14858  cshwidxmodr  14875  2cshw  14884  2cshwcshw  14896  cshwcshid  14898  swrds2  15011  swrd2lsw  15025  iseraltlem2  15770  fsum0diag2  15869  hashiun  15909  ackbijnn  15917  binom1dif  15922  bcxmas  15924  geolim  15959  geomulcvg  15965  risefacval2  16097  fallfacval2  16098  risefaccl  16102  fallfaccl  16103  fallrisefac  16112  risefacp1  16115  fallfacp1  16116  fallfacfac  16131  bpolysum  16139  fsumkthpow  16142  bpoly4  16145  fsumcube  16146  efaddlem  16179  efexp  16189  eftlub  16197  demoivreALT  16289  nn0ob  16474  divalglem4  16486  modremain  16498  mulgcdr  16640  nn0rppwr  16651  nn0seqcvgd  16660  modprmn0modprm0  16899  coprimeprodsq  16900  coprimeprodsq2  16901  pcexp  16951  dvdsprmpweqle  16978  difsqpwdvds  16979  ramub1lem1  17118  prmop1  17130  chnccat  18714  smndex2dlinvh  19029  mulgneg2  19231  mndodcongi  19670  oddvdsnn0  19671  sylow1lem1  19725  efgsrel  19861  fincygsubgodd  20241  srgbinomlem4  20368  cnfldmulg  21617  nn0subm  21635  nn0srg  21650  psrbagconf1o  22144  psrass1lem  22148  psrlidm  22176  psrass1  22178  psrcom  22182  mplsubrglem  22218  mplmonmul  22252  psdmul  22394  psdmvr  22397  psropprmul  22462  coe1sclmul  22508  coe1sclmul2  22510  dvnadd  26156  ply1divex  26362  elqaalem2  26552  geolim3  26575  dvradcnv  26657  pserdv2  26666  logtayllem  26896  logtayl  26897  cxpmul2  26926  atantayl3  27176  leibpilem2  27178  leibpi  27179  log2cnv  27181  dmgmaddn0  27259  chpp1  27391  0sgmppw  27434  logexprlim  27461  dchrhash  27507  bcctr  27511  bcmono  27513  bcmax  27514  bcp1ctr  27515  2lgslem1c  27629  2lgslem3a  27632  2lgslem3b  27633  2lgslem3c  27634  2lgslem3d  27635  2lgslem3a1  27636  2lgslem3b1  27637  2lgslem3c1  27638  2lgslem3d1  27639  2sqreultlem  27683  2sqreulem2  27688  dchrisumlem1  27725  ostth2lem2  27870  wlklenvclwlk  30113  pthhashvtx  30194  upgrwlkdvdelem  30201  wwlknp  30311  wwlknlsw  30315  wlkiswwlks1  30335  wlklnwwlkln2lem  30350  wlknwwlksnbij  30356  wwlksnred  30360  wwlksnext  30361  wwlksnredwwlkn  30363  wwlksnextwrd  30365  wwlksnextinj  30367  wwlksnextproplem2  30378  wwlksnextproplem3  30379  wspthsnwspthsnon  30384  clwlkclwwlklem2a1  30462  clwlkclwwlklem2a4  30467  clwlkclwwlklem2a  30468  clwlkclwwlklem2  30470  clwlkclwwlklem3  30471  wwlksext2clwwlk  30527  clwwlknonex2lem2  30578  eucrctshift  30723  eucrct2eupth  30725  numclwwlk2lem1lem  30822  numclwwlk1  30841  numclwwlk7  30871  ipasslem1  31312  ipasslem2  31313  dpfrac1  33337  archirngz  33629  psrmonmul  34060  nn0constr  34271  subfacval2  35766  bccolsum  36318  faclimlem1  36322  poimirlem28  38397  heiborlem4  38564  heiborlem6  38566  lcmineqlem3  42897  facp2  43009  sticksstones7  43018  oddnumth  43186  nicomachus  43187  sumcubes  43188  pell14qrgt0  43700  pell14qrdich  43710  pell1qrge1  43711  2nn0ind  43786  jm2.17a  43801  jm2.18  43829  jm2.19lem3  43832  proot1ex  44037  bcc0  45164  dvradcnv2  45171  binomcxplemrat  45174  binomcxplemnotnn0  45180  fperiodmullem  46136  stoweidlem10  46838  stoweidlem17  46845  stoweidlem26  46854  stirlinglem5  46906  stirlinglem7  46908  etransclem23  47085  cjnpoly  47757  subsubelfzo0  48215  fargshiftfo  48342  fmtnodvds  48447  goldbachthlem1  48448  fmtnofac2lem  48471  fmtnofac1  48473  nn0onn0exALTV  48615  nn0enn0exALTV  48616  isubgr3stgrlem2  48883  nn0mnd  49094  ply1mulgsumlem1  49316  ply1mulgsumlem2  49317  nn0onn0ex  49453  nn0enn0ex  49454  fllog2  49498  dignn0fr  49531  digexp  49537  0dig2nn0e  49542  0dig2nn0o  49543  dignn0ehalf  49547  nn0mulfsum  49554  nn0mullong  49555  itcovalpclem1  49600  itcovalpclem2  49601  itcovalt2lem2lem2  49604  ackval1  49611  ackval2  49612  ackval3  49613