Theorem nn0z 11277

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℕ₀cn0 11169  ℤcz 11254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255

This theorem is referenced by:  nn0negz  11292  nn0ltp1le  11312  nn0leltp1  11313  nn0ltlem1  11314  nn0lt2  11317  nn0lem1lt  11318  fnn0ind  11352  nn0pzuz  11621  nn0ge2m1nnALT  11658  fz1n  12230  ige2m1fz  12299  elfz2nn0  12300  fznn0  12301  elfz0add  12307  fzctr  12320  difelfzle  12321  fzofzim  12382  fzo1fzo0n0  12386  elincfzoext  12393  elfzodifsumelfzo  12401  zpnn0elfzo  12407  fzossfzop1  12412  ubmelm1fzo  12430  elfznelfzo  12439  flmulnn0  12490  quoremnn0  12517  zmodidfzoimp  12562  modmuladdnn0  12576  modfzo0difsn  12604  expdiv  12773  faclbnd3  12941  bccmpl  12958  bcnp1n  12963  bcval5  12967  bcn2  12968  bcp1m1  12969  hashge2el2difr  13118  fi1uzind  13134  fi1uzindOLD  13140  ccatalpha  13228  swrdfv2  13298  swrdsb0eq  13299  swrdsbslen  13300  swrdspsleq  13301  swrdlsw  13304  2swrd1eqwrdeq  13306  swrdccatin12lem1  13335  swrdccatin12lem3  13341  swrdccat3  13343  swrdccat  13344  revlen  13362  repswswrd  13382  repswccat  13383  cshwidxmodr  13401  cshf1  13407  2cshw  13410  cshweqrep  13418  cshwcshid  13424  cshwcsh2id  13425  cats1fv  13455  swrd2lsw  13543  2swrd2eqwrdeq  13544  isercoll  14246  iseraltlem2  14261  bcxmas  14406  geo2sum2  14444  geomulcvg  14446  risefacval2  14580  fallfacval2  14581  zrisefaccl  14590  zfallfaccl  14591  fallrisefac  14595  bpolylem  14618  fsumkthpow  14626  esum  14650  ege2le3  14659  eftlcl  14676  reeftlcl  14677  eftlub  14678  effsumlt  14680  eirrlem  14771  dvds1  14879  dvdsext  14881  addmodlteqALT  14885  oddnn02np1  14910  oddge22np1  14911  nn0ehalf  14933  nn0o1gt2  14935  nno  14936  nn0o  14937  nn0oddm1d2  14939  divalglem4  14957  divalglem5  14958  modremain  14970  bitsinv1  15002  nn0gcdid0  15080  nn0seqcvgd  15121  algcvga  15130  eucalgf  15134  nonsq  15305  odzdvds  15338  coprimeprodsq  15351  coprimeprodsq2  15352  oddprm  15353  iserodd  15378  pcexp  15402  pcidlem  15414  pc11  15422  dvdsprmpweqle  15428  difsqpwdvds  15429  pcfac  15441  prmunb  15456  hashbc2  15548  cshwshashlem2  15641  mulgaddcom  17387  mulginvcom  17388  mulgz  17391  mulgdirlem  17395  mulgass  17402  mndodcongi  17785  oddvdsnn0  17786  odeq  17792  odmulg  17796  efgsdmi  17968  cyggex2  18121  mulgass2  18424  chrrhm  19698  zncrng  19712  znzrh2  19713  zndvds  19717  znchr  19730  znunit  19731  chfacfisf  20478  chfacfisfcpmat  20479  chfacfscmulfsupp  20483  chfacfpmmulfsupp  20487  clmmulg  22709  itgcnlem  23362  degltlem1  23636  plyco0  23752  dgreq0  23825  plydivex  23856  aannenlem1  23887  abelthlem1  23989  abelthlem3  23991  abelthlem8  23997  abelthlem9  23998  advlogexp  24201  cxpexp  24214  leibpilem1  24467  leibpi  24469  log2cnv  24471  log2tlbnd  24472  basellem2  24608  sgmnncl  24673  chpp1  24681  bcmono  24802  bcmax  24803  bcp1ctr  24804  lgsneg1  24847  lgsdirnn0  24869  lgsdinn0  24870  2lgslem1c  24918  2lgslem3a1  24925  2lgslem3b1  24926  2lgslem3c1  24927  2lgsoddprmlem2  24934  dchrisumlem1  24978  qabvle  25114  ostth2lem2  25123  tgldimor  25197  redwlklem  26135  redwlk  26136  fargshiftlem  26162  fargshiftfo  26166  wlkiswwlk2lem3  26221  wwlknred  26251  wwlknext  26252  wwlkm1edg  26263  wwlkextproplem1  26269  wlkv0  26288  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2a2  26308  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwlkisclwwlk  26317  clwwisshclwwlem  26334  clwlkfclwwlk2wrd  26367  clwlkfclwwlk  26371  clwlkf1clwwlklem3  26375  nbhashuvtx1  26442  frgrawopreglem2  26572  numclwwlk5lem  26638  numclwwlk5  26639  numclwwlk7  26641  frgrareggt1  26643  nndiffz1  28936  xrge0mulgnn0  29020  hashf2  29473  signsvtn0  29973  fz0n  30869  bcneg1  30875  bccolsum  30878  faclimlem3  30884  faclim  30885  iprodfac  30886  poimirlem28  32607  mblfinlem1  32616  mblfinlem2  32617  nacsfix  36293  fzsplit1nn0  36335  eldioph2lem1  36341  fz1eqin  36350  diophin  36354  eq0rabdioph  36358  rexrabdioph  36376  rexzrexnn0  36386  irrapxlem4  36407  pell14qrss1234  36438  pell1qrss14  36450  monotoddzz  36526  rmxypos  36532  ltrmynn0  36533  ltrmxnn0  36534  lermxnn0  36535  rmxnn  36536  rmynn0  36542  jm2.17a  36545  jm2.17b  36546  rmygeid  36549  jm2.18  36573  jm2.19lem3  36576  jm2.19lem4  36577  jm2.22  36580  rmxdiophlem  36600  hbt  36719  proot1ex  36798  fzisoeu  38455  stirlinglem5  38971  fmtnof1  39985  fmtnorec1  39987  goldbachthlem1  39995  odz2prm2pw  40013  flsqrt  40046  lighneallem4  40065  wrdred1  40240  wrdred1hash  40241  pfxnd  40258  pfxccat3  40289  pfxccat3a  40292  elfzlble  40357  subsubelfzo0  40359  2ffzoeq  40361  upgrewlkle2  40808  1wlkv0  40859  red1wlk  40881  pthdadjvtx  40936  pthdlem1  40972  1wlkiswwlks2lem3  41068  wwlksm1edg  41078  wwlksnred  41098  wwlksnext  41099  clwlkclwwlklem2a1  41201  clwlkclwwlklem2a2  41202  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwlkclwwlk  41211  clwwisshclwwslem  41234  clwlksfclwwlk2wrd  41265  clwlksfclwwlk  41269  clwlksf1clwwlklem3  41274  eucrctshift  41411  eucrct2eupth1  41412  eucrct2eupth  41413  av-numclwwlk5lem  41541  av-numclwwlk5  41542  av-numclwwlk7  41545  av-frgrareggt1  41547  nn0le2is012  41938  nn0eo  42116  nn0ofldiv2  42120  flnn0div2ge  42121  fllog2  42160  blenpw2  42170  blennngt2o2  42184  nn0digval  42192  dignn0fr  42193  digexp  42199  0dig2nn0e  42204  0dig2nn0o  42205  dig2bits  42206  dignn0flhalflem2  42208  dignn0ehalf  42209  dignn0flhalf  42210  nn0sumshdiglemB  42212