Theorem nn0cn 12409

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11022  ℕ₀cn0 12399

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-mulcl 11086  ax-i2m1 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12144  df-n0 12400

This theorem is referenced by:  nn0nnaddcl  12430  elnn0nn  12441  nn0sub  12449  difgtsumgt  12452  nn0le2x  12453  nn0n0n1ge2  12467  uzaddcl  12815  fzctr  13554  nn0split  13557  elfzoext  13636  zpnn0elfzo1  13653  ubmelm1fzo  13677  subfzo0  13706  quoremnn0ALT  13775  modmuladdnn0  13836  addmodidr  13841  modfzo0difsn  13864  nn0ennn  13900  expadd  14025  expmul  14028  bernneq  14150  bernneq2  14151  faclbnd  14211  faclbnd4lem3  14216  faclbnd4lem4  14217  faclbnd6  14220  bccmpl  14230  bcn0  14231  bcnn  14233  bcnp1n  14235  bcn2  14240  bcp1m1  14241  bcpasc  14242  bcn2p1  14246  hashfzo0  14351  hashfz0  14353  hashxplem  14354  hashdifsnp1  14427  ccatalpha  14515  ccatws1lenp1b  14543  ccatw2s1len  14547  swrdfv2  14583  swrdspsleq  14587  swrdlsw  14589  pfxmpt  14600  pfxswrd  14627  wrdind  14643  wrd2ind  14644  pfxccatin12lem4  14647  pfxccatin12lem1  14649  pfxccatin12lem2  14652  pfxccatin12  14654  swrdccat3blem  14660  repswswrd  14705  repswrevw  14708  cshwidxmodr  14725  2cshw  14734  2cshwcshw  14746  cshwcshid  14748  swrds2  14861  swrd2lsw  14873  iseraltlem2  15604  fsum0diag2  15704  hashiun  15743  ackbijnn  15749  binom1dif  15754  bcxmas  15756  geolim  15791  geomulcvg  15797  risefacval2  15931  fallfacval2  15932  risefaccl  15936  fallfaccl  15937  fallrisefac  15946  risefacp1  15950  fallfacp1  15951  fallfacfac  15966  bpolysum  15974  fsumkthpow  15977  bpoly4  15980  fsumcube  15981  efaddlem  16014  efexp  16024  eftlub  16032  demoivreALT  16124  nn0ob  16309  divalglem4  16321  modremain  16333  mulgcdr  16475  nn0rppwr  16486  nn0seqcvgd  16495  modprmn0modprm0  16733  coprimeprodsq  16734  coprimeprodsq2  16735  pcexp  16785  dvdsprmpweqle  16812  difsqpwdvds  16813  ramub1lem1  16952  prmop1  16964  chnccat  18547  smndex2dlinvh  18840  mulgneg2  19036  mndodcongi  19470  oddvdsnn0  19471  sylow1lem1  19525  efgsrel  19661  fincygsubgodd  20041  srgbinomlem4  20162  cnfldmulg  21356  nn0subm  21375  nn0srg  21390  psrbagconf1o  21883  psrass1lem  21886  psrlidm  21915  psrass1  21917  psrcom  21921  mplsubrglem  21957  mplmonmul  21989  psdmul  22107  psdmvr  22110  psropprmul  22176  coe1sclmul  22222  coe1sclmul2  22224  dvnadd  25885  ply1divex  26096  elqaalem2  26282  geolim3  26301  dvradcnv  26384  pserdv2  26394  logtayllem  26622  logtayl  26623  cxpmul2  26652  atantayl3  26903  leibpilem2  26905  leibpi  26906  log2cnv  26908  dmgmaddn0  26987  chpp1  27119  0sgmppw  27163  logexprlim  27190  dchrhash  27236  bcctr  27240  bcmono  27242  bcmax  27243  bcp1ctr  27244  2lgslem1c  27358  2lgslem3a  27361  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  2lgslem3a1  27365  2lgslem3b1  27366  2lgslem3c1  27367  2lgslem3d1  27368  2sqreultlem  27412  2sqreulem2  27417  dchrisumlem1  27454  ostth2lem2  27599  wlklenvclwlk  29676  upgrwlkdvdelem  29758  wwlknp  29865  wwlknlsw  29869  wlkiswwlks1  29889  wlklnwwlkln2lem  29904  wlknwwlksnbij  29910  wwlksnred  29914  wwlksnext  29915  wwlksnredwwlkn  29917  wwlksnextwrd  29919  wwlksnextinj  29921  wwlksnextproplem2  29932  wwlksnextproplem3  29933  wspthsnwspthsnon  29938  clwlkclwwlklem2a1  30016  clwlkclwwlklem2a4  30021  clwlkclwwlklem2a  30022  clwlkclwwlklem2  30024  clwlkclwwlklem3  30025  wwlksext2clwwlk  30081  clwwlknonex2lem2  30132  eucrctshift  30267  eucrct2eupth  30269  numclwwlk2lem1lem  30366  numclwwlk1  30385  numclwwlk7  30415  ipasslem1  30855  ipasslem2  30856  dpfrac1  32922  archirngz  33220  nn0constr  33867  pthhashvtx  35271  subfacval2  35330  bccolsum  35882  faclimlem1  35886  poimirlem28  37788  heiborlem4  37954  heiborlem6  37956  lcmineqlem3  42224  facp2  42336  sticksstones7  42345  oddnumth  42508  nicomachus  42509  sumcubes  42510  pell14qrgt0  43043  pell14qrdich  43053  pell1qrge1  43054  2nn0ind  43129  jm2.17a  43144  jm2.18  43172  jm2.19lem3  43175  proot1ex  43380  bcc0  44523  dvradcnv2  44530  binomcxplemrat  44533  binomcxplemnotnn0  44539  fperiodmullem  45493  stoweidlem10  46196  stoweidlem17  46203  stoweidlem26  46212  stirlinglem5  46264  stirlinglem7  46266  etransclem23  46443  cjnpoly  47077  subsubelfzo0  47514  fargshiftfo  47630  fmtnodvds  47732  goldbachthlem1  47733  fmtnofac2lem  47756  fmtnofac1  47758  nn0onn0exALTV  47887  nn0enn0exALTV  47888  isubgr3stgrlem2  48155  nn0mnd  48367  ply1mulgsumlem1  48574  ply1mulgsumlem2  48575  nn0onn0ex  48711  nn0enn0ex  48712  fllog2  48756  dignn0fr  48789  digexp  48795  0dig2nn0e  48800  0dig2nn0o  48801  dignn0ehalf  48805  nn0mulfsum  48812  nn0mullong  48813  itcovalpclem1  48858  itcovalpclem2  48859  itcovalt2lem2lem2  48862  ackval1  48869  ackval2  48870  ackval3  48871