Theorem nn0z 12635

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

Syntax hints:   → wi 4   ∈ wcel 2099  ℕ₀cn0 12524  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433  ax-un 7746  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-i2m1 11226  ax-1ne0 11227  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-om 7877  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-neg 11497  df-nn 12265  df-n0 12525  df-z 12611

This theorem is referenced by:  nn0negz  12652  nn0ltp1le  12672  nn0leltp1  12673  nn0ltlem1  12674  nn0lt2  12677  nn0le2is012  12678  nn0lem1lt  12679  fnn0ind  12713  nn0pzuz  12941  nn0ge2m1nnALT  12978  fz1n  13573  ige2m1fz  13645  elfz2nn0  13646  fznn0  13647  elfz0add  13654  fzctr  13667  difelfzle  13668  fzoun  13723  fzofzim  13733  fzo1fzo0n0  13737  elincfzoext  13744  elfzodifsumelfzo  13752  fz0add1fz1  13756  zpnn0elfzo  13759  fzossfzop1  13764  ubmelm1fzo  13783  elfznelfzo  13792  flmulnn0  13847  quoremnn0  13876  zmodidfzoimp  13921  modmuladdnn0  13935  modfzo0difsn  13963  expdiv  14133  expnngt1  14258  faclbnd3  14309  bccmpl  14326  bcnp1n  14331  bcval5  14335  bcn2  14336  bcp1m1  14337  hashge2el2difr  14500  fi1uzind  14516  wrdred1  14568  wrdred1hash  14569  ccatalpha  14601  swrdnd0  14665  swrdfv2  14669  swrdsb0eq  14671  swrdsbslen  14672  swrdspsleq  14673  swrdlsw  14675  pfxnd  14695  pfxccatin12lem4  14734  pfxccatin12lem3  14740  pfxccat3  14742  swrdccat  14743  pfxccat3a  14746  revlen  14770  repswswrd  14792  repswccat  14794  cshwidxmodr  14812  cshf1  14818  2cshw  14821  cshweqrep  14829  cshwcshid  14836  cshwcsh2id  14837  cats1fv  14868  swrd2lsw  14961  2swrd2eqwrdeq  14962  isercoll  15672  iseraltlem2  15687  bcxmas  15839  geo2sum2  15878  geomulcvg  15880  risefacval2  16012  fallfacval2  16013  zrisefaccl  16022  zfallfaccl  16023  fallrisefac  16027  bpolylem  16050  fsumkthpow  16058  esum  16082  ege2le3  16092  eftlcl  16109  reeftlcl  16110  eftlub  16111  effsumlt  16113  eirrlem  16206  dvds1  16321  dvdsext  16323  addmodlteqALT  16327  oddnn02np1  16350  oddge22np1  16351  nn0ehalf  16380  nn0o1gt2  16383  nno  16384  nn0o  16385  nn0oddm1d2  16387  divalglem4  16398  divalglem5  16399  modremain  16410  bitsinv1  16442  nn0gcdid0  16521  nn0seqcvgd  16571  algcvga  16580  eucalgf  16584  nonsq  16761  numdenexp  16762  odzdvds  16797  coprimeprodsq  16810  coprimeprodsq2  16811  oddprm  16812  iserodd  16837  pcexp  16861  pcidlem  16874  pc11  16882  dvdsprmpweqle  16888  difsqpwdvds  16889  pcfac  16901  prmunb  16916  hashbc2  17008  cshwshashlem2  17099  smndex1ibas  18890  smndex1iidm  18891  smndex2dnrinv  18905  smndex2dlinvh  18907  mulgaddcom  19092  mulginvcom  19093  mulgz  19096  mulgdirlem  19099  mulgass  19105  mndodcongi  19541  oddvdsnn0  19542  odeq  19548  odmulg  19554  efgsdmi  19730  cyggex2  19895  fincygsubgodd  20112  mulgass2  20288  chrrhm  21525  zncrng  21542  znzrh2  21543  zndvds  21547  znchr  21560  znunit  21561  chfacfisf  22847  chfacfisfcpmat  22848  chfacfscmulfsupp  22852  chfacfpmmulfsupp  22856  clmmulg  25119  itgcnlem  25810  degltlem1  26099  plyco0  26219  dgreq0  26293  plydivex  26325  aannenlem1  26356  abelthlem1  26461  abelthlem3  26463  abelthlem8  26469  abelthlem9  26470  advlogexp  26682  cxpexp  26695  leibpi  26970  log2cnv  26972  log2tlbnd  26973  basellem2  27110  sgmnncl  27175  chpp1  27183  bcmono  27306  bcmax  27307  bcp1ctr  27308  lgsneg1  27351  lgsdirnn0  27373  lgsdinn0  27374  2lgslem1c  27422  2lgslem3a1  27429  2lgslem3b1  27430  2lgslem3c1  27431  2lgsoddprmlem2  27438  2sq2  27462  2sqreultlem  27476  dchrisumlem1  27518  qabvle  27654  ostth2lem2  27663  tgldimor  28429  upgrewlkle2  29543  wlkv0  29588  redwlk  29609  pthdadjvtx  29667  pthdlem1  29703  wwlknvtx  29779  wlkiswwlks2lem3  29805  wwlksm1edg  29815  wwlksnred  29826  wwlksnext  29827  clwlkclwwlklem2a1  29925  clwlkclwwlklem2a2  29926  clwlkclwwlklem2fv1  29928  clwlkclwwlklem2fv2  29929  clwlkclwwlklem2a4  29930  clwlkclwwlklem2a  29931  clwlkclwwlklem2  29933  clwlkclwwlk  29935  clwwisshclwwslem  29947  eucrctshift  30176  eucrct2eupth1  30177  eucrct2eupth  30178  numclwwlk5lem  30320  numclwwlk5  30321  numclwwlk7  30324  frgrreggt1  30326  nndiffz1  32688  xrge0mulgnn0  32898  hashf2  33917  signsvtn0  34416  nn0ltp1ne  34939  0nn0m1nnn0  34940  pthhashvtx  34955  fz0n  35553  bcneg1  35558  bccolsum  35561  faclimlem3  35567  faclim  35568  iprodfac  35569  poimirlem28  37349  mblfinlem1  37358  mblfinlem2  37359  lcmineqlem2  41729  sticksstones22  41866  gcdnn0id  42124  negexpidd  42339  nacsfix  42369  fzsplit1nn0  42411  eldioph2lem1  42417  fz1eqin  42426  diophin  42429  eq0rabdioph  42433  rexrabdioph  42451  rexzrexnn0  42461  irrapxlem4  42482  pell14qrss1234  42513  pell1qrss14  42525  monotoddzz  42601  rmxypos  42605  ltrmynn0  42606  ltrmxnn0  42607  lermxnn0  42608  rmxnn  42609  rmynn0  42615  jm2.17a  42618  jm2.17b  42619  rmygeid  42622  jm2.18  42646  jm2.19lem3  42649  jm2.19lem4  42650  jm2.22  42653  rmxdiophlem  42673  hbt  42791  proot1ex  42861  fzisoeu  44915  stirlinglem5  45699  elfzlble  46933  subsubelfzo0  46939  2ffzoeq  46940  fargshiftfo  47014  fmtnof1  47107  fmtnorec1  47109  goldbachthlem1  47117  odz2prm2pw  47135  flsqrt  47165  lighneallem4  47182  nn0eo  47916  nn0ofldiv2  47920  flnn0div2ge  47921  fllog2  47956  blenpw2  47966  blennngt2o2  47980  nn0digval  47988  dignn0fr  47989  digexp  47995  0dig2nn0e  48000  0dig2nn0o  48001  dig2bits  48002  dignn0flhalflem2  48004  dignn0ehalf  48005  dignn0flhalf  48006  nn0sumshdiglemB  48008