Theorem nn0cn 11721

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

Syntax hints:   → wi 4   ∈ wcel 2050  ℂcc 10335  ℕ₀cn0 11710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-mulcl 10399  ax-i2m1 10405

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-tp 4447  df-op 4449  df-uni 4714  df-iun 4795  df-br 4931  df-opab 4993  df-mpt 5010  df-tr 5032  df-id 5313  df-eprel 5318  df-po 5327  df-so 5328  df-fr 5367  df-we 5369  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-pred 5988  df-ord 6034  df-on 6035  df-lim 6036  df-suc 6037  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-ov 6981  df-om 7399  df-wrecs 7752  df-recs 7814  df-rdg 7852  df-nn 11442  df-n0 11711

This theorem is referenced by:  nn0nnaddcl  11743  elnn0nn  11754  nn0sub  11762  difgtsumgt  11765  nn0n0n1ge2  11777  uzaddcl  12121  fzctr  12838  nn0split  12841  elfzoext  12912  zpnn0elfzo1  12929  ubmelm1fzo  12951  subfzo0  12977  quoremnn0ALT  13043  modmuladdnn0  13101  addmodidr  13106  modfzo0difsn  13129  nn0ennn  13165  expadd  13289  expmul  13292  bernneq  13408  bernneq2  13409  faclbnd  13468  faclbnd4lem3  13473  faclbnd4lem4  13474  faclbnd6  13477  bccmpl  13487  bcn0  13488  bcnn  13490  bcnp1n  13492  bcn2  13497  bcp1m1  13498  bcpasc  13499  bcn2p1  13503  hashfzo0  13607  hashfz0  13609  hashxplem  13610  hashdifsnp1  13668  ccatalpha  13759  ccatws1lenp1b  13787  ccatw2s1len  13791  addlenrevswrdOLD  13832  swrdfv2  13841  swrdspsleq  13845  swrdlsw  13848  pfxmpt  13863  addlenrevpfx  13875  swrd0swrdOLD  13891  pfxswrd  13892  ccats1swrdeqOLD  13908  wrdind  13918  wrdindOLD  13919  wrd2ind  13920  wrd2indOLD  13921  swrdccatin12lem1  13928  pfxccatin12lem1  13930  swrdccatin12lem2bOLD  13931  pfxccatin12lem2  13934  swrdccatin12lem2OLD  13935  pfxccatin12  13937  swrdccatin12OLD  13938  swrdccat3blem  13947  repswswrd  14006  repswrevw  14009  cshwidxmodr  14031  2cshw  14040  2cshwcshw  14052  cshwcshid  14054  swrds2  14167  swrd2lsw  14179  iseraltlem2  14903  fsum0diag2  15001  hashiun  15040  ackbijnn  15046  binom1dif  15051  bcxmas  15053  geolim  15089  geomulcvg  15095  risefacval2  15227  fallfacval2  15228  risefaccl  15232  fallfaccl  15233  fallrisefac  15242  risefacp1  15246  fallfacp1  15247  fallfacfac  15262  bpolysum  15270  fsumkthpow  15273  bpoly4  15276  fsumcube  15277  efaddlem  15309  efexp  15317  eftlub  15325  demoivreALT  15417  nn0ob  15598  divalglem4  15610  modremain  15622  mulgcdr  15757  nn0seqcvgd  15773  modprmn0modprm0  16003  coprimeprodsq  16004  coprimeprodsq2  16005  pcexp  16055  dvdsprmpweqle  16081  difsqpwdvds  16082  ramub1lem1  16221  prmop1  16233  mulgneg2  18048  mndodcongi  18436  oddvdsnn0  18437  sylow1lem1  18487  efgsrel  18621  srgbinomlem4  19019  psrbagconf1o  19871  psrass1lem  19874  psrlidm  19900  psrass1  19902  psrcom  19906  mplsubrglem  19936  mplmonmul  19961  psropprmul  20112  coe1sclmul  20156  coe1sclmul2  20158  cnfldmulg  20282  nn0subm  20305  nn0srg  20320  dvnadd  24232  ply1divex  24436  elqaalem2  24615  geolim3  24634  dvradcnv  24715  pserdv2  24724  logtayllem  24946  logtayl  24947  cxpmul2  24976  atantayl3  25221  leibpilem2  25224  leibpi  25225  log2cnv  25227  dmgmaddn0  25305  chpp1  25437  0sgmppw  25479  logexprlim  25506  dchrhash  25552  bcctr  25556  bcmono  25558  bcmax  25559  bcp1ctr  25560  2lgslem1c  25674  2lgslem3a  25677  2lgslem3b  25678  2lgslem3c  25679  2lgslem3d  25680  2lgslem3a1  25681  2lgslem3b1  25682  2lgslem3c1  25683  2lgslem3d1  25684  2sqreultlem  25728  2sqreulem2  25733  dchrisumlem1  25770  ostth2lem2  25915  wlklenvclwlk  27142  upgrwlkdvdelem  27228  wwlknp  27332  wwlknlsw  27336  wlkiswwlks1  27356  wlklnwwlkln2lem  27372  wlknwwlksnbij  27378  wwlksnred  27382  wwlksnredOLD  27383  wwlksnext  27384  wwlksnredwwlkn  27387  wwlksnredwwlknOLD  27388  wwlksnextwrd  27391  wwlksnextinj  27393  wwlksnextwrdOLD  27396  wwlksnextinjOLD  27398  wwlksnextproplem2  27414  wwlksnextproplem2OLD  27415  wwlksnextproplem3  27416  wwlksnextproplem3OLD  27417  wspthsnwspthsnon  27425  clwlkclwwlklem2a1  27501  clwlkclwwlklem2a4  27506  clwlkclwwlklem2a  27507  clwlkclwwlklem2  27509  clwlkclwwlklem3  27510  wwlksext2clwwlk  27583  clwwlknonex2lem2  27639  eucrctshift  27776  eucrct2eupthOLD  27779  eucrct2eupth  27780  numclwwlk2lem1lem  27879  numclwwlk1  27912  numclwwlk7  27951  ipasslem1  28388  ipasslem2  28389  dpfrac1  30317  archirngz  30484  subfacval2  32019  bccolsum  32491  faclimlem1  32495  poimirlem28  34361  heiborlem4  34534  heiborlem6  34536  nn0rppwr  38614  pell14qrgt0  38852  pell14qrdich  38862  pell1qrge1  38863  2nn0ind  38938  jm2.17a  38953  jm2.18  38981  jm2.19lem3  38984  proot1ex  39197  fincygsubgodd  40047  bcc0  40088  dvradcnv2  40095  binomcxplemrat  40098  binomcxplemnotnn0  40104  fperiodmullem  41000  stoweidlem10  41727  stoweidlem17  41734  stoweidlem26  41743  stirlinglem5  41795  stirlinglem7  41797  etransclem23  41974  subsubelfzo0  42933  fargshiftfo  42975  fmtnodvds  43075  goldbachthlem1  43076  fmtnofac2lem  43099  fmtnofac1  43101  nn0onn0exALTV  43233  nn0enn0exALTV  43234  ply1mulgsumlem1  43808  ply1mulgsumlem2  43809  nn0onn0ex  43952  nn0enn0ex  43953  fllog2  43997  dignn0fr  44030  digexp  44036  0dig2nn0e  44041  0dig2nn0o  44042  dignn0ehalf  44046  nn0mulfsum  44053  nn0mullong  44054