Theorem nn0z 12613

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 12611	. 2 ⊢ ℕ0 ⊆ ℤ
2	1	sseli 3954	1 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2108  ℕ₀cn0 12501  ℤcz 12588

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-i2m1 11197  ax-1ne0 11198  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-neg 11469  df-nn 12241  df-n0 12502  df-z 12589

This theorem is referenced by:  nn0negz  12630  nn0ltp1le  12651  nn0leltp1  12652  nn0ltlem1  12653  nn0lt2  12656  nn0le2is012  12657  nn0lem1lt  12658  fnn0ind  12692  nn0pzuz  12921  nn0ge2m1nnALT  12958  fz1n  13559  ige2m1fz  13634  elfz2nn0  13635  fznn0  13636  elfz0add  13643  fzctr  13657  difelfzle  13658  fzoun  13713  fzofzim  13726  fzo1fzo0n0  13731  elincfzoext  13739  elfzodifsumelfzo  13747  fz0add1fz1  13751  zpnn0elfzo  13754  fzossfzop1  13759  ubmelm1fzo  13779  elfznelfzo  13788  flmulnn0  13844  quoremnn0  13873  zmodidfzoimp  13918  modmuladdnn0  13933  modfzo0difsn  13961  expdiv  14131  expnngt1  14259  faclbnd3  14310  bccmpl  14327  bcnp1n  14332  bcval5  14336  bcn2  14337  bcp1m1  14338  hashge2el2difr  14499  fi1uzind  14525  wrdred1  14578  wrdred1hash  14579  ccatalpha  14611  swrdnd0  14675  swrdfv2  14679  swrdsb0eq  14681  swrdsbslen  14682  swrdspsleq  14683  swrdlsw  14685  pfxnd  14705  pfxccatin12lem4  14744  pfxccatin12lem3  14750  pfxccat3  14752  swrdccat  14753  pfxccat3a  14756  revlen  14780  repswswrd  14802  repswccat  14804  cshwidxmodr  14822  cshf1  14828  2cshw  14831  cshweqrep  14839  cshwcshid  14846  cshwcsh2id  14847  cats1fv  14878  swrd2lsw  14971  2swrd2eqwrdeq  14972  isercoll  15684  iseraltlem2  15699  bcxmas  15851  geo2sum2  15890  geomulcvg  15892  risefacval2  16026  fallfacval2  16027  zrisefaccl  16036  zfallfaccl  16037  fallrisefac  16041  bpolylem  16064  fsumkthpow  16072  esum  16096  ege2le3  16106  eftlcl  16125  reeftlcl  16126  eftlub  16127  effsumlt  16129  eirrlem  16222  dvds1  16338  dvdsext  16340  addmodlteqALT  16344  oddnn02np1  16367  oddge22np1  16368  nn0ehalf  16397  nn0o1gt2  16400  nno  16401  nn0o  16402  nn0oddm1d2  16404  divalglem4  16415  divalglem5  16416  modremain  16427  bitsinv1  16461  nn0gcdid0  16540  nn0seqcvgd  16589  algcvga  16598  eucalgf  16602  nonsq  16778  numdenexp  16779  odzdvds  16815  coprimeprodsq  16828  coprimeprodsq2  16829  oddprm  16830  iserodd  16855  pcexp  16879  pcidlem  16892  pc11  16900  dvdsprmpweqle  16906  difsqpwdvds  16907  pcfac  16919  prmunb  16934  hashbc2  17026  cshwshashlem2  17116  smndex1ibas  18878  smndex1iidm  18879  smndex2dnrinv  18893  smndex2dlinvh  18895  mulgaddcom  19081  mulginvcom  19082  mulgz  19085  mulgdirlem  19088  mulgass  19094  mndodcongi  19524  oddvdsnn0  19525  odeq  19531  odmulg  19537  efgsdmi  19713  cyggex2  19878  fincygsubgodd  20095  mulgass2  20269  chrrhm  21492  zncrng  21505  znzrh2  21506  zndvds  21510  znchr  21523  znunit  21524  chfacfisf  22792  chfacfisfcpmat  22793  chfacfscmulfsupp  22797  chfacfpmmulfsupp  22801  clmmulg  25052  itgcnlem  25743  degltlem1  26029  plyco0  26149  dgreq0  26223  plydivex  26257  aannenlem1  26288  abelthlem1  26393  abelthlem3  26395  abelthlem8  26401  abelthlem9  26402  advlogexp  26616  cxpexp  26629  leibpi  26904  log2cnv  26906  log2tlbnd  26907  basellem2  27044  sgmnncl  27109  chpp1  27117  bcmono  27240  bcmax  27241  bcp1ctr  27242  lgsneg1  27285  lgsdirnn0  27307  lgsdinn0  27308  2lgslem1c  27356  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgsoddprmlem2  27372  2sq2  27396  2sqreultlem  27410  dchrisumlem1  27452  qabvle  27588  ostth2lem2  27597  tgldimor  28481  upgrewlkle2  29586  wlkv0  29631  redwlk  29652  pthdadjvtx  29710  pthdlem1  29748  wwlknvtx  29827  wlkiswwlks2lem3  29853  wwlksm1edg  29863  wwlksnred  29874  wwlksnext  29875  clwlkclwwlklem2a1  29973  clwlkclwwlklem2a2  29974  clwlkclwwlklem2fv1  29976  clwlkclwwlklem2fv2  29977  clwlkclwwlklem2a4  29978  clwlkclwwlklem2a  29979  clwlkclwwlklem2  29981  clwlkclwwlk  29983  clwwisshclwwslem  29995  eucrctshift  30224  eucrct2eupth1  30225  eucrct2eupth  30226  numclwwlk5lem  30368  numclwwlk5  30369  numclwwlk7  30372  frgrreggt1  30374  nndiffz1  32763  xrge0mulgnn0  33010  hashf2  34115  signsvtn0  34602  nn0ltp1ne  35134  0nn0m1nnn0  35135  pthhashvtx  35150  fz0n  35748  bcneg1  35753  bccolsum  35756  faclimlem3  35762  faclim  35763  iprodfac  35764  poimirlem28  37672  mblfinlem1  37681  mblfinlem2  37682  lcmineqlem2  42043  sticksstones22  42181  gcdnn0id  42378  negexpidd  42705  nacsfix  42735  fzsplit1nn0  42777  eldioph2lem1  42783  fz1eqin  42792  diophin  42795  eq0rabdioph  42799  rexrabdioph  42817  rexzrexnn0  42827  irrapxlem4  42848  pell14qrss1234  42879  pell1qrss14  42891  monotoddzz  42967  rmxypos  42971  ltrmynn0  42972  ltrmxnn0  42973  lermxnn0  42974  rmxnn  42975  rmynn0  42981  jm2.17a  42984  jm2.17b  42985  rmygeid  42988  jm2.18  43012  jm2.19lem3  43015  jm2.19lem4  43016  jm2.22  43019  rmxdiophlem  43039  hbt  43154  proot1ex  43220  fzisoeu  45329  stirlinglem5  46107  elfzlble  47349  subsubelfzo0  47355  2ffzoeq  47356  addmodne  47373  fargshiftfo  47456  fmtnof1  47549  fmtnorec1  47551  goldbachthlem1  47559  odz2prm2pw  47577  flsqrt  47607  lighneallem4  47624  nn0eo  48508  nn0ofldiv2  48512  flnn0div2ge  48513  fllog2  48548  blenpw2  48558  blennngt2o2  48572  nn0digval  48580  dignn0fr  48581  digexp  48587  0dig2nn0e  48592  0dig2nn0o  48593  dig2bits  48594  dignn0flhalflem2  48596  dignn0ehalf  48597  dignn0flhalf  48598  nn0sumshdiglemB  48600