Theorem nn0z 12561

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕ₀cn0 12449  ℤcz 12536

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-neg 11415  df-nn 12194  df-n0 12450  df-z 12537

This theorem is referenced by:  nn0negz  12578  nn0ltp1le  12599  nn0leltp1  12600  nn0ltlem1  12601  nn0lt2  12604  nn0le2is012  12605  nn0lem1lt  12606  fnn0ind  12640  nn0pzuz  12871  nn0ge2m1nnALT  12908  fz1n  13510  ige2m1fz  13585  elfz2nn0  13586  fznn0  13587  elfz0add  13594  fzctr  13608  difelfzle  13609  fzoun  13664  fzofzim  13677  fzo1fzo0n0  13683  elincfzoext  13691  elfzodifsumelfzo  13699  fz0add1fz1  13703  zpnn0elfzo  13706  fzossfzop1  13711  ubmelm1fzo  13731  elfznelfzo  13740  flmulnn0  13796  quoremnn0  13825  zmodidfzoimp  13870  modmuladdnn0  13887  modfzo0difsn  13915  expdiv  14085  expnngt1  14213  faclbnd3  14264  bccmpl  14281  bcnp1n  14286  bcval5  14290  bcn2  14291  bcp1m1  14292  hashge2el2difr  14453  fi1uzind  14479  wrdred1  14532  wrdred1hash  14533  ccatalpha  14565  swrdnd0  14629  swrdfv2  14633  swrdsb0eq  14635  swrdsbslen  14636  swrdspsleq  14637  swrdlsw  14639  pfxnd  14659  pfxccatin12lem4  14698  pfxccatin12lem3  14704  pfxccat3  14706  swrdccat  14707  pfxccat3a  14710  revlen  14734  repswswrd  14756  repswccat  14758  cshwidxmodr  14776  cshf1  14782  2cshw  14785  cshweqrep  14793  cshwcshid  14800  cshwcsh2id  14801  cats1fv  14832  swrd2lsw  14925  2swrd2eqwrdeq  14926  isercoll  15641  iseraltlem2  15656  bcxmas  15808  geo2sum2  15847  geomulcvg  15849  risefacval2  15983  fallfacval2  15984  zrisefaccl  15993  zfallfaccl  15994  fallrisefac  15998  bpolylem  16021  fsumkthpow  16029  esum  16053  ege2le3  16063  eftlcl  16082  reeftlcl  16083  eftlub  16084  effsumlt  16086  eirrlem  16179  dvds1  16296  dvdsext  16298  addmodlteqALT  16302  oddnn02np1  16325  oddge22np1  16326  nn0ehalf  16355  nn0o1gt2  16358  nno  16359  nn0o  16360  nn0oddm1d2  16362  divalglem4  16373  divalglem5  16374  modremain  16385  bitsinv1  16419  nn0gcdid0  16498  nn0seqcvgd  16547  algcvga  16556  eucalgf  16560  nonsq  16736  numdenexp  16737  odzdvds  16773  coprimeprodsq  16786  coprimeprodsq2  16787  oddprm  16788  iserodd  16813  pcexp  16837  pcidlem  16850  pc11  16858  dvdsprmpweqle  16864  difsqpwdvds  16865  pcfac  16877  prmunb  16892  hashbc2  16984  cshwshashlem2  17074  smndex1ibas  18834  smndex1iidm  18835  smndex2dnrinv  18849  smndex2dlinvh  18851  mulgaddcom  19037  mulginvcom  19038  mulgz  19041  mulgdirlem  19044  mulgass  19050  mndodcongi  19480  oddvdsnn0  19481  odeq  19487  odmulg  19493  efgsdmi  19669  cyggex2  19834  fincygsubgodd  20051  mulgass2  20225  chrrhm  21448  zncrng  21461  znzrh2  21462  zndvds  21466  znchr  21479  znunit  21480  chfacfisf  22748  chfacfisfcpmat  22749  chfacfscmulfsupp  22753  chfacfpmmulfsupp  22757  clmmulg  25008  itgcnlem  25698  degltlem1  25984  plyco0  26104  dgreq0  26178  plydivex  26212  aannenlem1  26243  abelthlem1  26348  abelthlem3  26350  abelthlem8  26356  abelthlem9  26357  advlogexp  26571  cxpexp  26584  leibpi  26859  log2cnv  26861  log2tlbnd  26862  basellem2  26999  sgmnncl  27064  chpp1  27072  bcmono  27195  bcmax  27196  bcp1ctr  27197  lgsneg1  27240  lgsdirnn0  27262  lgsdinn0  27263  2lgslem1c  27311  2lgslem3a1  27318  2lgslem3b1  27319  2lgslem3c1  27320  2lgsoddprmlem2  27327  2sq2  27351  2sqreultlem  27365  dchrisumlem1  27407  qabvle  27543  ostth2lem2  27552  tgldimor  28436  upgrewlkle2  29541  wlkv0  29586  redwlk  29607  pthdadjvtx  29665  pthdlem1  29703  wwlknvtx  29782  wlkiswwlks2lem3  29808  wwlksm1edg  29818  wwlksnred  29829  wwlksnext  29830  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a2  29929  clwlkclwwlklem2fv1  29931  clwlkclwwlklem2fv2  29932  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlk  29938  clwwisshclwwslem  29950  eucrctshift  30179  eucrct2eupth1  30180  eucrct2eupth  30181  numclwwlk5lem  30323  numclwwlk5  30324  numclwwlk7  30327  frgrreggt1  30329  nndiffz1  32716  xrge0mulgnn0  32963  hashf2  34081  signsvtn0  34568  nn0ltp1ne  35106  0nn0m1nnn0  35107  pthhashvtx  35122  fz0n  35725  bcneg1  35730  bccolsum  35733  faclimlem3  35739  faclim  35740  iprodfac  35741  poimirlem28  37649  mblfinlem1  37658  mblfinlem2  37659  lcmineqlem2  42025  sticksstones22  42163  gcdnn0id  42324  negexpidd  42677  nacsfix  42707  fzsplit1nn0  42749  eldioph2lem1  42755  fz1eqin  42764  diophin  42767  eq0rabdioph  42771  rexrabdioph  42789  rexzrexnn0  42799  irrapxlem4  42820  pell14qrss1234  42851  pell1qrss14  42863  monotoddzz  42939  rmxypos  42943  ltrmynn0  42944  ltrmxnn0  42945  lermxnn0  42946  rmxnn  42947  rmynn0  42953  jm2.17a  42956  jm2.17b  42957  rmygeid  42960  jm2.18  42984  jm2.19lem3  42987  jm2.19lem4  42988  jm2.22  42991  rmxdiophlem  43011  hbt  43126  proot1ex  43192  fzisoeu  45305  stirlinglem5  46083  elfzlble  47325  subsubelfzo0  47331  2ffzoeq  47332  addmodne  47349  fargshiftfo  47447  fmtnof1  47540  fmtnorec1  47542  goldbachthlem1  47550  odz2prm2pw  47568  flsqrt  47598  lighneallem4  47615  nn0eo  48521  nn0ofldiv2  48525  flnn0div2ge  48526  fllog2  48561  blenpw2  48571  blennngt2o2  48585  nn0digval  48593  dignn0fr  48594  digexp  48600  0dig2nn0e  48605  0dig2nn0o  48606  dig2bits  48607  dignn0flhalflem2  48609  dignn0ehalf  48610  dignn0flhalf  48611  nn0sumshdiglemB  48613