Theorem nn0cn 12441

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11030  ℕ₀cn0 12431

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 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-mulcl 11094  ax-i2m1 11100

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-nn 12169  df-n0 12432

This theorem is referenced by:  nn0nnaddcl  12462  elnn0nn  12473  nn0sub  12481  difgtsumgt  12484  nn0le2x  12485  nn0n0n1ge2  12499  uzaddcl  12848  fzctr  13588  nn0split  13591  elfzoext  13671  zpnn0elfzo1  13688  ubmelm1fzo  13712  subfzo0  13741  quoremnn0ALT  13810  modmuladdnn0  13871  addmodidr  13876  modfzo0difsn  13899  nn0ennn  13935  expadd  14060  expmul  14063  bernneq  14185  bernneq2  14186  faclbnd  14246  faclbnd4lem3  14251  faclbnd4lem4  14252  faclbnd6  14255  bccmpl  14265  bcn0  14266  bcnn  14268  bcnp1n  14270  bcn2  14275  bcp1m1  14276  bcpasc  14277  bcn2p1  14281  hashfzo0  14386  hashfz0  14388  hashxplem  14389  hashdifsnp1  14462  ccatalpha  14550  ccatws1lenp1b  14578  ccatw2s1len  14582  swrdfv2  14618  swrdspsleq  14622  swrdlsw  14624  pfxmpt  14635  pfxswrd  14662  wrdind  14678  wrd2ind  14679  pfxccatin12lem4  14682  pfxccatin12lem1  14684  pfxccatin12lem2  14687  pfxccatin12  14689  swrdccat3blem  14695  repswswrd  14740  repswrevw  14743  cshwidxmodr  14760  2cshw  14769  2cshwcshw  14781  cshwcshid  14783  swrds2  14896  swrd2lsw  14908  iseraltlem2  15639  fsum0diag2  15739  hashiun  15779  ackbijnn  15787  binom1dif  15792  bcxmas  15794  geolim  15829  geomulcvg  15835  risefacval2  15969  fallfacval2  15970  risefaccl  15974  fallfaccl  15975  fallrisefac  15984  risefacp1  15988  fallfacp1  15989  fallfacfac  16004  bpolysum  16012  fsumkthpow  16015  bpoly4  16018  fsumcube  16019  efaddlem  16052  efexp  16062  eftlub  16070  demoivreALT  16162  nn0ob  16347  divalglem4  16359  modremain  16371  mulgcdr  16513  nn0rppwr  16524  nn0seqcvgd  16533  modprmn0modprm0  16772  coprimeprodsq  16773  coprimeprodsq2  16774  pcexp  16824  dvdsprmpweqle  16851  difsqpwdvds  16852  ramub1lem1  16991  prmop1  17003  chnccat  18586  smndex2dlinvh  18882  mulgneg2  19078  mndodcongi  19512  oddvdsnn0  19513  sylow1lem1  19567  efgsrel  19703  fincygsubgodd  20083  srgbinomlem4  20204  cnfldmulg  21396  nn0subm  21415  nn0srg  21430  psrbagconf1o  21922  psrass1lem  21925  psrlidm  21953  psrass1  21955  psrcom  21959  mplsubrglem  21995  mplmonmul  22027  psdmul  22145  psdmvr  22148  psropprmul  22214  coe1sclmul  22260  coe1sclmul2  22262  dvnadd  25909  ply1divex  26115  elqaalem2  26300  geolim3  26319  dvradcnv  26402  pserdv2  26411  logtayllem  26639  logtayl  26640  cxpmul2  26669  atantayl3  26919  leibpilem2  26921  leibpi  26922  log2cnv  26924  dmgmaddn0  27003  chpp1  27135  0sgmppw  27178  logexprlim  27205  dchrhash  27251  bcctr  27255  bcmono  27257  bcmax  27258  bcp1ctr  27259  2lgslem1c  27373  2lgslem3a  27376  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  2lgslem3a1  27380  2lgslem3b1  27381  2lgslem3c1  27382  2lgslem3d1  27383  2sqreultlem  27427  2sqreulem2  27432  dchrisumlem1  27469  ostth2lem2  27614  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  32969  archirngz  33268  psrmonmul  33712  nn0constr  33924  pthhashvtx  35329  subfacval2  35388  bccolsum  35940  faclimlem1  35944  poimirlem28  37986  heiborlem4  38152  heiborlem6  38154  lcmineqlem3  42487  facp2  42599  sticksstones7  42608  oddnumth  42760  nicomachus  42761  sumcubes  42762  pell14qrgt0  43308  pell14qrdich  43318  pell1qrge1  43319  2nn0ind  43394  jm2.17a  43409  jm2.18  43437  jm2.19lem3  43440  proot1ex  43645  bcc0  44788  dvradcnv2  44795  binomcxplemrat  44798  binomcxplemnotnn0  44804  fperiodmullem  45757  stoweidlem10  46459  stoweidlem17  46466  stoweidlem26  46475  stirlinglem5  46527  stirlinglem7  46529  etransclem23  46706  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