Theorem nn0cn 12432

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 11058  ℕ₀cn0 12422

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-mulcl 11122  ax-i2m1 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-nn 12163  df-n0 12423

This theorem is referenced by:  nn0nnaddcl  12453  elnn0nn  12464  nn0sub  12472  difgtsumgt  12475  nn0n0n1ge2  12489  uzaddcl  12838  fzctr  13563  nn0split  13566  elfzoext  13639  zpnn0elfzo1  13656  ubmelm1fzo  13678  subfzo0  13704  quoremnn0ALT  13772  modmuladdnn0  13830  addmodidr  13835  modfzo0difsn  13858  nn0ennn  13894  expadd  14020  expmul  14023  bernneq  14142  bernneq2  14143  faclbnd  14200  faclbnd4lem3  14205  faclbnd4lem4  14206  faclbnd6  14209  bccmpl  14219  bcn0  14220  bcnn  14222  bcnp1n  14224  bcn2  14229  bcp1m1  14230  bcpasc  14231  bcn2p1  14235  hashfzo0  14340  hashfz0  14342  hashxplem  14343  hashdifsnp1  14407  ccatalpha  14493  ccatws1lenp1b  14521  ccatw2s1len  14525  swrdfv2  14561  swrdspsleq  14565  swrdlsw  14567  pfxmpt  14578  addlenrevpfx  14590  pfxswrd  14606  wrdind  14622  wrd2ind  14623  pfxccatin12lem4  14626  pfxccatin12lem1  14628  pfxccatin12lem2  14631  pfxccatin12  14633  swrdccat3blem  14639  repswswrd  14684  repswrevw  14687  cshwidxmodr  14704  2cshw  14713  2cshwcshw  14726  cshwcshid  14728  swrds2  14841  swrd2lsw  14853  iseraltlem2  15579  fsum0diag2  15679  hashiun  15718  ackbijnn  15724  binom1dif  15729  bcxmas  15731  geolim  15766  geomulcvg  15772  risefacval2  15904  fallfacval2  15905  risefaccl  15909  fallfaccl  15910  fallrisefac  15919  risefacp1  15923  fallfacp1  15924  fallfacfac  15939  bpolysum  15947  fsumkthpow  15950  bpoly4  15953  fsumcube  15954  efaddlem  15986  efexp  15994  eftlub  16002  demoivreALT  16094  nn0ob  16277  divalglem4  16289  modremain  16301  mulgcdr  16442  nn0seqcvgd  16457  modprmn0modprm0  16690  coprimeprodsq  16691  coprimeprodsq2  16692  pcexp  16742  dvdsprmpweqle  16769  difsqpwdvds  16770  ramub1lem1  16909  prmop1  16921  smndex2dlinvh  18741  mulgneg2  18924  mndodcongi  19339  oddvdsnn0  19340  sylow1lem1  19394  efgsrel  19530  fincygsubgodd  19905  srgbinomlem4  19974  cnfldmulg  20866  nn0subm  20889  nn0srg  20904  psrbagconf1o  21375  psrbagconf1oOLD  21376  psrass1lemOLD  21379  psrass1lem  21382  psrlidm  21409  psrass1  21411  psrcom  21415  mplsubrglem  21447  mplmonmul  21474  psropprmul  21646  coe1sclmul  21690  coe1sclmul2  21692  dvnadd  25330  ply1divex  25538  elqaalem2  25717  geolim3  25736  dvradcnv  25817  pserdv2  25826  logtayllem  26051  logtayl  26052  cxpmul2  26081  atantayl3  26326  leibpilem2  26328  leibpi  26329  log2cnv  26331  dmgmaddn0  26409  chpp1  26541  0sgmppw  26583  logexprlim  26610  dchrhash  26656  bcctr  26660  bcmono  26662  bcmax  26663  bcp1ctr  26664  2lgslem1c  26778  2lgslem3a  26781  2lgslem3b  26782  2lgslem3c  26783  2lgslem3d  26784  2lgslem3a1  26785  2lgslem3b1  26786  2lgslem3c1  26787  2lgslem3d1  26788  2sqreultlem  26832  2sqreulem2  26837  dchrisumlem1  26874  ostth2lem2  27019  wlklenvclwlk  28666  upgrwlkdvdelem  28747  wwlknp  28851  wwlknlsw  28855  wlkiswwlks1  28875  wlklnwwlkln2lem  28890  wlknwwlksnbij  28896  wwlksnred  28900  wwlksnext  28901  wwlksnredwwlkn  28903  wwlksnextwrd  28905  wwlksnextinj  28907  wwlksnextproplem2  28918  wwlksnextproplem3  28919  wspthsnwspthsnon  28924  clwlkclwwlklem2a1  28999  clwlkclwwlklem2a4  29004  clwlkclwwlklem2a  29005  clwlkclwwlklem2  29007  clwlkclwwlklem3  29008  wwlksext2clwwlk  29064  clwwlknonex2lem2  29115  eucrctshift  29250  eucrct2eupth  29252  numclwwlk2lem1lem  29349  numclwwlk1  29368  numclwwlk7  29398  ipasslem1  29836  ipasslem2  29837  dpfrac1  31818  archirngz  32095  pthhashvtx  33808  subfacval2  33868  bccolsum  34398  faclimlem1  34402  poimirlem28  36179  heiborlem4  36346  heiborlem6  36348  lcmineqlem3  40561  facp2  40624  sticksstones7  40633  fac2xp3  40685  factwoffsmonot  40688  nn0rppwr  40877  pell14qrgt0  41240  pell14qrdich  41250  pell1qrge1  41251  2nn0ind  41327  jm2.17a  41342  jm2.18  41370  jm2.19lem3  41373  proot1ex  41586  bcc0  42742  dvradcnv2  42749  binomcxplemrat  42752  binomcxplemnotnn0  42758  fperiodmullem  43658  stoweidlem10  44371  stoweidlem17  44378  stoweidlem26  44387  stirlinglem5  44439  stirlinglem7  44441  etransclem23  44618  subsubelfzo0  45678  fargshiftfo  45754  fmtnodvds  45856  goldbachthlem1  45857  fmtnofac2lem  45880  fmtnofac1  45882  nn0onn0exALTV  46011  nn0enn0exALTV  46012  nn0mnd  46233  ply1mulgsumlem1  46587  ply1mulgsumlem2  46588  nn0onn0ex  46729  nn0enn0ex  46730  fllog2  46774  dignn0fr  46807  digexp  46813  0dig2nn0e  46818  0dig2nn0o  46819  dignn0ehalf  46823  nn0mulfsum  46830  nn0mullong  46831  itcovalpclem1  46876  itcovalpclem2  46877  itcovalt2lem2lem2  46880  ackval1  46887  ackval2  46888  ackval3  46889