Theorem nn0cn 12173

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 10800  ℕ₀cn0 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-i2m1 10870

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-nn 11904  df-n0 12164

This theorem is referenced by:  nn0nnaddcl  12194  elnn0nn  12205  nn0sub  12213  difgtsumgt  12216  nn0n0n1ge2  12230  uzaddcl  12573  fzctr  13297  nn0split  13300  elfzoext  13372  zpnn0elfzo1  13389  ubmelm1fzo  13411  subfzo0  13437  quoremnn0ALT  13505  modmuladdnn0  13563  addmodidr  13568  modfzo0difsn  13591  nn0ennn  13627  expadd  13753  expmul  13756  bernneq  13872  bernneq2  13873  faclbnd  13932  faclbnd4lem3  13937  faclbnd4lem4  13938  faclbnd6  13941  bccmpl  13951  bcn0  13952  bcnn  13954  bcnp1n  13956  bcn2  13961  bcp1m1  13962  bcpasc  13963  bcn2p1  13967  hashfzo0  14073  hashfz0  14075  hashxplem  14076  hashdifsnp1  14138  ccatalpha  14226  ccatws1lenp1b  14254  ccatw2s1len  14259  swrdfv2  14302  swrdspsleq  14306  swrdlsw  14308  pfxmpt  14319  addlenrevpfx  14331  pfxswrd  14347  wrdind  14363  wrd2ind  14364  pfxccatin12lem4  14367  pfxccatin12lem1  14369  pfxccatin12lem2  14372  pfxccatin12  14374  swrdccat3blem  14380  repswswrd  14425  repswrevw  14428  cshwidxmodr  14445  2cshw  14454  2cshwcshw  14466  cshwcshid  14468  swrds2  14581  swrd2lsw  14593  iseraltlem2  15322  fsum0diag2  15423  hashiun  15462  ackbijnn  15468  binom1dif  15473  bcxmas  15475  geolim  15510  geomulcvg  15516  risefacval2  15648  fallfacval2  15649  risefaccl  15653  fallfaccl  15654  fallrisefac  15663  risefacp1  15667  fallfacp1  15668  fallfacfac  15683  bpolysum  15691  fsumkthpow  15694  bpoly4  15697  fsumcube  15698  efaddlem  15730  efexp  15738  eftlub  15746  demoivreALT  15838  nn0ob  16021  divalglem4  16033  modremain  16045  mulgcdr  16186  nn0seqcvgd  16203  modprmn0modprm0  16436  coprimeprodsq  16437  coprimeprodsq2  16438  pcexp  16488  dvdsprmpweqle  16515  difsqpwdvds  16516  ramub1lem1  16655  prmop1  16667  smndex2dlinvh  18471  mulgneg2  18652  mndodcongi  19066  oddvdsnn0  19067  sylow1lem1  19118  efgsrel  19255  fincygsubgodd  19630  srgbinomlem4  19694  cnfldmulg  20542  nn0subm  20565  nn0srg  20580  psrbagconf1o  21049  psrbagconf1oOLD  21050  psrass1lemOLD  21053  psrass1lem  21056  psrlidm  21082  psrass1  21084  psrcom  21088  mplsubrglem  21120  mplmonmul  21147  psropprmul  21319  coe1sclmul  21363  coe1sclmul2  21365  dvnadd  24998  ply1divex  25206  elqaalem2  25385  geolim3  25404  dvradcnv  25485  pserdv2  25494  logtayllem  25719  logtayl  25720  cxpmul2  25749  atantayl3  25994  leibpilem2  25996  leibpi  25997  log2cnv  25999  dmgmaddn0  26077  chpp1  26209  0sgmppw  26251  logexprlim  26278  dchrhash  26324  bcctr  26328  bcmono  26330  bcmax  26331  bcp1ctr  26332  2lgslem1c  26446  2lgslem3a  26449  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  2lgslem3a1  26453  2lgslem3b1  26454  2lgslem3c1  26455  2lgslem3d1  26456  2sqreultlem  26500  2sqreulem2  26505  dchrisumlem1  26542  ostth2lem2  26687  wlklenvclwlk  27924  wlklenvclwlkOLD  27925  upgrwlkdvdelem  28005  wwlknp  28109  wwlknlsw  28113  wlkiswwlks1  28133  wlklnwwlkln2lem  28148  wlknwwlksnbij  28154  wwlksnred  28158  wwlksnext  28159  wwlksnredwwlkn  28161  wwlksnextwrd  28163  wwlksnextinj  28165  wwlksnextproplem2  28176  wwlksnextproplem3  28177  wspthsnwspthsnon  28182  clwlkclwwlklem2a1  28257  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwlkclwwlklem3  28266  wwlksext2clwwlk  28322  clwwlknonex2lem2  28373  eucrctshift  28508  eucrct2eupth  28510  numclwwlk2lem1lem  28607  numclwwlk1  28626  numclwwlk7  28656  ipasslem1  29094  ipasslem2  29095  dpfrac1  31068  archirngz  31345  pthhashvtx  32989  subfacval2  33049  bccolsum  33611  faclimlem1  33615  poimirlem28  35732  heiborlem4  35899  heiborlem6  35901  lcmineqlem3  39967  facp2  40027  sticksstones7  40036  fac2xp3  40088  factwoffsmonot  40091  nn0rppwr  40254  pell14qrgt0  40597  pell14qrdich  40607  pell1qrge1  40608  2nn0ind  40683  jm2.17a  40698  jm2.18  40726  jm2.19lem3  40729  proot1ex  40942  bcc0  41847  dvradcnv2  41854  binomcxplemrat  41857  binomcxplemnotnn0  41863  fperiodmullem  42732  stoweidlem10  43441  stoweidlem17  43448  stoweidlem26  43457  stirlinglem5  43509  stirlinglem7  43511  etransclem23  43688  subsubelfzo0  44706  fargshiftfo  44782  fmtnodvds  44884  goldbachthlem1  44885  fmtnofac2lem  44908  fmtnofac1  44910  nn0onn0exALTV  45039  nn0enn0exALTV  45040  nn0mnd  45261  ply1mulgsumlem1  45615  ply1mulgsumlem2  45616  nn0onn0ex  45757  nn0enn0ex  45758  fllog2  45802  dignn0fr  45835  digexp  45841  0dig2nn0e  45846  0dig2nn0o  45847  dignn0ehalf  45851  nn0mulfsum  45858  nn0mullong  45859  itcovalpclem1  45904  itcovalpclem2  45905  itcovalt2lem2lem2  45908  ackval1  45915  ackval2  45916  ackval3  45917