Theorem nn0cn 12394

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11007  ℕ₀cn0 12384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-i2m1 11077

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-nn 12129  df-n0 12385

This theorem is referenced by:  nn0nnaddcl  12415  elnn0nn  12426  nn0sub  12434  difgtsumgt  12437  nn0le2x  12438  nn0n0n1ge2  12452  uzaddcl  12805  fzctr  13543  nn0split  13546  elfzoext  13625  zpnn0elfzo1  13642  ubmelm1fzo  13666  subfzo0  13692  quoremnn0ALT  13761  modmuladdnn0  13822  addmodidr  13827  modfzo0difsn  13850  nn0ennn  13886  expadd  14011  expmul  14014  bernneq  14136  bernneq2  14137  faclbnd  14197  faclbnd4lem3  14202  faclbnd4lem4  14203  faclbnd6  14206  bccmpl  14216  bcn0  14217  bcnn  14219  bcnp1n  14221  bcn2  14226  bcp1m1  14227  bcpasc  14228  bcn2p1  14232  hashfzo0  14337  hashfz0  14339  hashxplem  14340  hashdifsnp1  14413  ccatalpha  14500  ccatws1lenp1b  14528  ccatw2s1len  14532  swrdfv2  14568  swrdspsleq  14572  swrdlsw  14574  pfxmpt  14585  pfxswrd  14612  wrdind  14628  wrd2ind  14629  pfxccatin12lem4  14632  pfxccatin12lem1  14634  pfxccatin12lem2  14637  pfxccatin12  14639  swrdccat3blem  14645  repswswrd  14690  repswrevw  14693  cshwidxmodr  14710  2cshw  14719  2cshwcshw  14732  cshwcshid  14734  swrds2  14847  swrd2lsw  14859  iseraltlem2  15590  fsum0diag2  15690  hashiun  15729  ackbijnn  15735  binom1dif  15740  bcxmas  15742  geolim  15777  geomulcvg  15783  risefacval2  15917  fallfacval2  15918  risefaccl  15922  fallfaccl  15923  fallrisefac  15932  risefacp1  15936  fallfacp1  15937  fallfacfac  15952  bpolysum  15960  fsumkthpow  15963  bpoly4  15966  fsumcube  15967  efaddlem  16000  efexp  16010  eftlub  16018  demoivreALT  16110  nn0ob  16295  divalglem4  16307  modremain  16319  mulgcdr  16461  nn0rppwr  16472  nn0seqcvgd  16481  modprmn0modprm0  16719  coprimeprodsq  16720  coprimeprodsq2  16721  pcexp  16771  dvdsprmpweqle  16798  difsqpwdvds  16799  ramub1lem1  16938  prmop1  16950  smndex2dlinvh  18791  mulgneg2  18987  mndodcongi  19422  oddvdsnn0  19423  sylow1lem1  19477  efgsrel  19613  fincygsubgodd  19993  srgbinomlem4  20114  cnfldmulg  21310  nn0subm  21329  nn0srg  21344  psrbagconf1o  21836  psrass1lem  21839  psrlidm  21869  psrass1  21871  psrcom  21875  mplsubrglem  21911  mplmonmul  21941  psdmul  22051  psdmvr  22054  psropprmul  22120  coe1sclmul  22166  coe1sclmul2  22168  dvnadd  25829  ply1divex  26040  elqaalem2  26226  geolim3  26245  dvradcnv  26328  pserdv2  26338  logtayllem  26566  logtayl  26567  cxpmul2  26596  atantayl3  26847  leibpilem2  26849  leibpi  26850  log2cnv  26852  dmgmaddn0  26931  chpp1  27063  0sgmppw  27107  logexprlim  27134  dchrhash  27180  bcctr  27184  bcmono  27186  bcmax  27187  bcp1ctr  27188  2lgslem1c  27302  2lgslem3a  27305  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  2lgslem3a1  27309  2lgslem3b1  27310  2lgslem3c1  27311  2lgslem3d1  27312  2sqreultlem  27356  2sqreulem2  27361  dchrisumlem1  27398  ostth2lem2  27543  wlklenvclwlk  29599  upgrwlkdvdelem  29681  wwlknp  29788  wwlknlsw  29792  wlkiswwlks1  29812  wlklnwwlkln2lem  29827  wlknwwlksnbij  29833  wwlksnred  29837  wwlksnext  29838  wwlksnredwwlkn  29840  wwlksnextwrd  29842  wwlksnextinj  29844  wwlksnextproplem2  29855  wwlksnextproplem3  29856  wspthsnwspthsnon  29861  clwlkclwwlklem2a1  29936  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  clwlkclwwlklem3  29945  wwlksext2clwwlk  30001  clwwlknonex2lem2  30052  eucrctshift  30187  eucrct2eupth  30189  numclwwlk2lem1lem  30286  numclwwlk1  30305  numclwwlk7  30335  ipasslem1  30775  ipasslem2  30776  dpfrac1  32832  archirngz  33131  nn0constr  33728  pthhashvtx  35101  subfacval2  35160  bccolsum  35712  faclimlem1  35716  poimirlem28  37628  heiborlem4  37794  heiborlem6  37796  lcmineqlem3  42004  facp2  42116  sticksstones7  42125  oddnumth  42284  nicomachus  42285  sumcubes  42286  pell14qrgt0  42832  pell14qrdich  42842  pell1qrge1  42843  2nn0ind  42918  jm2.17a  42933  jm2.18  42961  jm2.19lem3  42964  proot1ex  43169  bcc0  44313  dvradcnv2  44320  binomcxplemrat  44323  binomcxplemnotnn0  44329  fperiodmullem  45285  stoweidlem10  45991  stoweidlem17  45998  stoweidlem26  46007  stirlinglem5  46059  stirlinglem7  46061  etransclem23  46238  cjnpoly  46873  subsubelfzo0  47310  fargshiftfo  47426  fmtnodvds  47528  goldbachthlem1  47529  fmtnofac2lem  47552  fmtnofac1  47554  nn0onn0exALTV  47683  nn0enn0exALTV  47684  isubgr3stgrlem2  47951  nn0mnd  48163  ply1mulgsumlem1  48371  ply1mulgsumlem2  48372  nn0onn0ex  48508  nn0enn0ex  48509  fllog2  48553  dignn0fr  48586  digexp  48592  0dig2nn0e  48597  0dig2nn0o  48598  dignn0ehalf  48602  nn0mulfsum  48609  nn0mullong  48610  itcovalpclem1  48655  itcovalpclem2  48656  itcovalt2lem2lem2  48659  ackval1  48666  ackval2  48667  ackval3  48668