Theorem nn0cn 12513

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℂcc 11097  ℕ₀cn0 12503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-mulcl 11161  ax-i2m1 11167

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-nn 12233  df-n0 12504

This theorem is referenced by:  nn0nnaddcl  12534  elnn0nn  12545  nn0sub  12553  difgtsumgt  12556  nn0le2x  12557  nn0n0n1ge2  12571  uzaddcl  12927  fzctr  13667  nn0split  13670  elfzoext  13750  zpnn0elfzo1  13767  ubmelm1fzo  13791  subfzo0  13820  quoremnn0ALT  13889  modmuladdnn0  13950  addmodidr  13955  modfzo0difsn  13978  nn0ennn  14014  expadd  14139  expmul  14142  bernneq  14264  bernneq2  14265  faclbnd  14325  faclbnd4lem3  14330  faclbnd4lem4  14331  faclbnd6  14334  bccmpl  14344  bcn0  14345  bcnn  14347  bcnp1n  14349  bcn2  14354  bcp1m1  14355  bcpasc  14356  bcn2p1  14360  hashfzo0  14466  hashfz0  14468  hashxplem  14469  hashdifsnp1  14542  ccatalpha  14630  ccatws1lenp1b  14658  ccatw2s1len  14662  swrdfv2  14698  swrdspsleq  14702  swrdlsw  14704  pfxmpt  14715  pfxswrd  14742  wrdind  14758  wrd2ind  14759  pfxccatin12lem4  14762  pfxccatin12lem1  14764  pfxccatin12lem2  14767  pfxccatin12  14769  swrdccat3blem  14775  repswswrd  14820  repswrevw  14823  cshwidxmodr  14840  2cshw  14849  2cshwcshw  14861  cshwcshid  14863  swrds2  14976  swrd2lsw  14988  iseraltlem2  15733  fsum0diag2  15833  hashiun  15873  ackbijnn  15881  binom1dif  15886  bcxmas  15888  geolim  15923  geomulcvg  15929  risefacval2  16063  fallfacval2  16064  risefaccl  16068  fallfaccl  16069  fallrisefac  16078  risefacp1  16082  fallfacp1  16083  fallfacfac  16098  bpolysum  16106  fsumkthpow  16109  bpoly4  16112  fsumcube  16113  efaddlem  16146  efexp  16156  eftlub  16164  demoivreALT  16256  nn0ob  16441  divalglem4  16453  modremain  16465  mulgcdr  16607  nn0rppwr  16618  nn0seqcvgd  16627  modprmn0modprm0  16866  coprimeprodsq  16867  coprimeprodsq2  16868  pcexp  16918  dvdsprmpweqle  16945  difsqpwdvds  16946  ramub1lem1  17085  prmop1  17097  chnccat  18681  smndex2dlinvh  18978  mulgneg2  19173  mndodcongi  19612  oddvdsnn0  19613  sylow1lem1  19667  efgsrel  19803  fincygsubgodd  20183  srgbinomlem4  20310  cnfldmulg  21522  nn0subm  21540  nn0srg  21555  psrbagconf1o  22047  psrass1lem  22051  psrlidm  22079  psrass1  22081  psrcom  22085  mplsubrglem  22121  mplmonmul  22155  psdmul  22297  psdmvr  22300  psropprmul  22365  coe1sclmul  22411  coe1sclmul2  22413  dvnadd  26056  ply1divex  26262  elqaalem2  26449  geolim3  26468  dvradcnv  26549  pserdv2  26558  logtayllem  26789  logtayl  26790  cxpmul2  26819  atantayl3  27069  leibpilem2  27071  leibpi  27072  log2cnv  27074  dmgmaddn0  27152  chpp1  27284  0sgmppw  27327  logexprlim  27354  dchrhash  27400  bcctr  27404  bcmono  27406  bcmax  27407  bcp1ctr  27408  2lgslem1c  27522  2lgslem3a  27525  2lgslem3b  27526  2lgslem3c  27527  2lgslem3d  27528  2lgslem3a1  27529  2lgslem3b1  27530  2lgslem3c1  27531  2lgslem3d1  27532  2sqreultlem  27576  2sqreulem2  27581  dchrisumlem1  27618  ostth2lem2  27763  wlklenvclwlk  29943  upgrwlkdvdelem  30025  wwlknp  30132  wwlknlsw  30136  wlkiswwlks1  30156  wlklnwwlkln2lem  30171  wlknwwlksnbij  30177  wwlksnred  30181  wwlksnext  30182  wwlksnredwwlkn  30184  wwlksnextwrd  30186  wwlksnextinj  30188  wwlksnextproplem2  30199  wwlksnextproplem3  30200  wspthsnwspthsnon  30205  clwlkclwwlklem2a1  30283  clwlkclwwlklem2a4  30288  clwlkclwwlklem2a  30289  clwlkclwwlklem2  30291  clwlkclwwlklem3  30292  wwlksext2clwwlk  30348  clwwlknonex2lem2  30399  eucrctshift  30534  eucrct2eupth  30536  numclwwlk2lem1lem  30633  numclwwlk1  30652  numclwwlk7  30682  ipasslem1  31123  ipasslem2  31124  dpfrac1  33151  archirngz  33449  psrmonmul  33884  nn0constr  34095  pthhashvtx  35518  subfacval2  35577  bccolsum  36129  faclimlem1  36133  poimirlem28  38186  heiborlem4  38352  heiborlem6  38354  lcmineqlem3  42687  facp2  42799  sticksstones7  42808  oddnumth  42961  nicomachus  42962  sumcubes  42963  pell14qrgt0  43477  pell14qrdich  43487  pell1qrge1  43488  2nn0ind  43563  jm2.17a  43578  jm2.18  43606  jm2.19lem3  43609  proot1ex  43814  bcc0  44941  dvradcnv2  44948  binomcxplemrat  44951  binomcxplemnotnn0  44957  fperiodmullem  45913  stoweidlem10  46615  stoweidlem17  46622  stoweidlem26  46631  stirlinglem5  46683  stirlinglem7  46685  etransclem23  46862  cjnpoly  47514  subsubelfzo0  47952  fargshiftfo  48079  fmtnodvds  48184  goldbachthlem1  48185  fmtnofac2lem  48208  fmtnofac1  48210  nn0onn0exALTV  48352  nn0enn0exALTV  48353  isubgr3stgrlem2  48620  nn0mnd  48832  ply1mulgsumlem1  49050  ply1mulgsumlem2  49051  nn0onn0ex  49187  nn0enn0ex  49188  fllog2  49232  dignn0fr  49265  digexp  49271  0dig2nn0e  49276  0dig2nn0o  49277  dignn0ehalf  49281  nn0mulfsum  49288  nn0mullong  49289  itcovalpclem1  49334  itcovalpclem2  49335  itcovalt2lem2lem2  49338  ackval1  49345  ackval2  49346  ackval3  49347