Theorem nn0cn 11179

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℂcc 9813  ℕ₀cn0 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898  df-n0 11170

This theorem is referenced by:  nn0nnaddcl  11201  elnn0nn  11212  nn0sub  11220  difgtsumgt  11223  nn0n0n1ge2  11235  uzaddcl  11620  fzctr  12320  nn0split  12323  elfzoext  12392  zpnn0elfzo1  12408  ubmelm1fzo  12430  subfzo0  12452  quoremnn0ALT  12518  modmuladdnn0  12576  addmodidr  12581  modfzo0difsn  12604  nn0ennn  12640  expadd  12764  expmul  12767  bernneq  12852  bernneq2  12853  faclbnd  12939  faclbnd4lem3  12944  faclbnd4lem4  12945  faclbnd6  12948  bccmpl  12958  bcn0  12959  bcnn  12961  bcnp1n  12963  bcn2  12968  bcp1m1  12969  bcpasc  12970  bcn2p1  12974  hashfzo0  13077  hashfz0  13079  hashxplem  13080  brfi1indlem  13133  ccatalpha  13228  ccatw2s1len  13254  addlenrevswrd  13289  swrdfv2  13298  swrdspsleq  13301  swrdlsw  13304  swrd0swrd  13313  ccats1swrdeq  13321  wrdind  13328  wrd2ind  13329  swrdccatin12lem1  13335  swrdccatin12lem2b  13337  swrdccatin12lem2  13340  swrdccatin12  13342  swrdccat3blem  13346  repswswrd  13382  repswrevw  13384  cshwidxmodr  13401  2cshw  13410  2cshwcshw  13422  cshwcshid  13424  swrds2  13533  swrd2lsw  13543  iseraltlem2  14261  fsum0diag2  14357  hashiun  14395  ackbijnn  14399  binom1dif  14404  bcxmas  14406  geolim  14440  geomulcvg  14446  risefacval2  14580  fallfacval2  14581  risefaccl  14585  fallfaccl  14586  fallrisefac  14595  risefacp1  14599  fallfacp1  14600  fallfacfac  14615  bpolysum  14623  fsumkthpow  14626  bpoly4  14629  fsumcube  14630  efaddlem  14662  efexp  14670  eftlub  14678  demoivreALT  14770  nn0ob  14938  divalglem4  14957  modremain  14970  mulgcdr  15105  nn0seqcvgd  15121  modprmn0modprm0  15350  coprimeprodsq  15351  coprimeprodsq2  15352  pcexp  15402  dvdsprmpweqle  15428  difsqpwdvds  15429  ramub1lem1  15568  prmop1  15580  mulgneg2  17398  mndodcongi  17785  oddvdsnn0  17786  sylow1lem1  17836  efgsrel  17970  srgbinomlem4  18366  psrbagconf1o  19195  psrass1lem  19198  psrlidm  19224  psrass1  19226  psrcom  19230  mplsubrglem  19260  mplmonmul  19285  psropprmul  19429  coe1sclmul  19473  coe1sclmul2  19475  cnfldmulg  19597  nn0subm  19620  nn0srg  19635  dvnadd  23498  ply1divex  23700  elqaalem2  23879  geolim3  23898  dvradcnv  23979  pserdv2  23988  logtayllem  24205  logtayl  24206  cxpmul2  24235  atantayl3  24466  leibpilem2  24468  leibpi  24469  log2cnv  24471  dmgmaddn0  24549  chpp1  24681  0sgmppw  24723  logexprlim  24750  dchrhash  24796  bcctr  24800  bcmono  24802  bcmax  24803  bcp1ctr  24804  2lgslem1c  24918  2lgslem3a  24921  2lgslem3b  24922  2lgslem3c  24923  2lgslem3d  24924  2lgslem3a1  24925  2lgslem3b1  24926  2lgslem3c1  24927  2lgslem3d1  24928  dchrisumlem1  24978  ostth2lem2  25123  cusgrasizeinds  26004  wlklenvm1  26060  fargshiftfo  26166  wwlknimp  26215  wlkiswwlk1  26218  wlklniswwlkn2  26228  wwlknred  26251  wwlknext  26252  wwlknredwwlkn  26254  wwlkextwrd  26256  wwlkextinj  26258  wwlkextproplem2  26270  wwlkextproplem3  26271  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwlkisclwwlklem0  26316  wwlkext2clwwlk  26331  wlklenvclwlk  26366  rusgranumwlks  26483  rusgranumwlk  26484  usgreghash2spot  26596  frgregordn0  26597  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwwlk1  26625  numclwwlk3  26636  numclwwlk7  26641  ipasslem1  27070  ipasslem2  27071  archirngz  29074  subfacval2  30423  bccolsum  30878  faclimlem1  30882  poimirlem28  32607  heiborlem4  32783  heiborlem6  32785  pell14qrgt0  36441  pell14qrdich  36451  pell1qrge1  36452  2nn0ind  36528  jm2.17a  36545  jm2.18  36573  jm2.19lem3  36576  proot1ex  36798  bcc0  37561  dvradcnv2  37568  binomcxplemrat  37571  binomcxplemnotnn0  37577  fperiodmullem  38458  stoweidlem10  38903  stoweidlem17  38910  stoweidlem26  38919  stirlinglem5  38971  stirlinglem7  38973  etransclem23  39150  fmtnodvds  39994  goldbachthlem1  39995  fmtnofac2lem  40018  fmtnofac1  40020  nn0onn0exALTV  40147  nn0enn0exALTV  40148  pfxmpt  40250  addlenrevpfx  40260  pfxccatin12lem1  40286  pfxccatin12lem2  40287  pfxccatin12  40288  subsubelfzo0  40359  1wlklenvclwlk  40863  upgrwlkdvdelem  40942  wwlknp  41045  1wlkiswwlks1  41064  1wlklnwwlkln2lem  41079  wwlksnred  41098  wwlksnext  41099  wwlksnredwwlkn  41101  wwlksnextwrd  41103  wwlksnextinj  41105  wwlksnextproplem2  41116  wwlksnextproplem3  41117  wspthsnwspthsnon  41122  clwlkclwwlklem2a1  41201  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwlkclwwlklem3  41210  wwlksext2clwwlk  41231  eucrctshift  41411  eucrct2eupth  41413  fusgreghash2wsp  41502  frrusgrord0  41503  av-clwwlkextfrlem1  41509  av-numclwwlkovf2ex  41517  av-numclwwlk1  41528  av-numclwwlk7  41545  ply1mulgsumlem1  41968  ply1mulgsumlem2  41969  nn0onn0ex  42112  nn0enn0ex  42113  fllog2  42160  dignn0fr  42193  digexp  42199  0dig2nn0e  42204  0dig2nn0o  42205  dignn0ehalf  42209  nn0mulfsum  42216  nn0mullong  42217  dpfrac1  42312  dpfrac1OLD  42313