Theorem nn0cn 11910

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10537  ℕ₀cn0 11900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601  ax-i2m1 10607

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-nn 11641  df-n0 11901

This theorem is referenced by:  nn0nnaddcl  11931  elnn0nn  11942  nn0sub  11950  difgtsumgt  11953  nn0n0n1ge2  11965  uzaddcl  12307  fzctr  13022  nn0split  13025  elfzoext  13097  zpnn0elfzo1  13114  ubmelm1fzo  13136  subfzo0  13162  quoremnn0ALT  13228  modmuladdnn0  13286  addmodidr  13291  modfzo0difsn  13314  nn0ennn  13350  expadd  13474  expmul  13477  bernneq  13593  bernneq2  13594  faclbnd  13653  faclbnd4lem3  13658  faclbnd4lem4  13659  faclbnd6  13662  bccmpl  13672  bcn0  13673  bcnn  13675  bcnp1n  13677  bcn2  13682  bcp1m1  13683  bcpasc  13684  bcn2p1  13688  hashfzo0  13794  hashfz0  13796  hashxplem  13797  hashdifsnp1  13857  ccatalpha  13949  ccatws1lenp1b  13977  ccatw2s1len  13982  swrdfv2  14025  swrdspsleq  14029  swrdlsw  14031  pfxmpt  14042  addlenrevpfx  14054  pfxswrd  14070  wrdind  14086  wrd2ind  14087  pfxccatin12lem4  14090  pfxccatin12lem1  14092  pfxccatin12lem2  14095  pfxccatin12  14097  swrdccat3blem  14103  repswswrd  14148  repswrevw  14151  cshwidxmodr  14168  2cshw  14177  2cshwcshw  14189  cshwcshid  14191  swrds2  14304  swrd2lsw  14316  iseraltlem2  15041  fsum0diag2  15140  hashiun  15179  ackbijnn  15185  binom1dif  15190  bcxmas  15192  geolim  15228  geomulcvg  15234  risefacval2  15366  fallfacval2  15367  risefaccl  15371  fallfaccl  15372  fallrisefac  15381  risefacp1  15385  fallfacp1  15386  fallfacfac  15401  bpolysum  15409  fsumkthpow  15412  bpoly4  15415  fsumcube  15416  efaddlem  15448  efexp  15456  eftlub  15464  demoivreALT  15556  nn0ob  15737  divalglem4  15749  modremain  15761  mulgcdr  15900  nn0seqcvgd  15916  modprmn0modprm0  16146  coprimeprodsq  16147  coprimeprodsq2  16148  pcexp  16198  dvdsprmpweqle  16224  difsqpwdvds  16225  ramub1lem1  16364  prmop1  16376  smndex2dlinvh  18084  mulgneg2  18263  mndodcongi  18673  oddvdsnn0  18674  sylow1lem1  18725  efgsrel  18862  fincygsubgodd  19236  srgbinomlem4  19295  psrbagconf1o  20156  psrass1lem  20159  psrlidm  20185  psrass1  20187  psrcom  20191  mplsubrglem  20221  mplmonmul  20247  psropprmul  20408  coe1sclmul  20452  coe1sclmul2  20454  cnfldmulg  20579  nn0subm  20602  nn0srg  20617  dvnadd  24528  ply1divex  24732  elqaalem2  24911  geolim3  24930  dvradcnv  25011  pserdv2  25020  logtayllem  25244  logtayl  25245  cxpmul2  25274  atantayl3  25519  leibpilem2  25521  leibpi  25522  log2cnv  25524  dmgmaddn0  25602  chpp1  25734  0sgmppw  25776  logexprlim  25803  dchrhash  25849  bcctr  25853  bcmono  25855  bcmax  25856  bcp1ctr  25857  2lgslem1c  25971  2lgslem3a  25974  2lgslem3b  25975  2lgslem3c  25976  2lgslem3d  25977  2lgslem3a1  25978  2lgslem3b1  25979  2lgslem3c1  25980  2lgslem3d1  25981  2sqreultlem  26025  2sqreulem2  26030  dchrisumlem1  26067  ostth2lem2  26212  wlklenvclwlk  27438  wlklenvclwlkOLD  27439  upgrwlkdvdelem  27519  wwlknp  27623  wwlknlsw  27627  wlkiswwlks1  27647  wlklnwwlkln2lem  27662  wlknwwlksnbij  27668  wwlksnred  27672  wwlksnext  27673  wwlksnredwwlkn  27675  wwlksnextwrd  27677  wwlksnextinj  27679  wwlksnextproplem2  27691  wwlksnextproplem3  27692  wspthsnwspthsnon  27697  clwlkclwwlklem2a1  27772  clwlkclwwlklem2a4  27777  clwlkclwwlklem2a  27778  clwlkclwwlklem2  27780  clwlkclwwlklem3  27781  wwlksext2clwwlk  27838  clwwlknonex2lem2  27889  eucrctshift  28024  eucrct2eupth  28026  numclwwlk2lem1lem  28123  numclwwlk1  28142  numclwwlk7  28172  ipasslem1  28610  ipasslem2  28611  dpfrac1  30570  archirngz  30820  pthhashvtx  32376  subfacval2  32436  bccolsum  32973  faclimlem1  32977  poimirlem28  34922  heiborlem4  35094  heiborlem6  35096  fac2xp3  39101  facp2  39102  factwoffsmonot  39105  nn0rppwr  39189  pell14qrgt0  39463  pell14qrdich  39473  pell1qrge1  39474  2nn0ind  39549  jm2.17a  39564  jm2.18  39592  jm2.19lem3  39595  proot1ex  39808  bcc0  40679  dvradcnv2  40686  binomcxplemrat  40689  binomcxplemnotnn0  40695  fperiodmullem  41577  stoweidlem10  42302  stoweidlem17  42309  stoweidlem26  42318  stirlinglem5  42370  stirlinglem7  42372  etransclem23  42549  subsubelfzo0  43533  fargshiftfo  43609  fmtnodvds  43713  goldbachthlem1  43714  fmtnofac2lem  43737  fmtnofac1  43739  nn0onn0exALTV  43871  nn0enn0exALTV  43872  nn0mnd  44093  ply1mulgsumlem1  44447  ply1mulgsumlem2  44448  nn0onn0ex  44590  nn0enn0ex  44591  fllog2  44635  dignn0fr  44668  digexp  44674  0dig2nn0e  44679  0dig2nn0o  44680  dignn0ehalf  44684  nn0mulfsum  44691  nn0mullong  44692