Theorem nn0z 12008

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕ₀cn0 11900  ℤcz 11984

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-i2m1 10607  ax-1ne0 10608  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-neg 10875  df-nn 11641  df-n0 11901  df-z 11985

This theorem is referenced by:  nn0negz  12023  nn0ltp1le  12043  nn0leltp1  12044  nn0ltlem1  12045  nn0lt2  12048  nn0le2is012  12049  nn0lem1lt  12050  fnn0ind  12084  nn0pzuz  12308  nn0ge2m1nnALT  12345  fz1n  12928  ige2m1fz  13000  elfz2nn0  13001  fznn0  13002  elfz0add  13009  fzctr  13022  difelfzle  13023  fzoun  13077  fzofzim  13087  fzo1fzo0n0  13091  elincfzoext  13098  elfzodifsumelfzo  13106  fz0add1fz1  13110  zpnn0elfzo  13113  fzossfzop1  13118  ubmelm1fzo  13136  elfznelfzo  13145  flmulnn0  13200  quoremnn0  13227  zmodidfzoimp  13272  modmuladdnn0  13286  modfzo0difsn  13314  expdiv  13483  expnngt1  13605  faclbnd3  13655  bccmpl  13672  bcnp1n  13677  bcval5  13681  bcn2  13682  bcp1m1  13683  hashge2el2difr  13842  fi1uzind  13858  wrdred1  13914  wrdred1hash  13915  ccatalpha  13949  swrdnd0  14021  swrdfv2  14025  swrdsb0eq  14027  swrdsbslen  14028  swrdspsleq  14029  swrdlsw  14031  pfxnd  14051  pfxccatin12lem4  14090  pfxccatin12lem3  14096  pfxccat3  14098  swrdccat  14099  pfxccat3a  14102  revlen  14126  repswswrd  14148  repswccat  14150  cshwidxmodr  14168  cshf1  14174  2cshw  14177  cshweqrep  14185  cshwcshid  14191  cshwcsh2id  14192  cats1fv  14223  swrd2lsw  14316  2swrd2eqwrdeq  14317  isercoll  15026  iseraltlem2  15041  bcxmas  15192  geo2sum2  15232  geomulcvg  15234  risefacval2  15366  fallfacval2  15367  zrisefaccl  15376  zfallfaccl  15377  fallrisefac  15381  bpolylem  15404  fsumkthpow  15412  esum  15436  ege2le3  15445  eftlcl  15462  reeftlcl  15463  eftlub  15464  effsumlt  15466  eirrlem  15559  dvds1  15671  dvdsext  15673  addmodlteqALT  15677  oddnn02np1  15699  oddge22np1  15700  nn0ehalf  15731  nn0o1gt2  15734  nno  15735  nn0o  15736  nn0oddm1d2  15738  divalglem4  15749  divalglem5  15750  modremain  15761  bitsinv1  15793  nn0gcdid0  15871  nn0seqcvgd  15916  algcvga  15925  eucalgf  15929  nonsq  16101  odzdvds  16134  coprimeprodsq  16147  coprimeprodsq2  16148  oddprm  16149  iserodd  16174  pcexp  16198  pcidlem  16210  pc11  16218  dvdsprmpweqle  16224  difsqpwdvds  16225  pcfac  16237  prmunb  16252  hashbc2  16344  cshwshashlem2  16432  smndex1ibas  18067  smndex1iidm  18068  smndex2dnrinv  18082  smndex2dlinvh  18084  mulgaddcom  18253  mulginvcom  18254  mulgz  18257  mulgdirlem  18260  mulgass  18266  mndodcongi  18673  oddvdsnn0  18674  odeq  18680  odmulg  18685  efgsdmi  18860  cyggex2  19019  fincygsubgodd  19236  mulgass2  19353  chrrhm  20680  zncrng  20693  znzrh2  20694  zndvds  20698  znchr  20711  znunit  20712  chfacfisf  21464  chfacfisfcpmat  21465  chfacfscmulfsupp  21469  chfacfpmmulfsupp  21473  clmmulg  23707  itgcnlem  24392  degltlem1  24668  plyco0  24784  dgreq0  24857  plydivex  24888  aannenlem1  24919  abelthlem1  25021  abelthlem3  25023  abelthlem8  25029  abelthlem9  25030  advlogexp  25240  cxpexp  25253  leibpi  25522  log2cnv  25524  log2tlbnd  25525  basellem2  25661  sgmnncl  25726  chpp1  25734  bcmono  25855  bcmax  25856  bcp1ctr  25857  lgsneg1  25900  lgsdirnn0  25922  lgsdinn0  25923  2lgslem1c  25971  2lgslem3a1  25978  2lgslem3b1  25979  2lgslem3c1  25980  2lgsoddprmlem2  25987  2sq2  26011  2sqreultlem  26025  dchrisumlem1  26067  qabvle  26203  ostth2lem2  26212  tgldimor  26290  upgrewlkle2  27390  wlkv0  27434  redwlk  27456  pthdadjvtx  27513  pthdlem1  27549  wwlknvtx  27625  wlkiswwlks2lem3  27651  wwlksm1edg  27661  wwlksnred  27672  wwlksnext  27673  clwlkclwwlklem2a1  27772  clwlkclwwlklem2a2  27773  clwlkclwwlklem2fv1  27775  clwlkclwwlklem2fv2  27776  clwlkclwwlklem2a4  27777  clwlkclwwlklem2a  27778  clwlkclwwlklem2  27780  clwlkclwwlk  27782  clwwisshclwwslem  27794  eucrctshift  28024  eucrct2eupth1  28025  eucrct2eupth  28026  numclwwlk5lem  28168  numclwwlk5  28169  numclwwlk7  28172  frgrreggt1  28174  nndiffz1  30511  xrge0mulgnn0  30678  hashf2  31345  signsvtn0  31842  nn0ltp1ne  32352  0nn0m1nnn0  32353  pthhashvtx  32376  fz0n  32964  bcneg1  32970  bccolsum  32973  faclimlem3  32979  faclim  32980  iprodfac  32981  poimirlem28  34922  mblfinlem1  34931  mblfinlem2  34932  numdenexp  39193  negexpidd  39286  nacsfix  39316  fzsplit1nn0  39358  eldioph2lem1  39364  fz1eqin  39373  diophin  39376  eq0rabdioph  39380  rexrabdioph  39398  rexzrexnn0  39408  irrapxlem4  39429  pell14qrss1234  39460  pell1qrss14  39472  monotoddzz  39547  rmxypos  39551  ltrmynn0  39552  ltrmxnn0  39553  lermxnn0  39554  rmxnn  39555  rmynn0  39561  jm2.17a  39564  jm2.17b  39565  rmygeid  39568  jm2.18  39592  jm2.19lem3  39595  jm2.19lem4  39596  jm2.22  39599  rmxdiophlem  39619  hbt  39737  proot1ex  39808  fzisoeu  41574  stirlinglem5  42370  elfzlble  43527  subsubelfzo0  43533  2ffzoeq  43535  fargshiftfo  43609  fmtnof1  43704  fmtnorec1  43706  goldbachthlem1  43714  odz2prm2pw  43732  flsqrt  43763  lighneallem4  43782  nn0eo  44595  nn0ofldiv2  44599  flnn0div2ge  44600  fllog2  44635  blenpw2  44645  blennngt2o2  44659  nn0digval  44667  dignn0fr  44668  digexp  44674  0dig2nn0e  44679  0dig2nn0o  44680  dig2bits  44681  dignn0flhalflem2  44683  dignn0ehalf  44684  dignn0flhalf  44685  nn0sumshdiglemB  44687