Theorem nn0cn 12447

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℕ₀cn0 12437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-i2m1 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  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 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175  df-n0 12438

This theorem is referenced by:  nn0nnaddcl  12468  elnn0nn  12479  nn0sub  12487  difgtsumgt  12490  nn0le2x  12491  nn0n0n1ge2  12505  uzaddcl  12854  fzctr  13594  nn0split  13597  elfzoext  13677  zpnn0elfzo1  13694  ubmelm1fzo  13718  subfzo0  13747  quoremnn0ALT  13816  modmuladdnn0  13877  addmodidr  13882  modfzo0difsn  13905  nn0ennn  13941  expadd  14066  expmul  14069  bernneq  14191  bernneq2  14192  faclbnd  14252  faclbnd4lem3  14257  faclbnd4lem4  14258  faclbnd6  14261  bccmpl  14271  bcn0  14272  bcnn  14274  bcnp1n  14276  bcn2  14281  bcp1m1  14282  bcpasc  14283  bcn2p1  14287  hashfzo0  14392  hashfz0  14394  hashxplem  14395  hashdifsnp1  14468  ccatalpha  14556  ccatws1lenp1b  14584  ccatw2s1len  14588  swrdfv2  14624  swrdspsleq  14628  swrdlsw  14630  pfxmpt  14641  pfxswrd  14668  wrdind  14684  wrd2ind  14685  pfxccatin12lem4  14688  pfxccatin12lem1  14690  pfxccatin12lem2  14693  pfxccatin12  14695  swrdccat3blem  14701  repswswrd  14746  repswrevw  14749  cshwidxmodr  14766  2cshw  14775  2cshwcshw  14787  cshwcshid  14789  swrds2  14902  swrd2lsw  14914  iseraltlem2  15645  fsum0diag2  15745  hashiun  15785  ackbijnn  15793  binom1dif  15798  bcxmas  15800  geolim  15835  geomulcvg  15841  risefacval2  15975  fallfacval2  15976  risefaccl  15980  fallfaccl  15981  fallrisefac  15990  risefacp1  15994  fallfacp1  15995  fallfacfac  16010  bpolysum  16018  fsumkthpow  16021  bpoly4  16024  fsumcube  16025  efaddlem  16058  efexp  16068  eftlub  16076  demoivreALT  16168  nn0ob  16353  divalglem4  16365  modremain  16377  mulgcdr  16519  nn0rppwr  16530  nn0seqcvgd  16539  modprmn0modprm0  16778  coprimeprodsq  16779  coprimeprodsq2  16780  pcexp  16830  dvdsprmpweqle  16857  difsqpwdvds  16858  ramub1lem1  16997  prmop1  17009  chnccat  18592  smndex2dlinvh  18888  mulgneg2  19084  mndodcongi  19518  oddvdsnn0  19519  sylow1lem1  19573  efgsrel  19709  fincygsubgodd  20089  srgbinomlem4  20210  cnfldmulg  21384  nn0subm  21402  nn0srg  21417  psrbagconf1o  21909  psrass1lem  21912  psrlidm  21940  psrass1  21942  psrcom  21946  mplsubrglem  21982  mplmonmul  22014  psdmul  22132  psdmvr  22135  psropprmul  22201  coe1sclmul  22247  coe1sclmul2  22249  dvnadd  25896  ply1divex  26102  elqaalem2  26286  geolim3  26305  dvradcnv  26386  pserdv2  26395  logtayllem  26623  logtayl  26624  cxpmul2  26653  atantayl3  26903  leibpilem2  26905  leibpi  26906  log2cnv  26908  dmgmaddn0  26986  chpp1  27118  0sgmppw  27161  logexprlim  27188  dchrhash  27234  bcctr  27238  bcmono  27240  bcmax  27241  bcp1ctr  27242  2lgslem1c  27356  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgslem3d1  27366  2sqreultlem  27410  2sqreulem2  27415  dchrisumlem1  27452  ostth2lem2  27597  wlklenvclwlk  29722  upgrwlkdvdelem  29804  wwlknp  29911  wwlknlsw  29915  wlkiswwlks1  29935  wlklnwwlkln2lem  29950  wlknwwlksnbij  29956  wwlksnred  29960  wwlksnext  29961  wwlksnredwwlkn  29963  wwlksnextwrd  29965  wwlksnextinj  29967  wwlksnextproplem2  29978  wwlksnextproplem3  29979  wspthsnwspthsnon  29984  clwlkclwwlklem2a1  30062  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlklem3  30071  wwlksext2clwwlk  30127  clwwlknonex2lem2  30178  eucrctshift  30313  eucrct2eupth  30315  numclwwlk2lem1lem  30412  numclwwlk1  30431  numclwwlk7  30461  ipasslem1  30902  ipasslem2  30903  dpfrac1  32951  archirngz  33250  psrmonmul  33694  nn0constr  33905  pthhashvtx  35310  subfacval2  35369  bccolsum  35921  faclimlem1  35925  poimirlem28  37969  heiborlem4  38135  heiborlem6  38137  lcmineqlem3  42470  facp2  42582  sticksstones7  42591  oddnumth  42743  nicomachus  42744  sumcubes  42745  pell14qrgt0  43287  pell14qrdich  43297  pell1qrge1  43298  2nn0ind  43373  jm2.17a  43388  jm2.18  43416  jm2.19lem3  43419  proot1ex  43624  bcc0  44767  dvradcnv2  44774  binomcxplemrat  44777  binomcxplemnotnn0  44783  fperiodmullem  45736  stoweidlem10  46438  stoweidlem17  46445  stoweidlem26  46454  stirlinglem5  46506  stirlinglem7  46508  etransclem23  46685  cjnpoly  47337  subsubelfzo0  47775  fargshiftfo  47902  fmtnodvds  48007  goldbachthlem1  48008  fmtnofac2lem  48031  fmtnofac1  48033  nn0onn0exALTV  48175  nn0enn0exALTV  48176  isubgr3stgrlem2  48443  nn0mnd  48655  ply1mulgsumlem1  48862  ply1mulgsumlem2  48863  nn0onn0ex  48999  nn0enn0ex  49000  fllog2  49044  dignn0fr  49077  digexp  49083  0dig2nn0e  49088  0dig2nn0o  49089  dignn0ehalf  49093  nn0mulfsum  49100  nn0mullong  49101  itcovalpclem1  49146  itcovalpclem2  49147  itcovalt2lem2lem2  49150  ackval1  49157  ackval2  49158  ackval3  49159