Theorem nn0cn 12563

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11182  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-i2m1 11252

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-nn 12294  df-n0 12554

This theorem is referenced by:  nn0nnaddcl  12584  elnn0nn  12595  nn0sub  12603  difgtsumgt  12606  nn0n0n1ge2  12620  uzaddcl  12969  fzctr  13697  nn0split  13700  elfzoext  13773  zpnn0elfzo1  13790  ubmelm1fzo  13813  subfzo0  13839  quoremnn0ALT  13908  modmuladdnn0  13966  addmodidr  13971  modfzo0difsn  13994  nn0ennn  14030  expadd  14155  expmul  14158  bernneq  14278  bernneq2  14279  faclbnd  14339  faclbnd4lem3  14344  faclbnd4lem4  14345  faclbnd6  14348  bccmpl  14358  bcn0  14359  bcnn  14361  bcnp1n  14363  bcn2  14368  bcp1m1  14369  bcpasc  14370  bcn2p1  14374  hashfzo0  14479  hashfz0  14481  hashxplem  14482  hashdifsnp1  14555  ccatalpha  14641  ccatws1lenp1b  14669  ccatw2s1len  14673  swrdfv2  14709  swrdspsleq  14713  swrdlsw  14715  pfxmpt  14726  addlenrevpfx  14738  pfxswrd  14754  wrdind  14770  wrd2ind  14771  pfxccatin12lem4  14774  pfxccatin12lem1  14776  pfxccatin12lem2  14779  pfxccatin12  14781  swrdccat3blem  14787  repswswrd  14832  repswrevw  14835  cshwidxmodr  14852  2cshw  14861  2cshwcshw  14874  cshwcshid  14876  swrds2  14989  swrd2lsw  15001  iseraltlem2  15731  fsum0diag2  15831  hashiun  15870  ackbijnn  15876  binom1dif  15881  bcxmas  15883  geolim  15918  geomulcvg  15924  risefacval2  16058  fallfacval2  16059  risefaccl  16063  fallfaccl  16064  fallrisefac  16073  risefacp1  16077  fallfacp1  16078  fallfacfac  16093  bpolysum  16101  fsumkthpow  16104  bpoly4  16107  fsumcube  16108  efaddlem  16141  efexp  16149  eftlub  16157  demoivreALT  16249  nn0ob  16432  divalglem4  16444  modremain  16456  mulgcdr  16597  nn0rppwr  16608  nn0seqcvgd  16617  modprmn0modprm0  16854  coprimeprodsq  16855  coprimeprodsq2  16856  pcexp  16906  dvdsprmpweqle  16933  difsqpwdvds  16934  ramub1lem1  17073  prmop1  17085  smndex2dlinvh  18952  mulgneg2  19148  mndodcongi  19585  oddvdsnn0  19586  sylow1lem1  19640  efgsrel  19776  fincygsubgodd  20156  srgbinomlem4  20256  cnfldmulg  21439  nn0subm  21463  nn0srg  21478  psrbagconf1o  21972  psrass1lem  21975  psrlidm  22005  psrass1  22007  psrcom  22011  mplsubrglem  22047  mplmonmul  22077  psdmul  22193  psropprmul  22260  coe1sclmul  22306  coe1sclmul2  22308  dvnadd  25985  ply1divex  26196  elqaalem2  26380  geolim3  26399  dvradcnv  26482  pserdv2  26492  logtayllem  26719  logtayl  26720  cxpmul2  26749  atantayl3  27000  leibpilem2  27002  leibpi  27003  log2cnv  27005  dmgmaddn0  27084  chpp1  27216  0sgmppw  27260  logexprlim  27287  dchrhash  27333  bcctr  27337  bcmono  27339  bcmax  27340  bcp1ctr  27341  2lgslem1c  27455  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2lgslem3a1  27462  2lgslem3b1  27463  2lgslem3c1  27464  2lgslem3d1  27465  2sqreultlem  27509  2sqreulem2  27514  dchrisumlem1  27551  ostth2lem2  27696  wlklenvclwlk  29691  upgrwlkdvdelem  29772  wwlknp  29876  wwlknlsw  29880  wlkiswwlks1  29900  wlklnwwlkln2lem  29915  wlknwwlksnbij  29921  wwlksnred  29925  wwlksnext  29926  wwlksnredwwlkn  29928  wwlksnextwrd  29930  wwlksnextinj  29932  wwlksnextproplem2  29943  wwlksnextproplem3  29944  wspthsnwspthsnon  29949  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlklem3  30033  wwlksext2clwwlk  30089  clwwlknonex2lem2  30140  eucrctshift  30275  eucrct2eupth  30277  numclwwlk2lem1lem  30374  numclwwlk1  30393  numclwwlk7  30423  ipasslem1  30863  ipasslem2  30864  dpfrac1  32856  archirngz  33169  pthhashvtx  35095  subfacval2  35155  bccolsum  35701  faclimlem1  35705  poimirlem28  37608  heiborlem4  37774  heiborlem6  37776  lcmineqlem3  41988  facp2  42100  sticksstones7  42109  fac2xp3  42196  factwoffsmonot  42199  oddnumth  42299  nicomachus  42300  sumcubes  42301  pell14qrgt0  42815  pell14qrdich  42825  pell1qrge1  42826  2nn0ind  42902  jm2.17a  42917  jm2.18  42945  jm2.19lem3  42948  proot1ex  43157  bcc0  44309  dvradcnv2  44316  binomcxplemrat  44319  binomcxplemnotnn0  44325  fperiodmullem  45218  stoweidlem10  45931  stoweidlem17  45938  stoweidlem26  45947  stirlinglem5  45999  stirlinglem7  46001  etransclem23  46178  subsubelfzo0  47241  fargshiftfo  47316  fmtnodvds  47418  goldbachthlem1  47419  fmtnofac2lem  47442  fmtnofac1  47444  nn0onn0exALTV  47573  nn0enn0exALTV  47574  nn0mnd  47902  ply1mulgsumlem1  48115  ply1mulgsumlem2  48116  nn0onn0ex  48257  nn0enn0ex  48258  fllog2  48302  dignn0fr  48335  digexp  48341  0dig2nn0e  48346  0dig2nn0o  48347  dignn0ehalf  48351  nn0mulfsum  48358  nn0mullong  48359  itcovalpclem1  48404  itcovalpclem2  48405  itcovalt2lem2lem2  48408  ackval1  48415  ackval2  48416  ackval3  48417