Theorem nn0cn 11563

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

Syntax hints:   → wi 4   ∈ wcel 2155  ℂcc 10213  ℕ₀cn0 11553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-i2m1 10283  ax-1ne0 10284  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-reu 3099  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-ov 6871  df-om 7290  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-nn 11300  df-n0 11554

This theorem is referenced by:  nn0nnaddcl  11584  elnn0nn  11595  nn0sub  11603  difgtsumgt  11606  nn0n0n1ge2  11618  uzaddcl  11956  fzctr  12669  nn0split  12672  elfzoext  12743  zpnn0elfzo1  12760  ubmelm1fzo  12782  subfzo0  12808  quoremnn0ALT  12874  modmuladdnn0  12932  addmodidr  12937  modfzo0difsn  12960  nn0ennn  12996  expadd  13119  expmul  13122  bernneq  13207  bernneq2  13208  faclbnd  13291  faclbnd4lem3  13296  faclbnd4lem4  13297  faclbnd6  13300  bccmpl  13310  bcn0  13311  bcnn  13313  bcnp1n  13315  bcn2  13320  bcp1m1  13321  bcpasc  13322  bcn2p1  13326  hashfzo0  13428  hashfz0  13430  hashxplem  13431  hashdifsnp1  13489  ccatalpha  13584  ccatws1lenp1b  13611  ccatw2s1len  13616  ccatw2s1lenOLD  13617  addlenrevswrd  13655  swrdfv2  13664  swrdspsleq  13667  swrdlsw  13670  swrd0swrd  13679  ccats1swrdeq  13687  wrdind  13694  wrd2ind  13695  swrdccatin12lem1  13702  swrdccatin12lem2b  13704  swrdccatin12lem2  13707  swrdccatin12  13709  swrdccat3blem  13713  repswswrd  13749  repswrevw  13751  cshwidxmodr  13768  2cshw  13777  2cshwcshw  13789  cshwcshid  13791  swrds2  13903  swrd2lsw  13914  iseraltlem2  14630  fsum0diag2  14731  hashiun  14770  ackbijnn  14776  binom1dif  14781  bcxmas  14783  geolim  14817  geomulcvg  14823  risefacval2  14955  fallfacval2  14956  risefaccl  14960  fallfaccl  14961  fallrisefac  14970  risefacp1  14974  fallfacp1  14975  fallfacfac  14990  bpolysum  14998  fsumkthpow  15001  bpoly4  15004  fsumcube  15005  efaddlem  15037  efexp  15045  eftlub  15053  demoivreALT  15145  nn0ob  15314  divalglem4  15333  modremain  15345  mulgcdr  15480  nn0seqcvgd  15496  modprmn0modprm0  15723  coprimeprodsq  15724  coprimeprodsq2  15725  pcexp  15775  dvdsprmpweqle  15801  difsqpwdvds  15802  ramub1lem1  15941  prmop1  15953  mulgneg2  17772  mndodcongi  18157  oddvdsnn0  18158  sylow1lem1  18208  efgsrel  18342  srgbinomlem4  18739  psrbagconf1o  19577  psrass1lem  19580  psrlidm  19606  psrass1  19608  psrcom  19612  mplsubrglem  19642  mplmonmul  19667  psropprmul  19810  coe1sclmul  19854  coe1sclmul2  19856  cnfldmulg  19980  nn0subm  20003  nn0srg  20018  dvnadd  23900  ply1divex  24104  elqaalem2  24283  geolim3  24302  dvradcnv  24383  pserdv2  24392  logtayllem  24613  logtayl  24614  cxpmul2  24643  atantayl3  24874  leibpilem2  24876  leibpi  24877  log2cnv  24879  dmgmaddn0  24957  chpp1  25089  0sgmppw  25131  logexprlim  25158  dchrhash  25204  bcctr  25208  bcmono  25210  bcmax  25211  bcp1ctr  25212  2lgslem1c  25326  2lgslem3a  25329  2lgslem3b  25330  2lgslem3c  25331  2lgslem3d  25332  2lgslem3a1  25333  2lgslem3b1  25334  2lgslem3c1  25335  2lgslem3d1  25336  dchrisumlem1  25386  ostth2lem2  25531  wlklenvclwlk  26773  upgrwlkdvdelem  26854  wwlknp  26958  wwlknlsw  26963  wlkiswwlks1  26988  wlklnwwlkln2lem  27003  wlknwwlksnbij  27013  wwlksnred  27023  wwlksnext  27024  wwlksnredwwlkn  27026  wwlksnextwrd  27028  wwlksnextinj  27030  wwlksnextproplem2  27042  wwlksnextproplem3  27043  wspthsnwspthsnon  27048  wspthsnwspthsnonOLD  27050  clwlkclwwlklem2a1  27129  clwlkclwwlklem2a4  27134  clwlkclwwlklem2a  27135  clwlkclwwlklem2  27137  clwlkclwwlklem3  27138  wwlksext2clwwlk  27201  wwlksext2clwwlkOLD  27202  clwwlknonex2lem2  27271  eucrctshift  27410  eucrct2eupth  27412  numclwwlk2lem1lem  27512  numclwwlk2lem1lemOLD  27513  numclwwlk1  27535  numclwwlk7  27573  ipasslem1  28008  ipasslem2  28009  dpfrac1  29919  archirngz  30062  subfacval2  31486  bccolsum  31941  faclimlem1  31945  poimirlem28  33744  heiborlem4  33918  heiborlem6  33920  pell14qrgt0  37919  pell14qrdich  37929  pell1qrge1  37930  2nn0ind  38005  jm2.17a  38022  jm2.18  38050  jm2.19lem3  38053  proot1ex  38274  bcc0  39033  dvradcnv2  39040  binomcxplemrat  39043  binomcxplemnotnn0  39049  fperiodmullem  39992  stoweidlem10  40700  stoweidlem17  40707  stoweidlem26  40716  stirlinglem5  40768  stirlinglem7  40770  etransclem23  40947  subsubelfzo0  41905  fargshiftfo  41947  pfxmpt  41956  addlenrevpfx  41966  pfxccatin12lem1  41992  pfxccatin12lem2  41993  pfxccatin12  41994  fmtnodvds  42025  goldbachthlem1  42026  fmtnofac2lem  42049  fmtnofac1  42051  nn0onn0exALTV  42178  nn0enn0exALTV  42179  ply1mulgsumlem1  42736  ply1mulgsumlem2  42737  nn0onn0ex  42880  nn0enn0ex  42881  fllog2  42924  dignn0fr  42957  digexp  42963  0dig2nn0e  42968  0dig2nn0o  42969  dignn0ehalf  42973  nn0mulfsum  42980  nn0mullong  42981