Theorem nn0z 12589

Description: A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0z	⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)

Proof of Theorem nn0z

Step	Hyp	Ref	Expression
1		nn0ssz 12587	. 2 ⊢ ℕ0 ⊆ ℤ
2	1	sseli 3979	1 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2104  ℕ₀cn0 12478  ℤcz 12564

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-i2m1 11182  ax-1ne0 11183  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7416  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-neg 11453  df-nn 12219  df-n0 12479  df-z 12565

This theorem is referenced by:  nn0negz  12606  nn0ltp1le  12626  nn0leltp1  12627  nn0ltlem1  12628  nn0lt2  12631  nn0le2is012  12632  nn0lem1lt  12633  fnn0ind  12667  nn0pzuz  12895  nn0ge2m1nnALT  12932  fz1n  13525  ige2m1fz  13597  elfz2nn0  13598  fznn0  13599  elfz0add  13606  fzctr  13619  difelfzle  13620  fzoun  13675  fzofzim  13685  fzo1fzo0n0  13689  elincfzoext  13696  elfzodifsumelfzo  13704  fz0add1fz1  13708  zpnn0elfzo  13711  fzossfzop1  13716  ubmelm1fzo  13734  elfznelfzo  13743  flmulnn0  13798  quoremnn0  13827  zmodidfzoimp  13872  modmuladdnn0  13886  modfzo0difsn  13914  expdiv  14085  expnngt1  14210  faclbnd3  14258  bccmpl  14275  bcnp1n  14280  bcval5  14284  bcn2  14285  bcp1m1  14286  hashge2el2difr  14448  fi1uzind  14464  wrdred1  14516  wrdred1hash  14517  ccatalpha  14549  swrdnd0  14613  swrdfv2  14617  swrdsb0eq  14619  swrdsbslen  14620  swrdspsleq  14621  swrdlsw  14623  pfxnd  14643  pfxccatin12lem4  14682  pfxccatin12lem3  14688  pfxccat3  14690  swrdccat  14691  pfxccat3a  14694  revlen  14718  repswswrd  14740  repswccat  14742  cshwidxmodr  14760  cshf1  14766  2cshw  14769  cshweqrep  14777  cshwcshid  14784  cshwcsh2id  14785  cats1fv  14816  swrd2lsw  14909  2swrd2eqwrdeq  14910  isercoll  15620  iseraltlem2  15635  bcxmas  15787  geo2sum2  15826  geomulcvg  15828  risefacval2  15960  fallfacval2  15961  zrisefaccl  15970  zfallfaccl  15971  fallrisefac  15975  bpolylem  15998  fsumkthpow  16006  esum  16030  ege2le3  16039  eftlcl  16056  reeftlcl  16057  eftlub  16058  effsumlt  16060  eirrlem  16153  dvds1  16268  dvdsext  16270  addmodlteqALT  16274  oddnn02np1  16297  oddge22np1  16298  nn0ehalf  16327  nn0o1gt2  16330  nno  16331  nn0o  16332  nn0oddm1d2  16334  divalglem4  16345  divalglem5  16346  modremain  16357  bitsinv1  16389  nn0gcdid0  16468  nn0seqcvgd  16513  algcvga  16522  eucalgf  16526  nonsq  16701  odzdvds  16734  coprimeprodsq  16747  coprimeprodsq2  16748  oddprm  16749  iserodd  16774  pcexp  16798  pcidlem  16811  pc11  16819  dvdsprmpweqle  16825  difsqpwdvds  16826  pcfac  16838  prmunb  16853  hashbc2  16945  cshwshashlem2  17036  smndex1ibas  18819  smndex1iidm  18820  smndex2dnrinv  18834  smndex2dlinvh  18836  mulgaddcom  19016  mulginvcom  19017  mulgz  19020  mulgdirlem  19023  mulgass  19029  mndodcongi  19454  oddvdsnn0  19455  odeq  19461  odmulg  19467  efgsdmi  19643  cyggex2  19808  fincygsubgodd  20025  mulgass2  20199  chrrhm  21304  zncrng  21321  znzrh2  21322  zndvds  21326  znchr  21339  znunit  21340  chfacfisf  22578  chfacfisfcpmat  22579  chfacfscmulfsupp  22583  chfacfpmmulfsupp  22587  clmmulg  24850  itgcnlem  25541  degltlem1  25824  plyco0  25940  dgreq0  26013  plydivex  26044  aannenlem1  26075  abelthlem1  26177  abelthlem3  26179  abelthlem8  26185  abelthlem9  26186  advlogexp  26397  cxpexp  26410  leibpi  26681  log2cnv  26683  log2tlbnd  26684  basellem2  26820  sgmnncl  26885  chpp1  26893  bcmono  27014  bcmax  27015  bcp1ctr  27016  lgsneg1  27059  lgsdirnn0  27081  lgsdinn0  27082  2lgslem1c  27130  2lgslem3a1  27137  2lgslem3b1  27138  2lgslem3c1  27139  2lgsoddprmlem2  27146  2sq2  27170  2sqreultlem  27184  dchrisumlem1  27226  qabvle  27362  ostth2lem2  27371  tgldimor  28018  upgrewlkle2  29128  wlkv0  29173  redwlk  29194  pthdadjvtx  29252  pthdlem1  29288  wwlknvtx  29364  wlkiswwlks2lem3  29390  wwlksm1edg  29400  wwlksnred  29411  wwlksnext  29412  clwlkclwwlklem2a1  29510  clwlkclwwlklem2a2  29511  clwlkclwwlklem2fv1  29513  clwlkclwwlklem2fv2  29514  clwlkclwwlklem2a4  29515  clwlkclwwlklem2a  29516  clwlkclwwlklem2  29518  clwlkclwwlk  29520  clwwisshclwwslem  29532  eucrctshift  29761  eucrct2eupth1  29762  eucrct2eupth  29763  numclwwlk5lem  29905  numclwwlk5  29906  numclwwlk7  29909  frgrreggt1  29911  nndiffz1  32262  xrge0mulgnn0  32455  hashf2  33378  signsvtn0  33877  nn0ltp1ne  34397  0nn0m1nnn0  34398  pthhashvtx  34414  fz0n  35002  bcneg1  35008  bccolsum  35011  faclimlem3  35017  faclim  35018  iprodfac  35019  poimirlem28  36821  mblfinlem1  36830  mblfinlem2  36831  lcmineqlem2  41203  sticksstones22  41292  gcdnn0id  41524  numdenexp  41532  negexpidd  41724  nacsfix  41754  fzsplit1nn0  41796  eldioph2lem1  41802  fz1eqin  41811  diophin  41814  eq0rabdioph  41818  rexrabdioph  41836  rexzrexnn0  41846  irrapxlem4  41867  pell14qrss1234  41898  pell1qrss14  41910  monotoddzz  41986  rmxypos  41990  ltrmynn0  41991  ltrmxnn0  41992  lermxnn0  41993  rmxnn  41994  rmynn0  42000  jm2.17a  42003  jm2.17b  42004  rmygeid  42007  jm2.18  42031  jm2.19lem3  42034  jm2.19lem4  42035  jm2.22  42038  rmxdiophlem  42058  hbt  42176  proot1ex  42247  fzisoeu  44310  stirlinglem5  45094  elfzlble  46328  subsubelfzo0  46334  2ffzoeq  46336  fargshiftfo  46410  fmtnof1  46503  fmtnorec1  46505  goldbachthlem1  46513  odz2prm2pw  46531  flsqrt  46561  lighneallem4  46578  nn0eo  47303  nn0ofldiv2  47307  flnn0div2ge  47308  fllog2  47343  blenpw2  47353  blennngt2o2  47367  nn0digval  47375  dignn0fr  47376  digexp  47382  0dig2nn0e  47387  0dig2nn0o  47388  dig2bits  47389  dignn0flhalflem2  47391  dignn0ehalf  47392  dignn0flhalf  47393  nn0sumshdiglemB  47395