Theorem nn0z 12499

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℕ₀cn0 12388  ℤcz 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-i2m1 11081  ax-1ne0 11082  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-neg 11354  df-nn 12133  df-n0 12389  df-z 12476

This theorem is referenced by:  nn0negz  12516  nn0ltp1le  12537  nn0leltp1  12538  nn0ltlem1  12539  nn0lt2  12542  nn0le2is012  12543  nn0lem1lt  12544  fnn0ind  12578  nn0pzuz  12805  nn0ge2m1nnALT  12842  fz1n  13444  ige2m1fz  13519  elfz2nn0  13520  fznn0  13521  elfz0add  13528  fzctr  13542  difelfzle  13543  fzoun  13598  fzofzim  13611  fzo1fzo0n0  13617  elincfzoext  13625  elfzodifsumelfzo  13633  fz0add1fz1  13637  zpnn0elfzo  13640  fzossfzop1  13645  ubmelm1fzo  13665  elfznelfzo  13675  flmulnn0  13733  quoremnn0  13762  zmodidfzoimp  13807  modmuladdnn0  13824  modfzo0difsn  13852  expdiv  14022  expnngt1  14150  faclbnd3  14201  bccmpl  14218  bcnp1n  14223  bcval5  14227  bcn2  14228  bcp1m1  14229  hashge2el2difr  14390  fi1uzind  14416  wrdred1  14469  wrdred1hash  14470  ccatalpha  14503  swrdnd0  14567  swrdfv2  14571  swrdsb0eq  14573  swrdsbslen  14574  swrdspsleq  14575  swrdlsw  14577  pfxnd  14597  pfxccatin12lem4  14635  pfxccatin12lem3  14641  pfxccat3  14643  swrdccat  14644  pfxccat3a  14647  revlen  14671  repswswrd  14693  repswccat  14695  cshwidxmodr  14713  cshf1  14719  2cshw  14722  cshweqrep  14730  cshwcshid  14736  cshwcsh2id  14737  cats1fv  14768  swrd2lsw  14861  2swrd2eqwrdeq  14862  isercoll  15577  iseraltlem2  15592  bcxmas  15744  geo2sum2  15783  geomulcvg  15785  risefacval2  15919  fallfacval2  15920  zrisefaccl  15929  zfallfaccl  15930  fallrisefac  15934  bpolylem  15957  fsumkthpow  15965  esum  15989  ege2le3  15999  eftlcl  16018  reeftlcl  16019  eftlub  16020  effsumlt  16022  eirrlem  16115  dvds1  16232  dvdsext  16234  addmodlteqALT  16238  oddnn02np1  16261  oddge22np1  16262  nn0ehalf  16291  nn0o1gt2  16294  nno  16295  nn0o  16296  nn0oddm1d2  16298  divalglem4  16309  divalglem5  16310  modremain  16321  bitsinv1  16355  nn0gcdid0  16434  nn0seqcvgd  16483  algcvga  16492  eucalgf  16496  nonsq  16672  numdenexp  16673  odzdvds  16709  coprimeprodsq  16722  coprimeprodsq2  16723  oddprm  16724  iserodd  16749  pcexp  16773  pcidlem  16786  pc11  16794  dvdsprmpweqle  16800  difsqpwdvds  16801  pcfac  16813  prmunb  16828  hashbc2  16920  cshwshashlem2  17010  chnccat  18534  smndex1ibas  18810  smndex1iidm  18811  smndex2dnrinv  18825  smndex2dlinvh  18827  mulgaddcom  19013  mulginvcom  19014  mulgz  19017  mulgdirlem  19020  mulgass  19026  mndodcongi  19457  oddvdsnn0  19458  odeq  19464  odmulg  19470  efgsdmi  19646  cyggex2  19811  fincygsubgodd  20028  mulgass2  20229  chrrhm  21470  zncrng  21483  znzrh2  21484  zndvds  21488  znchr  21501  znunit  21502  chfacfisf  22770  chfacfisfcpmat  22771  chfacfscmulfsupp  22775  chfacfpmmulfsupp  22779  clmmulg  25029  itgcnlem  25719  degltlem1  26005  plyco0  26125  dgreq0  26199  plydivex  26233  aannenlem1  26264  abelthlem1  26369  abelthlem3  26371  abelthlem8  26377  abelthlem9  26378  advlogexp  26592  cxpexp  26605  leibpi  26880  log2cnv  26882  log2tlbnd  26883  basellem2  27020  sgmnncl  27085  chpp1  27093  bcmono  27216  bcmax  27217  bcp1ctr  27218  lgsneg1  27261  lgsdirnn0  27283  lgsdinn0  27284  2lgslem1c  27332  2lgslem3a1  27339  2lgslem3b1  27340  2lgslem3c1  27341  2lgsoddprmlem2  27348  2sq2  27372  2sqreultlem  27386  dchrisumlem1  27428  qabvle  27564  ostth2lem2  27573  tgldimor  28481  upgrewlkle2  29587  wlkv0  29630  redwlk  29651  pthdadjvtx  29708  pthdlem1  29746  wwlknvtx  29825  wlkiswwlks2lem3  29851  wwlksm1edg  29861  wwlksnred  29872  wwlksnext  29873  clwlkclwwlklem2a1  29974  clwlkclwwlklem2a2  29975  clwlkclwwlklem2fv1  29977  clwlkclwwlklem2fv2  29978  clwlkclwwlklem2a4  29979  clwlkclwwlklem2a  29980  clwlkclwwlklem2  29982  clwlkclwwlk  29984  clwwisshclwwslem  29996  eucrctshift  30225  eucrct2eupth1  30226  eucrct2eupth  30227  numclwwlk5lem  30369  numclwwlk5  30370  numclwwlk7  30373  frgrreggt1  30375  nndiffz1  32773  nn0diffz0  32781  xrge0mulgnn0  33003  hashf2  34118  signsvtn0  34604  nn0ltp1ne  35177  0nn0m1nnn0  35178  pthhashvtx  35193  fz0n  35796  bcneg1  35801  bccolsum  35804  faclimlem3  35810  faclim  35811  iprodfac  35812  poimirlem28  37708  mblfinlem1  37717  mblfinlem2  37718  lcmineqlem2  42143  sticksstones22  42281  gcdnn0id  42447  negexpidd  42799  nacsfix  42829  fzsplit1nn0  42871  eldioph2lem1  42877  fz1eqin  42886  diophin  42889  eq0rabdioph  42893  rexrabdioph  42911  rexzrexnn0  42921  irrapxlem4  42942  pell14qrss1234  42973  pell1qrss14  42985  monotoddzz  43060  rmxypos  43064  ltrmynn0  43065  ltrmxnn0  43066  lermxnn0  43067  rmxnn  43068  rmynn0  43074  jm2.17a  43077  jm2.17b  43078  rmygeid  43081  jm2.18  43105  jm2.19lem3  43108  jm2.19lem4  43109  jm2.22  43112  rmxdiophlem  43132  hbt  43247  proot1ex  43313  fzisoeu  45425  stirlinglem5  46200  elfzlble  47444  subsubelfzo0  47450  2ffzoeq  47451  addmodne  47468  fargshiftfo  47566  fmtnof1  47659  fmtnorec1  47661  goldbachthlem1  47669  odz2prm2pw  47687  flsqrt  47717  lighneallem4  47734  nn0eo  48653  nn0ofldiv2  48657  flnn0div2ge  48658  fllog2  48693  blenpw2  48703  blennngt2o2  48717  nn0digval  48725  dignn0fr  48726  digexp  48732  0dig2nn0e  48737  0dig2nn0o  48738  dig2bits  48739  dignn0flhalflem2  48741  dignn0ehalf  48742  dignn0flhalf  48743  nn0sumshdiglemB  48745