Theorem nn0cn 12491

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

Syntax hints:   → wi 4   ∈ wcel 2142  ℂcc 11071  ℕ₀cn0 12481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-mulcl 11135  ax-i2m1 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-nn 12211  df-n0 12482

This theorem is referenced by:  nn0nnaddcl  12512  elnn0nn  12523  nn0sub  12531  difgtsumgt  12534  nn0le2x  12535  nn0n0n1ge2  12549  uzaddcl  12905  fzctr  13645  nn0split  13648  elfzoext  13728  zpnn0elfzo1  13745  ubmelm1fzo  13769  subfzo0  13798  quoremnn0ALT  13867  modmuladdnn0  13928  addmodidr  13933  modfzo0difsn  13956  nn0ennn  13992  expadd  14117  expmul  14120  bernneq  14242  bernneq2  14243  faclbnd  14303  faclbnd4lem3  14308  faclbnd4lem4  14309  faclbnd6  14312  bccmpl  14322  bcn0  14323  bcnn  14325  bcnp1n  14327  bcn2  14332  bcp1m1  14333  bcpasc  14334  bcn2p1  14338  hashfzo0  14443  hashfz0  14445  hashxplem  14446  hashdifsnp1  14519  ccatalpha  14607  ccatws1lenp1b  14635  ccatw2s1len  14639  swrdfv2  14675  swrdspsleq  14679  swrdlsw  14681  pfxmpt  14692  pfxswrd  14719  wrdind  14735  wrd2ind  14736  pfxccatin12lem4  14739  pfxccatin12lem1  14741  pfxccatin12lem2  14744  pfxccatin12  14746  swrdccat3blem  14752  repswswrd  14797  repswrevw  14800  cshwidxmodr  14817  2cshw  14826  2cshwcshw  14838  cshwcshid  14840  swrds2  14953  swrd2lsw  14965  iseraltlem2  15710  fsum0diag2  15810  hashiun  15850  ackbijnn  15858  binom1dif  15863  bcxmas  15865  geolim  15900  geomulcvg  15906  risefacval2  16040  fallfacval2  16041  risefaccl  16045  fallfaccl  16046  fallrisefac  16055  risefacp1  16059  fallfacp1  16060  fallfacfac  16075  bpolysum  16083  fsumkthpow  16086  bpoly4  16089  fsumcube  16090  efaddlem  16123  efexp  16133  eftlub  16141  demoivreALT  16233  nn0ob  16418  divalglem4  16430  modremain  16442  mulgcdr  16584  nn0rppwr  16595  nn0seqcvgd  16604  modprmn0modprm0  16843  coprimeprodsq  16844  coprimeprodsq2  16845  pcexp  16895  dvdsprmpweqle  16922  difsqpwdvds  16923  ramub1lem1  17062  prmop1  17074  chnccat  18658  smndex2dlinvh  18954  mulgneg2  19150  mndodcongi  19583  oddvdsnn0  19584  sylow1lem1  19638  efgsrel  19774  fincygsubgodd  20154  srgbinomlem4  20275  cnfldmulg  21453  nn0subm  21471  nn0srg  21486  psrbagconf1o  21978  psrass1lem  21982  psrlidm  22010  psrass1  22012  psrcom  22016  mplsubrglem  22052  mplmonmul  22086  psdmul  22228  psdmvr  22231  psropprmul  22296  coe1sclmul  22342  coe1sclmul2  22344  dvnadd  25988  ply1divex  26194  elqaalem2  26381  geolim3  26400  dvradcnv  26481  pserdv2  26490  logtayllem  26721  logtayl  26722  cxpmul2  26751  atantayl3  27001  leibpilem2  27003  leibpi  27004  log2cnv  27006  dmgmaddn0  27084  chpp1  27216  0sgmppw  27259  logexprlim  27286  dchrhash  27332  bcctr  27336  bcmono  27338  bcmax  27339  bcp1ctr  27340  2lgslem1c  27454  2lgslem3a  27457  2lgslem3b  27458  2lgslem3c  27459  2lgslem3d  27460  2lgslem3a1  27461  2lgslem3b1  27462  2lgslem3c1  27463  2lgslem3d1  27464  2sqreultlem  27508  2sqreulem2  27513  dchrisumlem1  27550  ostth2lem2  27695  wlklenvclwlk  29851  upgrwlkdvdelem  29933  wwlknp  30040  wwlknlsw  30044  wlkiswwlks1  30064  wlklnwwlkln2lem  30079  wlknwwlksnbij  30085  wwlksnred  30089  wwlksnext  30090  wwlksnredwwlkn  30092  wwlksnextwrd  30094  wwlksnextinj  30096  wwlksnextproplem2  30107  wwlksnextproplem3  30108  wspthsnwspthsnon  30113  clwlkclwwlklem2a1  30191  clwlkclwwlklem2a4  30196  clwlkclwwlklem2a  30197  clwlkclwwlklem2  30199  clwlkclwwlklem3  30200  wwlksext2clwwlk  30256  clwwlknonex2lem2  30307  eucrctshift  30442  eucrct2eupth  30444  numclwwlk2lem1lem  30541  numclwwlk1  30560  numclwwlk7  30590  ipasslem1  31031  ipasslem2  31032  dpfrac1  33066  archirngz  33366  psrmonmul  33844  nn0constr  34055  pthhashvtx  35475  subfacval2  35534  bccolsum  36086  faclimlem1  36090  poimirlem28  38144  heiborlem4  38310  heiborlem6  38312  lcmineqlem3  42645  facp2  42757  sticksstones7  42766  oddnumth  42917  nicomachus  42918  sumcubes  42919  pell14qrgt0  43433  pell14qrdich  43443  pell1qrge1  43444  2nn0ind  43519  jm2.17a  43534  jm2.18  43562  jm2.19lem3  43565  proot1ex  43770  bcc0  44913  dvradcnv2  44920  binomcxplemrat  44923  binomcxplemnotnn0  44929  fperiodmullem  45879  stoweidlem10  46581  stoweidlem17  46588  stoweidlem26  46597  stirlinglem5  46649  stirlinglem7  46651  etransclem23  46828  cjnpoly  47480  subsubelfzo0  47918  fargshiftfo  48045  fmtnodvds  48150  goldbachthlem1  48151  fmtnofac2lem  48174  fmtnofac1  48176  nn0onn0exALTV  48318  nn0enn0exALTV  48319  isubgr3stgrlem2  48586  nn0mnd  48798  ply1mulgsumlem1  49005  ply1mulgsumlem2  49006  nn0onn0ex  49142  nn0enn0ex  49143  fllog2  49187  dignn0fr  49220  digexp  49226  0dig2nn0e  49231  0dig2nn0o  49232  dignn0ehalf  49236  nn0mulfsum  49243  nn0mullong  49244  itcovalpclem1  49289  itcovalpclem2  49290  itcovalt2lem2lem2  49293  ackval1  49300  ackval2  49301  ackval3  49302