Theorem nn0z 12616

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℕ₀cn0 12505  ℤcz 12592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-i2m1 11169  ax-1ne0 11170  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-neg 11445  df-nn 12235  df-n0 12506  df-z 12593

This theorem is referenced by:  nn0negz  12633  nn0ltp1le  12655  nn0leltp1  12656  nn0ltlem1  12657  nn0lt2  12660  nn0le2is012  12661  nn0lem1lt  12662  fnn0ind  12696  nn0pzuz  12930  nn0ge2m1nnALT  12967  fz1n  13571  ige2m1fz  13647  elfz2nn0  13648  fznn0  13649  elfz0add  13656  fzctr  13670  difelfzle  13671  fzoun  13727  fzofzim  13740  fzo1fzo0n0  13746  elincfzoext  13754  elfzodifsumelfzo  13762  fz0add1fz1  13766  zpnn0elfzo  13769  fzossfzop1  13774  ubmelm1fzo  13794  elfznelfzo  13804  flmulnn0  13862  quoremnn0  13891  zmodidfzoimp  13936  modmuladdnn0  13953  modfzo0difsn  13981  expdiv  14151  expnngt1  14279  faclbnd3  14330  bccmpl  14347  bcnp1n  14352  bcval5  14356  bcn2  14357  bcp1m1  14358  hashge2el2difr  14520  fi1uzind  14546  wrdred1  14599  wrdred1hash  14600  ccatalpha  14633  swrdnd0  14697  swrdfv2  14701  swrdsb0eq  14703  swrdsbslen  14704  swrdspsleq  14705  swrdlsw  14707  pfxnd  14727  pfxccatin12lem4  14765  pfxccatin12lem3  14771  pfxccat3  14773  swrdccat  14774  pfxccat3a  14777  revlen  14801  repswswrd  14823  repswccat  14825  cshwidxmodr  14843  cshf1  14849  2cshw  14852  cshweqrep  14860  cshwcshid  14866  cshwcsh2id  14867  cats1fv  14898  swrd2lsw  14991  2swrd2eqwrdeq  14992  isercoll  15721  iseraltlem2  15736  bcxmas  15891  geo2sum2  15930  geomulcvg  15932  risefacval2  16066  fallfacval2  16067  zrisefaccl  16076  zfallfaccl  16077  fallrisefac  16081  bpolylem  16103  fsumkthpow  16111  esum  16135  ege2le3  16145  eftlcl  16164  reeftlcl  16165  eftlub  16166  effsumlt  16168  eirrlem  16261  dvds1  16378  dvdsext  16380  addmodlteqALT  16384  oddnn02np1  16407  oddge22np1  16408  nn0ehalf  16437  nn0o1gt2  16440  nno  16441  nn0o  16442  nn0oddm1d2  16444  divalglem4  16455  divalglem5  16456  modremain  16467  bitsinv1  16501  nn0gcdid0  16580  nn0seqcvgd  16629  algcvga  16638  eucalgf  16642  nonsq  16819  numdenexp  16820  odzdvds  16856  coprimeprodsq  16869  coprimeprodsq2  16870  oddprm  16871  iserodd  16896  pcexp  16920  pcidlem  16933  pc11  16941  dvdsprmpweqle  16947  difsqpwdvds  16948  pcfac  16960  prmunb  16975  hashbc2  17067  cshwshashlem2  17157  chnccat  18683  smndex1ibas  18960  smndex1iidm  18961  smndex2dnrinv  18978  smndex2dlinvh  18980  mulgaddcom  19165  mulginvcom  19166  mulgz  19169  mulgdirlem  19172  mulgass  19178  mndodcongi  19614  oddvdsnn0  19615  odeq  19621  odmulg  19627  efgsdmi  19803  cyggex2  19968  fincygsubgodd  20185  mulgass2  20393  chrrhm  21662  zncrng  21675  znzrh2  21676  zndvds  21680  znchr  21693  znunit  21694  chfacfisf  22992  chfacfisfcpmat  22993  chfacfscmulfsupp  22997  chfacfpmmulfsupp  23001  clmmulg  25241  itgcnlem  25930  degltlem1  26210  plyco0  26330  dgreq0  26403  plydivex  26439  aannenlem1  26470  abelthlem1  26572  abelthlem3  26574  abelthlem8  26580  abelthlem9  26581  advlogexp  26798  cxpexp  26811  leibpi  27085  log2cnv  27087  log2tlbnd  27088  basellem2  27224  sgmnncl  27289  chpp1  27297  bcmono  27419  bcmax  27420  bcp1ctr  27421  lgsneg1  27464  lgsdirnn0  27486  lgsdinn0  27487  2lgslem1c  27535  2lgslem3a1  27542  2lgslem3b1  27543  2lgslem3c1  27544  2lgsoddprmlem2  27551  2sq2  27575  2sqreultlem  27589  dchrisumlem1  27631  qabvle  27767  ostth2lem2  27776  tgldimor  28749  upgrewlkle2  29934  wlkv0  29977  redwlk  29998  pthdadjvtx  30055  pthdlem1  30093  wwlknvtx  30172  wlkiswwlks2lem3  30198  wwlksm1edg  30208  wwlksnred  30219  wwlksnext  30220  clwlkclwwlklem2a1  30321  clwlkclwwlklem2a2  30322  clwlkclwwlklem2fv1  30324  clwlkclwwlklem2fv2  30325  clwlkclwwlklem2a4  30326  clwlkclwwlklem2a  30327  clwlkclwwlklem2  30329  clwlkclwwlk  30331  clwwisshclwwslem  30343  eucrctshift  30572  eucrct2eupth1  30573  eucrct2eupth  30574  numclwwlk5lem  30716  numclwwlk5  30717  numclwwlk7  30720  frgrreggt1  30722  nndiffz1  33109  nn0diffz0  33117  xrge0mulgnn0  33313  hashf2  34452  signsvtn0  34935  nn0ltp1ne  35581  0nn0m1nnn0  35582  pthhashvtx  35598  fz0n  36201  bcneg1  36206  bccolsum  36209  faclimlem3  36215  faclim  36216  iprodfac  36217  poimirlem28  38277  mblfinlem1  38286  mblfinlem2  38287  lcmineqlem2  42775  sticksstones22  42913  gcdnn0id  43068  negexpidd  43393  nacsfix  43423  fzsplit1nn0  43465  eldioph2lem1  43471  fz1eqin  43480  diophin  43483  eq0rabdioph  43487  rexrabdioph  43501  rexzrexnn0  43511  irrapxlem4  43532  pell14qrss1234  43563  pell1qrss14  43575  monotoddzz  43650  rmxypos  43654  ltrmynn0  43655  ltrmxnn0  43656  lermxnn0  43657  rmxnn  43658  rmynn0  43664  jm2.17a  43667  jm2.17b  43668  rmygeid  43671  jm2.18  43695  jm2.19lem3  43698  jm2.19lem4  43699  jm2.22  43702  rmxdiophlem  43722  hbt  43837  proot1ex  43903  fzisoeu  45999  stirlinglem5  46772  elfzlble  48034  subsubelfzo0  48041  2ffzoeq  48042  addmodne  48064  fargshiftfo  48168  fmtnof1  48264  fmtnorec1  48266  goldbachthlem1  48274  odz2prm2pw  48292  flsqrt  48322  lighneallem4  48339  nn0eo  49285  nn0ofldiv2  49289  flnn0div2ge  49290  fllog2  49325  blenpw2  49335  blennngt2o2  49349  nn0digval  49357  dignn0fr  49358  digexp  49364  0dig2nn0e  49369  0dig2nn0o  49370  dig2bits  49371  dignn0flhalflem2  49373  dignn0ehalf  49374  dignn0flhalf  49375  nn0sumshdiglemB  49377