Theorem nn0cn 12401

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11014  ℕ₀cn0 12391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677  ax-1cn 11074  ax-icn 11075  ax-addcl 11076  ax-mulcl 11078  ax-i2m1 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-nn 12136  df-n0 12392

This theorem is referenced by:  nn0nnaddcl  12422  elnn0nn  12433  nn0sub  12441  difgtsumgt  12444  nn0le2x  12445  nn0n0n1ge2  12459  uzaddcl  12812  fzctr  13550  nn0split  13553  elfzoext  13632  zpnn0elfzo1  13649  ubmelm1fzo  13673  subfzo0  13702  quoremnn0ALT  13771  modmuladdnn0  13832  addmodidr  13837  modfzo0difsn  13860  nn0ennn  13896  expadd  14021  expmul  14024  bernneq  14146  bernneq2  14147  faclbnd  14207  faclbnd4lem3  14212  faclbnd4lem4  14213  faclbnd6  14216  bccmpl  14226  bcn0  14227  bcnn  14229  bcnp1n  14231  bcn2  14236  bcp1m1  14237  bcpasc  14238  bcn2p1  14242  hashfzo0  14347  hashfz0  14349  hashxplem  14350  hashdifsnp1  14423  ccatalpha  14511  ccatws1lenp1b  14539  ccatw2s1len  14543  swrdfv2  14579  swrdspsleq  14583  swrdlsw  14585  pfxmpt  14596  pfxswrd  14623  wrdind  14639  wrd2ind  14640  pfxccatin12lem4  14643  pfxccatin12lem1  14645  pfxccatin12lem2  14648  pfxccatin12  14650  swrdccat3blem  14656  repswswrd  14701  repswrevw  14704  cshwidxmodr  14721  2cshw  14730  2cshwcshw  14742  cshwcshid  14744  swrds2  14857  swrd2lsw  14869  iseraltlem2  15600  fsum0diag2  15700  hashiun  15739  ackbijnn  15745  binom1dif  15750  bcxmas  15752  geolim  15787  geomulcvg  15793  risefacval2  15927  fallfacval2  15928  risefaccl  15932  fallfaccl  15933  fallrisefac  15942  risefacp1  15946  fallfacp1  15947  fallfacfac  15962  bpolysum  15970  fsumkthpow  15973  bpoly4  15976  fsumcube  15977  efaddlem  16010  efexp  16020  eftlub  16028  demoivreALT  16120  nn0ob  16305  divalglem4  16317  modremain  16329  mulgcdr  16471  nn0rppwr  16482  nn0seqcvgd  16491  modprmn0modprm0  16729  coprimeprodsq  16730  coprimeprodsq2  16731  pcexp  16781  dvdsprmpweqle  16808  difsqpwdvds  16809  ramub1lem1  16948  prmop1  16960  chnccat  18542  smndex2dlinvh  18835  mulgneg2  19031  mndodcongi  19465  oddvdsnn0  19466  sylow1lem1  19520  efgsrel  19656  fincygsubgodd  20036  srgbinomlem4  20157  cnfldmulg  21350  nn0subm  21369  nn0srg  21384  psrbagconf1o  21876  psrass1lem  21879  psrlidm  21909  psrass1  21911  psrcom  21915  mplsubrglem  21951  mplmonmul  21981  psdmul  22091  psdmvr  22094  psropprmul  22160  coe1sclmul  22206  coe1sclmul2  22208  dvnadd  25868  ply1divex  26079  elqaalem2  26265  geolim3  26284  dvradcnv  26367  pserdv2  26377  logtayllem  26605  logtayl  26606  cxpmul2  26635  atantayl3  26886  leibpilem2  26888  leibpi  26889  log2cnv  26891  dmgmaddn0  26970  chpp1  27102  0sgmppw  27146  logexprlim  27173  dchrhash  27219  bcctr  27223  bcmono  27225  bcmax  27226  bcp1ctr  27227  2lgslem1c  27341  2lgslem3a  27344  2lgslem3b  27345  2lgslem3c  27346  2lgslem3d  27347  2lgslem3a1  27348  2lgslem3b1  27349  2lgslem3c1  27350  2lgslem3d1  27351  2sqreultlem  27395  2sqreulem2  27400  dchrisumlem1  27437  ostth2lem2  27582  wlklenvclwlk  29643  upgrwlkdvdelem  29725  wwlknp  29832  wwlknlsw  29836  wlkiswwlks1  29856  wlklnwwlkln2lem  29871  wlknwwlksnbij  29877  wwlksnred  29881  wwlksnext  29882  wwlksnredwwlkn  29884  wwlksnextwrd  29886  wwlksnextinj  29888  wwlksnextproplem2  29899  wwlksnextproplem3  29900  wspthsnwspthsnon  29905  clwlkclwwlklem2a1  29983  clwlkclwwlklem2a4  29988  clwlkclwwlklem2a  29989  clwlkclwwlklem2  29991  clwlkclwwlklem3  29992  wwlksext2clwwlk  30048  clwwlknonex2lem2  30099  eucrctshift  30234  eucrct2eupth  30236  numclwwlk2lem1lem  30333  numclwwlk1  30352  numclwwlk7  30382  ipasslem1  30822  ipasslem2  30823  dpfrac1  32883  archirngz  33169  nn0constr  33785  pthhashvtx  35183  subfacval2  35242  bccolsum  35794  faclimlem1  35798  poimirlem28  37698  heiborlem4  37864  heiborlem6  37866  lcmineqlem3  42134  facp2  42246  sticksstones7  42255  oddnumth  42419  nicomachus  42420  sumcubes  42421  pell14qrgt0  42966  pell14qrdich  42976  pell1qrge1  42977  2nn0ind  43052  jm2.17a  43067  jm2.18  43095  jm2.19lem3  43098  proot1ex  43303  bcc0  44447  dvradcnv2  44454  binomcxplemrat  44457  binomcxplemnotnn0  44463  fperiodmullem  45418  stoweidlem10  46122  stoweidlem17  46129  stoweidlem26  46138  stirlinglem5  46190  stirlinglem7  46192  etransclem23  46369  cjnpoly  47003  subsubelfzo0  47440  fargshiftfo  47556  fmtnodvds  47658  goldbachthlem1  47659  fmtnofac2lem  47682  fmtnofac1  47684  nn0onn0exALTV  47813  nn0enn0exALTV  47814  isubgr3stgrlem2  48081  nn0mnd  48293  ply1mulgsumlem1  48501  ply1mulgsumlem2  48502  nn0onn0ex  48638  nn0enn0ex  48639  fllog2  48683  dignn0fr  48716  digexp  48722  0dig2nn0e  48727  0dig2nn0o  48728  dignn0ehalf  48732  nn0mulfsum  48739  nn0mullong  48740  itcovalpclem1  48785  itcovalpclem2  48786  itcovalt2lem2lem2  48789  ackval1  48796  ackval2  48797  ackval3  48798