Theorem nn0z 12554

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕ₀cn0 12442  ℤcz 12529

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-neg 11408  df-nn 12187  df-n0 12443  df-z 12530

This theorem is referenced by:  nn0negz  12571  nn0ltp1le  12592  nn0leltp1  12593  nn0ltlem1  12594  nn0lt2  12597  nn0le2is012  12598  nn0lem1lt  12599  fnn0ind  12633  nn0pzuz  12864  nn0ge2m1nnALT  12901  fz1n  13503  ige2m1fz  13578  elfz2nn0  13579  fznn0  13580  elfz0add  13587  fzctr  13601  difelfzle  13602  fzoun  13657  fzofzim  13670  fzo1fzo0n0  13676  elincfzoext  13684  elfzodifsumelfzo  13692  fz0add1fz1  13696  zpnn0elfzo  13699  fzossfzop1  13704  ubmelm1fzo  13724  elfznelfzo  13733  flmulnn0  13789  quoremnn0  13818  zmodidfzoimp  13863  modmuladdnn0  13880  modfzo0difsn  13908  expdiv  14078  expnngt1  14206  faclbnd3  14257  bccmpl  14274  bcnp1n  14279  bcval5  14283  bcn2  14284  bcp1m1  14285  hashge2el2difr  14446  fi1uzind  14472  wrdred1  14525  wrdred1hash  14526  ccatalpha  14558  swrdnd0  14622  swrdfv2  14626  swrdsb0eq  14628  swrdsbslen  14629  swrdspsleq  14630  swrdlsw  14632  pfxnd  14652  pfxccatin12lem4  14691  pfxccatin12lem3  14697  pfxccat3  14699  swrdccat  14700  pfxccat3a  14703  revlen  14727  repswswrd  14749  repswccat  14751  cshwidxmodr  14769  cshf1  14775  2cshw  14778  cshweqrep  14786  cshwcshid  14793  cshwcsh2id  14794  cats1fv  14825  swrd2lsw  14918  2swrd2eqwrdeq  14919  isercoll  15634  iseraltlem2  15649  bcxmas  15801  geo2sum2  15840  geomulcvg  15842  risefacval2  15976  fallfacval2  15977  zrisefaccl  15986  zfallfaccl  15987  fallrisefac  15991  bpolylem  16014  fsumkthpow  16022  esum  16046  ege2le3  16056  eftlcl  16075  reeftlcl  16076  eftlub  16077  effsumlt  16079  eirrlem  16172  dvds1  16289  dvdsext  16291  addmodlteqALT  16295  oddnn02np1  16318  oddge22np1  16319  nn0ehalf  16348  nn0o1gt2  16351  nno  16352  nn0o  16353  nn0oddm1d2  16355  divalglem4  16366  divalglem5  16367  modremain  16378  bitsinv1  16412  nn0gcdid0  16491  nn0seqcvgd  16540  algcvga  16549  eucalgf  16553  nonsq  16729  numdenexp  16730  odzdvds  16766  coprimeprodsq  16779  coprimeprodsq2  16780  oddprm  16781  iserodd  16806  pcexp  16830  pcidlem  16843  pc11  16851  dvdsprmpweqle  16857  difsqpwdvds  16858  pcfac  16870  prmunb  16885  hashbc2  16977  cshwshashlem2  17067  smndex1ibas  18827  smndex1iidm  18828  smndex2dnrinv  18842  smndex2dlinvh  18844  mulgaddcom  19030  mulginvcom  19031  mulgz  19034  mulgdirlem  19037  mulgass  19043  mndodcongi  19473  oddvdsnn0  19474  odeq  19480  odmulg  19486  efgsdmi  19662  cyggex2  19827  fincygsubgodd  20044  mulgass2  20218  chrrhm  21441  zncrng  21454  znzrh2  21455  zndvds  21459  znchr  21472  znunit  21473  chfacfisf  22741  chfacfisfcpmat  22742  chfacfscmulfsupp  22746  chfacfpmmulfsupp  22750  clmmulg  25001  itgcnlem  25691  degltlem1  25977  plyco0  26097  dgreq0  26171  plydivex  26205  aannenlem1  26236  abelthlem1  26341  abelthlem3  26343  abelthlem8  26349  abelthlem9  26350  advlogexp  26564  cxpexp  26577  leibpi  26852  log2cnv  26854  log2tlbnd  26855  basellem2  26992  sgmnncl  27057  chpp1  27065  bcmono  27188  bcmax  27189  bcp1ctr  27190  lgsneg1  27233  lgsdirnn0  27255  lgsdinn0  27256  2lgslem1c  27304  2lgslem3a1  27311  2lgslem3b1  27312  2lgslem3c1  27313  2lgsoddprmlem2  27320  2sq2  27344  2sqreultlem  27358  dchrisumlem1  27400  qabvle  27536  ostth2lem2  27545  tgldimor  28429  upgrewlkle2  29534  wlkv0  29579  redwlk  29600  pthdadjvtx  29658  pthdlem1  29696  wwlknvtx  29775  wlkiswwlks2lem3  29801  wwlksm1edg  29811  wwlksnred  29822  wwlksnext  29823  clwlkclwwlklem2a1  29921  clwlkclwwlklem2a2  29922  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwlkclwwlk  29931  clwwisshclwwslem  29943  eucrctshift  30172  eucrct2eupth1  30173  eucrct2eupth  30174  numclwwlk5lem  30316  numclwwlk5  30317  numclwwlk7  30320  frgrreggt1  30322  nndiffz1  32709  xrge0mulgnn0  32956  hashf2  34074  signsvtn0  34561  nn0ltp1ne  35099  0nn0m1nnn0  35100  pthhashvtx  35115  fz0n  35718  bcneg1  35723  bccolsum  35726  faclimlem3  35732  faclim  35733  iprodfac  35734  poimirlem28  37642  mblfinlem1  37651  mblfinlem2  37652  lcmineqlem2  42018  sticksstones22  42156  gcdnn0id  42317  negexpidd  42670  nacsfix  42700  fzsplit1nn0  42742  eldioph2lem1  42748  fz1eqin  42757  diophin  42760  eq0rabdioph  42764  rexrabdioph  42782  rexzrexnn0  42792  irrapxlem4  42813  pell14qrss1234  42844  pell1qrss14  42856  monotoddzz  42932  rmxypos  42936  ltrmynn0  42937  ltrmxnn0  42938  lermxnn0  42939  rmxnn  42940  rmynn0  42946  jm2.17a  42949  jm2.17b  42950  rmygeid  42953  jm2.18  42977  jm2.19lem3  42980  jm2.19lem4  42981  jm2.22  42984  rmxdiophlem  43004  hbt  43119  proot1ex  43185  fzisoeu  45298  stirlinglem5  46076  elfzlble  47321  subsubelfzo0  47327  2ffzoeq  47328  addmodne  47345  fargshiftfo  47443  fmtnof1  47536  fmtnorec1  47538  goldbachthlem1  47546  odz2prm2pw  47564  flsqrt  47594  lighneallem4  47611  nn0eo  48517  nn0ofldiv2  48521  flnn0div2ge  48522  fllog2  48557  blenpw2  48567  blennngt2o2  48581  nn0digval  48589  dignn0fr  48590  digexp  48596  0dig2nn0e  48601  0dig2nn0o  48602  dig2bits  48603  dignn0flhalflem2  48605  dignn0ehalf  48606  dignn0flhalf  48607  nn0sumshdiglemB  48609