Theorem nn0cn 12623

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℂcc 11205  ℕ₀cn0 12613

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-mulcl 11269  ax-i2m1 11275

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  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 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7427  df-om 7882  df-2nd 8006  df-frecs 8306  df-wrecs 8337  df-recs 8386  df-rdg 8425  df-nn 12343  df-n0 12614

This theorem is used by:  nn0nnaddcl  12644  elnn0nn  12655  nn0sub  12663  difgtsumgt  12666  nn0le2x  12667  nn0n0n1ge2  12681  uzaddcl  13038  nn0split  13784  elfzoext  13864  zpnn0elfzo1  13881  ubmelm1fzo  13905  subfzo0  13935  quoremnn0ALT  14004  modmuladdnn0  14065  addmodidr  14070  modfzo0difsn  14093  nn0ennn  14129  expadd  14254  expmul  14257  bernneq  14380  bernneq2  14381  faclbnd  14441  faclbnd4lem3  14446  faclbnd4lem4  14447  faclbnd6  14450  bccmpl  14460  bcn0  14461  bcnn  14463  bcnp1n  14465  bcn2  14470  bcp1m1  14471  bcpasc  14472  bcn2p1  14476  hashfzo0  14582  hashfz0  14584  hashxplem  14585  hashdifsnp1  14658  ccatalpha  14747  ccatws1lenp1b  14777  ccatw2s1len  14781  swrdfv2  14819  swrdspsleq  14823  swrdlsw  14825  pfxmpt  14836  pfxswrd  14863  wrdind  14879  wrd2ind  14880  pfxccatin12lem4  14883  pfxccatin12lem1  14885  pfxccatin12lem2  14888  pfxccatin12  14890  swrdccat3blem  14896  repswswrd  14943  repswrevw  14946  cshwidxmodr  14963  2cshw  14972  2cshwcshw  14984  cshwcshid  14986  swrds2  15100  swrd2lsw  15114  iseraltlem2  15859  fsum0diag2  15958  hashiun  15998  ackbijnn  16006  binom1dif  16011  bcxmas  16013  geolim  16048  geomulcvg  16054  risefacval2  16186  fallfacval2  16187  risefaccl  16191  fallfaccl  16192  fallrisefac  16201  risefacp1  16204  fallfacp1  16205  fallfacfac  16220  bpolysum  16228  fsumkthpow  16231  bpoly4  16234  fsumcube  16235  efaddlem  16268  efexp  16278  eftlub  16286  demoivreALT  16378  nn0ob  16563  divalglem4  16575  modremain  16587  mulgcdr  16732  nn0rppwr  16744  nn0seqcvgd  16754  modprmn0modprm0  16994  coprimeprodsq  16995  coprimeprodsq2  16996  pcexp  17046  dvdsprmpweqle  17073  difsqpwdvds  17074  ramub1lem1  17213  prmop1  17225  chnccat  18809  smndex2dlinvh  19125  mulgneg2  19327  mndodcongi  19766  oddvdsnn0  19767  sylow1lem1  19821  efgsrel  19957  fincygsubgodd  20337  srgbinomlem4  20464  cnfldmulg  21719  nn0subm  21737  nn0srg  21752  psrbagconf1o  22246  psrass1lem  22250  psrlidm  22278  psrass1  22280  psrcom  22284  mplsubrglem  22320  mplmonmul  22354  psdmul  22496  psdmvr  22499  psropprmul  22564  coe1sclmul  22610  coe1sclmul2  22612  dvnadd  26258  ply1divex  26464  elqaalem2  26652  geolim3  26675  dvradcnv  26757  pserdv2  26766  logtayllem  26996  logtayl  26997  cxpmul2  27026  atantayl3  27276  leibpilem2  27278  leibpi  27279  log2cnv  27281  dmgmaddn0  27359  chpp1  27491  0sgmppw  27534  logexprlim  27561  dchrhash  27607  bcctr  27611  bcmono  27613  bcmax  27614  bcp1ctr  27615  2lgslem1c  27729  2lgslem3a  27732  2lgslem3b  27733  2lgslem3c  27734  2lgslem3d  27735  2lgslem3a1  27736  2lgslem3b1  27737  2lgslem3c1  27738  2lgslem3d1  27739  2sqreultlem  27783  2sqreulem2  27788  dchrisumlem1  27825  ostth2lem2  27970  wlklenvclwlk  30243  pthhashvtx  30324  upgrwlkdvdelem  30331  wwlknp  30441  wwlknlsw  30445  wlkiswwlks1  30465  wlklnwwlkln2lem  30480  wlknwwlksnbij  30486  wwlksnred  30490  wwlksnext  30491  wwlksnredwwlkn  30493  wwlksnextwrd  30495  wwlksnextinj  30497  wwlksnextproplem2  30508  wwlksnextproplem3  30509  wspthsnwspthsnon  30514  clwlkclwwlklem2a1  30592  clwlkclwwlklem2a4  30597  clwlkclwwlklem2a  30598  clwlkclwwlklem2  30600  clwlkclwwlklem3  30601  wwlksext2clwwlk  30657  clwwlknonex2lem2  30708  eucrctshift  30853  eucrct2eupth  30855  numclwwlk2lem1lem  30952  numclwwlk1  30971  numclwwlk7  31001  ipasslem1  31442  ipasslem2  31443  dpfrac1  33508  archirngz  33800  psrmonmul  34232  nn0constr  34443  subfacval2  36042  bccolsum  36600  faclimlem1  36604  poimirlem28  38675  heiborlem4  38857  heiborlem6  38859  lcmineqlem3  43190  facp2  43302  sticksstones7  43311  oddnumth  43477  nicomachus  43478  sumcubes  43479  pell14qrgt0  43975  pell14qrdich  43985  pell1qrge1  43986  2nn0ind  44061  jm2.17a  44076  jm2.18  44104  jm2.19lem3  44107  proot1ex  44307  bcc0  45433  dvradcnv2  45440  binomcxplemrat  45443  binomcxplemnotnn0  45449  fperiodmullem  46427  stoweidlem10  47128  stoweidlem17  47135  stoweidlem26  47144  stirlinglem5  47196  stirlinglem7  47198  etransclem23  47375  cjnpoly  48047  subsubelfzo0  48505  fargshiftfo  48632  fmtnodvds  48737  goldbachthlem1  48738  fmtnofac2lem  48761  fmtnofac1  48763  nn0onn0exALTV  48905  nn0enn0exALTV  48906  isubgr3stgrlem2  49173  nn0mnd  49384  ply1mulgsumlem1  49606  ply1mulgsumlem2  49607  nn0onn0ex  49743  nn0enn0ex  49744  fllog2  49788  dignn0fr  49821  digexp  49827  0dig2nn0e  49832  0dig2nn0o  49833  dignn0ehalf  49837  nn0mulfsum  49844  nn0mullong  49845  itcovalpclem1  49890  itcovalpclem2  49891  itcovalt2lem2lem2  49894  ackval1  49901  ackval2  49902  ackval3  49903