Theorem nn0cn 12438

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11027  ℕ₀cn0 12428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-i2m1 11097

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12166  df-n0 12429

This theorem is referenced by:  nn0nnaddcl  12459  elnn0nn  12470  nn0sub  12478  difgtsumgt  12481  nn0le2x  12482  nn0n0n1ge2  12496  uzaddcl  12845  fzctr  13585  nn0split  13588  elfzoext  13668  zpnn0elfzo1  13685  ubmelm1fzo  13709  subfzo0  13738  quoremnn0ALT  13807  modmuladdnn0  13868  addmodidr  13873  modfzo0difsn  13896  nn0ennn  13932  expadd  14057  expmul  14060  bernneq  14182  bernneq2  14183  faclbnd  14243  faclbnd4lem3  14248  faclbnd4lem4  14249  faclbnd6  14252  bccmpl  14262  bcn0  14263  bcnn  14265  bcnp1n  14267  bcn2  14272  bcp1m1  14273  bcpasc  14274  bcn2p1  14278  hashfzo0  14383  hashfz0  14385  hashxplem  14386  hashdifsnp1  14459  ccatalpha  14547  ccatws1lenp1b  14575  ccatw2s1len  14579  swrdfv2  14615  swrdspsleq  14619  swrdlsw  14621  pfxmpt  14632  pfxswrd  14659  wrdind  14675  wrd2ind  14676  pfxccatin12lem4  14679  pfxccatin12lem1  14681  pfxccatin12lem2  14684  pfxccatin12  14686  swrdccat3blem  14692  repswswrd  14737  repswrevw  14740  cshwidxmodr  14757  2cshw  14766  2cshwcshw  14778  cshwcshid  14780  swrds2  14893  swrd2lsw  14905  iseraltlem2  15636  fsum0diag2  15736  hashiun  15776  ackbijnn  15784  binom1dif  15789  bcxmas  15791  geolim  15826  geomulcvg  15832  risefacval2  15966  fallfacval2  15967  risefaccl  15971  fallfaccl  15972  fallrisefac  15981  risefacp1  15985  fallfacp1  15986  fallfacfac  16001  bpolysum  16009  fsumkthpow  16012  bpoly4  16015  fsumcube  16016  efaddlem  16049  efexp  16059  eftlub  16067  demoivreALT  16159  nn0ob  16344  divalglem4  16356  modremain  16368  mulgcdr  16510  nn0rppwr  16521  nn0seqcvgd  16530  modprmn0modprm0  16769  coprimeprodsq  16770  coprimeprodsq2  16771  pcexp  16821  dvdsprmpweqle  16848  difsqpwdvds  16849  ramub1lem1  16988  prmop1  17000  chnccat  18583  smndex2dlinvh  18879  mulgneg2  19075  mndodcongi  19509  oddvdsnn0  19510  sylow1lem1  19564  efgsrel  19700  fincygsubgodd  20080  srgbinomlem4  20201  cnfldmulg  21379  nn0subm  21397  nn0srg  21412  psrbagconf1o  21904  psrass1lem  21908  psrlidm  21936  psrass1  21938  psrcom  21942  mplsubrglem  21978  mplmonmul  22012  psdmul  22154  psdmvr  22157  psropprmul  22222  coe1sclmul  22268  coe1sclmul2  22270  dvnadd  25914  ply1divex  26120  elqaalem2  26304  geolim3  26323  dvradcnv  26404  pserdv2  26413  logtayllem  26641  logtayl  26642  cxpmul2  26671  atantayl3  26921  leibpilem2  26923  leibpi  26924  log2cnv  26926  dmgmaddn0  27004  chpp1  27136  0sgmppw  27179  logexprlim  27206  dchrhash  27252  bcctr  27256  bcmono  27258  bcmax  27259  bcp1ctr  27260  2lgslem1c  27374  2lgslem3a  27377  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  2lgslem3a1  27381  2lgslem3b1  27382  2lgslem3c1  27383  2lgslem3d1  27384  2sqreultlem  27428  2sqreulem2  27433  dchrisumlem1  27470  ostth2lem2  27615  wlklenvclwlk  29740  upgrwlkdvdelem  29822  wwlknp  29929  wwlknlsw  29933  wlkiswwlks1  29953  wlklnwwlkln2lem  29968  wlknwwlksnbij  29974  wwlksnred  29978  wwlksnext  29979  wwlksnredwwlkn  29981  wwlksnextwrd  29983  wwlksnextinj  29985  wwlksnextproplem2  29996  wwlksnextproplem3  29997  wspthsnwspthsnon  30002  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwlkclwwlklem3  30089  wwlksext2clwwlk  30145  clwwlknonex2lem2  30196  eucrctshift  30331  eucrct2eupth  30333  numclwwlk2lem1lem  30430  numclwwlk1  30449  numclwwlk7  30479  ipasslem1  30920  ipasslem2  30921  dpfrac1  32970  archirngz  33270  psrmonmul  33734  nn0constr  33945  pthhashvtx  35356  subfacval2  35415  bccolsum  35967  faclimlem1  35971  poimirlem28  38015  heiborlem4  38181  heiborlem6  38183  lcmineqlem3  42516  facp2  42628  sticksstones7  42637  oddnumth  42788  nicomachus  42789  sumcubes  42790  pell14qrgt0  43304  pell14qrdich  43314  pell1qrge1  43315  2nn0ind  43390  jm2.17a  43405  jm2.18  43433  jm2.19lem3  43436  proot1ex  43641  bcc0  44784  dvradcnv2  44791  binomcxplemrat  44794  binomcxplemnotnn0  44800  fperiodmullem  45751  stoweidlem10  46453  stoweidlem17  46460  stoweidlem26  46469  stirlinglem5  46521  stirlinglem7  46523  etransclem23  46700  cjnpoly  47352  subsubelfzo0  47790  fargshiftfo  47917  fmtnodvds  48022  goldbachthlem1  48023  fmtnofac2lem  48046  fmtnofac1  48048  nn0onn0exALTV  48190  nn0enn0exALTV  48191  isubgr3stgrlem2  48458  nn0mnd  48670  ply1mulgsumlem1  48877  ply1mulgsumlem2  48878  nn0onn0ex  49014  nn0enn0ex  49015  fllog2  49059  dignn0fr  49092  digexp  49098  0dig2nn0e  49103  0dig2nn0o  49104  dignn0ehalf  49108  nn0mulfsum  49115  nn0mullong  49116  itcovalpclem1  49161  itcovalpclem2  49162  itcovalt2lem2lem2  49165  ackval1  49172  ackval2  49173  ackval3  49174