Theorem nn0z 11999

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℕ₀cn0 11891  ℤcz 11975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-i2m1 10599  ax-1ne0 10600  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-neg 10867  df-nn 11633  df-n0 11892  df-z 11976

This theorem is referenced by:  nn0negz  12014  nn0ltp1le  12034  nn0leltp1  12035  nn0ltlem1  12036  nn0lt2  12039  nn0le2is012  12040  nn0lem1lt  12041  fnn0ind  12075  nn0pzuz  12299  nn0ge2m1nnALT  12336  fz1n  12919  ige2m1fz  12991  elfz2nn0  12992  fznn0  12993  elfz0add  13000  fzctr  13013  difelfzle  13014  fzoun  13068  fzofzim  13078  fzo1fzo0n0  13082  elincfzoext  13089  elfzodifsumelfzo  13097  fz0add1fz1  13101  zpnn0elfzo  13104  fzossfzop1  13109  ubmelm1fzo  13127  elfznelfzo  13136  flmulnn0  13191  quoremnn0  13218  zmodidfzoimp  13263  modmuladdnn0  13277  modfzo0difsn  13305  expdiv  13474  expnngt1  13596  faclbnd3  13646  bccmpl  13663  bcnp1n  13668  bcval5  13672  bcn2  13673  bcp1m1  13674  hashge2el2difr  13833  fi1uzind  13849  wrdred1  13906  wrdred1hash  13907  ccatalpha  13941  swrdnd0  14013  swrdfv2  14017  swrdsb0eq  14019  swrdsbslen  14020  swrdspsleq  14021  swrdlsw  14023  pfxnd  14043  pfxccatin12lem4  14082  pfxccatin12lem3  14088  pfxccat3  14090  swrdccat  14091  pfxccat3a  14094  revlen  14118  repswswrd  14140  repswccat  14142  cshwidxmodr  14160  cshf1  14166  2cshw  14169  cshweqrep  14177  cshwcshid  14183  cshwcsh2id  14184  cats1fv  14215  swrd2lsw  14308  2swrd2eqwrdeq  14309  isercoll  15018  iseraltlem2  15033  bcxmas  15184  geo2sum2  15224  geomulcvg  15226  risefacval2  15358  fallfacval2  15359  zrisefaccl  15368  zfallfaccl  15369  fallrisefac  15373  bpolylem  15396  fsumkthpow  15404  esum  15428  ege2le3  15437  eftlcl  15454  reeftlcl  15455  eftlub  15456  effsumlt  15458  eirrlem  15551  dvds1  15663  dvdsext  15665  addmodlteqALT  15669  oddnn02np1  15691  oddge22np1  15692  nn0ehalf  15723  nn0o1gt2  15726  nno  15727  nn0o  15728  nn0oddm1d2  15730  divalglem4  15741  divalglem5  15742  modremain  15753  bitsinv1  15785  nn0gcdid0  15863  nn0seqcvgd  15908  algcvga  15917  eucalgf  15921  nonsq  16093  odzdvds  16126  coprimeprodsq  16139  coprimeprodsq2  16140  oddprm  16141  iserodd  16166  pcexp  16190  pcidlem  16202  pc11  16210  dvdsprmpweqle  16216  difsqpwdvds  16217  pcfac  16229  prmunb  16244  hashbc2  16336  cshwshashlem2  16424  smndex1ibas  18059  smndex1iidm  18060  smndex2dnrinv  18074  smndex2dlinvh  18076  mulgaddcom  18245  mulginvcom  18246  mulgz  18249  mulgdirlem  18252  mulgass  18258  mndodcongi  18665  oddvdsnn0  18666  odeq  18672  odmulg  18677  efgsdmi  18852  cyggex2  19011  fincygsubgodd  19228  mulgass2  19345  chrrhm  20672  zncrng  20685  znzrh2  20686  zndvds  20690  znchr  20703  znunit  20704  chfacfisf  21456  chfacfisfcpmat  21457  chfacfscmulfsupp  21461  chfacfpmmulfsupp  21465  clmmulg  23699  itgcnlem  24384  degltlem1  24660  plyco0  24776  dgreq0  24849  plydivex  24880  aannenlem1  24911  abelthlem1  25013  abelthlem3  25015  abelthlem8  25021  abelthlem9  25022  advlogexp  25232  cxpexp  25245  leibpi  25514  log2cnv  25516  log2tlbnd  25517  basellem2  25653  sgmnncl  25718  chpp1  25726  bcmono  25847  bcmax  25848  bcp1ctr  25849  lgsneg1  25892  lgsdirnn0  25914  lgsdinn0  25915  2lgslem1c  25963  2lgslem3a1  25970  2lgslem3b1  25971  2lgslem3c1  25972  2lgsoddprmlem2  25979  2sq2  26003  2sqreultlem  26017  dchrisumlem1  26059  qabvle  26195  ostth2lem2  26204  tgldimor  26282  upgrewlkle2  27382  wlkv0  27426  redwlk  27448  pthdadjvtx  27505  pthdlem1  27541  wwlknvtx  27617  wlkiswwlks2lem3  27643  wwlksm1edg  27653  wwlksnred  27664  wwlksnext  27665  clwlkclwwlklem2a1  27764  clwlkclwwlklem2a2  27765  clwlkclwwlklem2fv1  27767  clwlkclwwlklem2fv2  27768  clwlkclwwlklem2a4  27769  clwlkclwwlklem2a  27770  clwlkclwwlklem2  27772  clwlkclwwlk  27774  clwwisshclwwslem  27786  eucrctshift  28016  eucrct2eupth1  28017  eucrct2eupth  28018  numclwwlk5lem  28160  numclwwlk5  28161  numclwwlk7  28164  frgrreggt1  28166  nndiffz1  30503  xrge0mulgnn0  30671  hashf2  31338  signsvtn0  31835  nn0ltp1ne  32345  0nn0m1nnn0  32346  pthhashvtx  32369  fz0n  32957  bcneg1  32963  bccolsum  32966  faclimlem3  32972  faclim  32973  iprodfac  32974  poimirlem28  34914  mblfinlem1  34923  mblfinlem2  34924  numdenexp  39179  negexpidd  39272  nacsfix  39302  fzsplit1nn0  39344  eldioph2lem1  39350  fz1eqin  39359  diophin  39362  eq0rabdioph  39366  rexrabdioph  39384  rexzrexnn0  39394  irrapxlem4  39415  pell14qrss1234  39446  pell1qrss14  39458  monotoddzz  39533  rmxypos  39537  ltrmynn0  39538  ltrmxnn0  39539  lermxnn0  39540  rmxnn  39541  rmynn0  39547  jm2.17a  39550  jm2.17b  39551  rmygeid  39554  jm2.18  39578  jm2.19lem3  39581  jm2.19lem4  39582  jm2.22  39585  rmxdiophlem  39605  hbt  39723  proot1ex  39794  fzisoeu  41560  stirlinglem5  42357  elfzlble  43514  subsubelfzo0  43520  2ffzoeq  43522  fargshiftfo  43596  fmtnof1  43691  fmtnorec1  43693  goldbachthlem1  43701  odz2prm2pw  43719  flsqrt  43750  lighneallem4  43769  nn0eo  44582  nn0ofldiv2  44586  flnn0div2ge  44587  fllog2  44622  blenpw2  44632  blennngt2o2  44646  nn0digval  44654  dignn0fr  44655  digexp  44661  0dig2nn0e  44666  0dig2nn0o  44667  dig2bits  44668  dignn0flhalflem2  44670  dignn0ehalf  44671  dignn0flhalf  44672  nn0sumshdiglemB  44674