Theorem nn0z 12546

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℕ₀cn0 12435  ℤcz 12522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-i2m1 11104  ax-1ne0 11105  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-neg 11378  df-nn 12173  df-n0 12436  df-z 12523

This theorem is referenced by:  nn0negz  12563  nn0ltp1le  12585  nn0leltp1  12586  nn0ltlem1  12587  nn0lt2  12590  nn0le2is012  12591  nn0lem1lt  12592  fnn0ind  12626  nn0pzuz  12853  nn0ge2m1nnALT  12890  fz1n  13494  ige2m1fz  13569  elfz2nn0  13570  fznn0  13571  elfz0add  13578  fzctr  13592  difelfzle  13593  fzoun  13649  fzofzim  13662  fzo1fzo0n0  13668  elincfzoext  13676  elfzodifsumelfzo  13684  fz0add1fz1  13688  zpnn0elfzo  13691  fzossfzop1  13696  ubmelm1fzo  13716  elfznelfzo  13726  flmulnn0  13784  quoremnn0  13813  zmodidfzoimp  13858  modmuladdnn0  13875  modfzo0difsn  13903  expdiv  14073  expnngt1  14201  faclbnd3  14252  bccmpl  14269  bcnp1n  14274  bcval5  14278  bcn2  14279  bcp1m1  14280  hashge2el2difr  14441  fi1uzind  14467  wrdred1  14520  wrdred1hash  14521  ccatalpha  14554  swrdnd0  14618  swrdfv2  14622  swrdsb0eq  14624  swrdsbslen  14625  swrdspsleq  14626  swrdlsw  14628  pfxnd  14648  pfxccatin12lem4  14686  pfxccatin12lem3  14692  pfxccat3  14694  swrdccat  14695  pfxccat3a  14698  revlen  14722  repswswrd  14744  repswccat  14746  cshwidxmodr  14764  cshf1  14770  2cshw  14773  cshweqrep  14781  cshwcshid  14787  cshwcsh2id  14788  cats1fv  14819  swrd2lsw  14912  2swrd2eqwrdeq  14913  isercoll  15628  iseraltlem2  15643  bcxmas  15798  geo2sum2  15837  geomulcvg  15839  risefacval2  15973  fallfacval2  15974  zrisefaccl  15983  zfallfaccl  15984  fallrisefac  15988  bpolylem  16011  fsumkthpow  16019  esum  16043  ege2le3  16053  eftlcl  16072  reeftlcl  16073  eftlub  16074  effsumlt  16076  eirrlem  16169  dvds1  16286  dvdsext  16288  addmodlteqALT  16292  oddnn02np1  16315  oddge22np1  16316  nn0ehalf  16345  nn0o1gt2  16348  nno  16349  nn0o  16350  nn0oddm1d2  16352  divalglem4  16363  divalglem5  16364  modremain  16375  bitsinv1  16409  nn0gcdid0  16488  nn0seqcvgd  16537  algcvga  16546  eucalgf  16550  nonsq  16727  numdenexp  16728  odzdvds  16764  coprimeprodsq  16777  coprimeprodsq2  16778  oddprm  16779  iserodd  16804  pcexp  16828  pcidlem  16841  pc11  16849  dvdsprmpweqle  16855  difsqpwdvds  16856  pcfac  16868  prmunb  16883  hashbc2  16975  cshwshashlem2  17065  chnccat  18590  smndex1ibas  18866  smndex1iidm  18867  smndex2dnrinv  18884  smndex2dlinvh  18886  mulgaddcom  19072  mulginvcom  19073  mulgz  19076  mulgdirlem  19079  mulgass  19085  mndodcongi  19516  oddvdsnn0  19517  odeq  19523  odmulg  19529  efgsdmi  19705  cyggex2  19870  fincygsubgodd  20087  mulgass2  20288  chrrhm  21513  zncrng  21526  znzrh2  21527  zndvds  21531  znchr  21544  znunit  21545  chfacfisf  22844  chfacfisfcpmat  22845  chfacfscmulfsupp  22849  chfacfpmmulfsupp  22853  clmmulg  25093  itgcnlem  25782  degltlem1  26062  plyco0  26182  dgreq0  26255  plydivex  26288  aannenlem1  26319  abelthlem1  26421  abelthlem3  26423  abelthlem8  26429  abelthlem9  26430  advlogexp  26644  cxpexp  26657  leibpi  26931  log2cnv  26933  log2tlbnd  26934  basellem2  27070  sgmnncl  27135  chpp1  27143  bcmono  27265  bcmax  27266  bcp1ctr  27267  lgsneg1  27310  lgsdirnn0  27332  lgsdinn0  27333  2lgslem1c  27381  2lgslem3a1  27388  2lgslem3b1  27389  2lgslem3c1  27390  2lgsoddprmlem2  27397  2sq2  27421  2sqreultlem  27435  dchrisumlem1  27477  qabvle  27613  ostth2lem2  27622  tgldimor  28595  upgrewlkle2  29700  wlkv0  29743  redwlk  29764  pthdadjvtx  29821  pthdlem1  29859  wwlknvtx  29938  wlkiswwlks2lem3  29964  wwlksm1edg  29974  wwlksnred  29985  wwlksnext  29986  clwlkclwwlklem2a1  30087  clwlkclwwlklem2a2  30088  clwlkclwwlklem2fv1  30090  clwlkclwwlklem2fv2  30091  clwlkclwwlklem2a4  30092  clwlkclwwlklem2a  30093  clwlkclwwlklem2  30095  clwlkclwwlk  30097  clwwisshclwwslem  30109  eucrctshift  30338  eucrct2eupth1  30339  eucrct2eupth  30340  numclwwlk5lem  30482  numclwwlk5  30483  numclwwlk7  30486  frgrreggt1  30488  nndiffz1  32885  nn0diffz0  32893  xrge0mulgnn0  33101  hashf2  34275  signsvtn0  34761  nn0ltp1ne  35347  0nn0m1nnn0  35348  pthhashvtx  35363  fz0n  35966  bcneg1  35971  bccolsum  35974  faclimlem3  35980  faclim  35981  iprodfac  35982  poimirlem28  38022  mblfinlem1  38031  mblfinlem2  38032  lcmineqlem2  42522  sticksstones22  42660  gcdnn0id  42813  negexpidd  43138  nacsfix  43168  fzsplit1nn0  43210  eldioph2lem1  43216  fz1eqin  43225  diophin  43228  eq0rabdioph  43232  rexrabdioph  43246  rexzrexnn0  43256  irrapxlem4  43277  pell14qrss1234  43308  pell1qrss14  43320  monotoddzz  43395  rmxypos  43399  ltrmynn0  43400  ltrmxnn0  43401  lermxnn0  43402  rmxnn  43403  rmynn0  43409  jm2.17a  43412  jm2.17b  43413  rmygeid  43416  jm2.18  43440  jm2.19lem3  43443  jm2.19lem4  43444  jm2.22  43447  rmxdiophlem  43467  hbt  43582  proot1ex  43648  fzisoeu  45755  stirlinglem5  46528  elfzlble  47790  subsubelfzo0  47797  2ffzoeq  47798  addmodne  47820  fargshiftfo  47924  fmtnof1  48020  fmtnorec1  48022  goldbachthlem1  48030  odz2prm2pw  48048  flsqrt  48078  lighneallem4  48095  nn0eo  49026  nn0ofldiv2  49030  flnn0div2ge  49031  fllog2  49066  blenpw2  49076  blennngt2o2  49090  nn0digval  49098  dignn0fr  49099  digexp  49105  0dig2nn0e  49110  0dig2nn0o  49111  dig2bits  49112  dignn0flhalflem2  49114  dignn0ehalf  49115  dignn0flhalf  49116  nn0sumshdiglemB  49118