Theorem nn0cn 12428

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11042  ℕ₀cn0 12418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-i2m1 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163  df-n0 12419

This theorem is referenced by:  nn0nnaddcl  12449  elnn0nn  12460  nn0sub  12468  difgtsumgt  12471  nn0le2x  12472  nn0n0n1ge2  12486  uzaddcl  12839  fzctr  13577  nn0split  13580  elfzoext  13659  zpnn0elfzo1  13676  ubmelm1fzo  13700  subfzo0  13726  quoremnn0ALT  13795  modmuladdnn0  13856  addmodidr  13861  modfzo0difsn  13884  nn0ennn  13920  expadd  14045  expmul  14048  bernneq  14170  bernneq2  14171  faclbnd  14231  faclbnd4lem3  14236  faclbnd4lem4  14237  faclbnd6  14240  bccmpl  14250  bcn0  14251  bcnn  14253  bcnp1n  14255  bcn2  14260  bcp1m1  14261  bcpasc  14262  bcn2p1  14266  hashfzo0  14371  hashfz0  14373  hashxplem  14374  hashdifsnp1  14447  ccatalpha  14534  ccatws1lenp1b  14562  ccatw2s1len  14566  swrdfv2  14602  swrdspsleq  14606  swrdlsw  14608  pfxmpt  14619  addlenrevpfx  14631  pfxswrd  14647  wrdind  14663  wrd2ind  14664  pfxccatin12lem4  14667  pfxccatin12lem1  14669  pfxccatin12lem2  14672  pfxccatin12  14674  swrdccat3blem  14680  repswswrd  14725  repswrevw  14728  cshwidxmodr  14745  2cshw  14754  2cshwcshw  14767  cshwcshid  14769  swrds2  14882  swrd2lsw  14894  iseraltlem2  15625  fsum0diag2  15725  hashiun  15764  ackbijnn  15770  binom1dif  15775  bcxmas  15777  geolim  15812  geomulcvg  15818  risefacval2  15952  fallfacval2  15953  risefaccl  15957  fallfaccl  15958  fallrisefac  15967  risefacp1  15971  fallfacp1  15972  fallfacfac  15987  bpolysum  15995  fsumkthpow  15998  bpoly4  16001  fsumcube  16002  efaddlem  16035  efexp  16045  eftlub  16053  demoivreALT  16145  nn0ob  16330  divalglem4  16342  modremain  16354  mulgcdr  16496  nn0rppwr  16507  nn0seqcvgd  16516  modprmn0modprm0  16754  coprimeprodsq  16755  coprimeprodsq2  16756  pcexp  16806  dvdsprmpweqle  16833  difsqpwdvds  16834  ramub1lem1  16973  prmop1  16985  smndex2dlinvh  18820  mulgneg2  19016  mndodcongi  19449  oddvdsnn0  19450  sylow1lem1  19504  efgsrel  19640  fincygsubgodd  20020  srgbinomlem4  20114  cnfldmulg  21291  nn0subm  21315  nn0srg  21330  psrbagconf1o  21814  psrass1lem  21817  psrlidm  21847  psrass1  21849  psrcom  21853  mplsubrglem  21889  mplmonmul  21919  psdmul  22029  psdmvr  22032  psropprmul  22098  coe1sclmul  22144  coe1sclmul2  22146  dvnadd  25807  ply1divex  26018  elqaalem2  26204  geolim3  26223  dvradcnv  26306  pserdv2  26316  logtayllem  26544  logtayl  26545  cxpmul2  26574  atantayl3  26825  leibpilem2  26827  leibpi  26828  log2cnv  26830  dmgmaddn0  26909  chpp1  27041  0sgmppw  27085  logexprlim  27112  dchrhash  27158  bcctr  27162  bcmono  27164  bcmax  27165  bcp1ctr  27166  2lgslem1c  27280  2lgslem3a  27283  2lgslem3b  27284  2lgslem3c  27285  2lgslem3d  27286  2lgslem3a1  27287  2lgslem3b1  27288  2lgslem3c1  27289  2lgslem3d1  27290  2sqreultlem  27334  2sqreulem2  27339  dchrisumlem1  27376  ostth2lem2  27521  wlklenvclwlk  29557  upgrwlkdvdelem  29639  wwlknp  29746  wwlknlsw  29750  wlkiswwlks1  29770  wlklnwwlkln2lem  29785  wlknwwlksnbij  29791  wwlksnred  29795  wwlksnext  29796  wwlksnredwwlkn  29798  wwlksnextwrd  29800  wwlksnextinj  29802  wwlksnextproplem2  29813  wwlksnextproplem3  29814  wspthsnwspthsnon  29819  clwlkclwwlklem2a1  29894  clwlkclwwlklem2a4  29899  clwlkclwwlklem2a  29900  clwlkclwwlklem2  29902  clwlkclwwlklem3  29903  wwlksext2clwwlk  29959  clwwlknonex2lem2  30010  eucrctshift  30145  eucrct2eupth  30147  numclwwlk2lem1lem  30244  numclwwlk1  30263  numclwwlk7  30293  ipasslem1  30733  ipasslem2  30734  dpfrac1  32785  archirngz  33116  nn0constr  33724  pthhashvtx  35088  subfacval2  35147  bccolsum  35699  faclimlem1  35703  poimirlem28  37615  heiborlem4  37781  heiborlem6  37783  lcmineqlem3  41992  facp2  42104  sticksstones7  42113  oddnumth  42272  nicomachus  42273  sumcubes  42274  pell14qrgt0  42820  pell14qrdich  42830  pell1qrge1  42831  2nn0ind  42907  jm2.17a  42922  jm2.18  42950  jm2.19lem3  42953  proot1ex  43158  bcc0  44302  dvradcnv2  44309  binomcxplemrat  44312  binomcxplemnotnn0  44318  fperiodmullem  45274  stoweidlem10  45981  stoweidlem17  45988  stoweidlem26  45997  stirlinglem5  46049  stirlinglem7  46051  etransclem23  46228  cjnpoly  46863  subsubelfzo0  47300  fargshiftfo  47416  fmtnodvds  47518  goldbachthlem1  47519  fmtnofac2lem  47542  fmtnofac1  47544  nn0onn0exALTV  47673  nn0enn0exALTV  47674  isubgr3stgrlem2  47939  nn0mnd  48140  ply1mulgsumlem1  48348  ply1mulgsumlem2  48349  nn0onn0ex  48485  nn0enn0ex  48486  fllog2  48530  dignn0fr  48563  digexp  48569  0dig2nn0e  48574  0dig2nn0o  48575  dignn0ehalf  48579  nn0mulfsum  48586  nn0mullong  48587  itcovalpclem1  48632  itcovalpclem2  48633  itcovalt2lem2lem2  48636  ackval1  48643  ackval2  48644  ackval3  48645