Theorem nn0z 12664

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕ₀cn0 12553  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-neg 11523  df-nn 12294  df-n0 12554  df-z 12640

This theorem is referenced by:  nn0negz  12681  nn0ltp1le  12701  nn0leltp1  12702  nn0ltlem1  12703  nn0lt2  12706  nn0le2is012  12707  nn0lem1lt  12708  fnn0ind  12742  nn0pzuz  12970  nn0ge2m1nnALT  13007  fz1n  13602  ige2m1fz  13674  elfz2nn0  13675  fznn0  13676  elfz0add  13683  fzctr  13697  difelfzle  13698  fzoun  13753  fzofzim  13763  fzo1fzo0n0  13767  elincfzoext  13774  elfzodifsumelfzo  13782  fz0add1fz1  13786  zpnn0elfzo  13789  fzossfzop1  13794  ubmelm1fzo  13813  elfznelfzo  13822  flmulnn0  13878  quoremnn0  13907  zmodidfzoimp  13952  modmuladdnn0  13966  modfzo0difsn  13994  expdiv  14164  expnngt1  14290  faclbnd3  14341  bccmpl  14358  bcnp1n  14363  bcval5  14367  bcn2  14368  bcp1m1  14369  hashge2el2difr  14530  fi1uzind  14556  wrdred1  14608  wrdred1hash  14609  ccatalpha  14641  swrdnd0  14705  swrdfv2  14709  swrdsb0eq  14711  swrdsbslen  14712  swrdspsleq  14713  swrdlsw  14715  pfxnd  14735  pfxccatin12lem4  14774  pfxccatin12lem3  14780  pfxccat3  14782  swrdccat  14783  pfxccat3a  14786  revlen  14810  repswswrd  14832  repswccat  14834  cshwidxmodr  14852  cshf1  14858  2cshw  14861  cshweqrep  14869  cshwcshid  14876  cshwcsh2id  14877  cats1fv  14908  swrd2lsw  15001  2swrd2eqwrdeq  15002  isercoll  15716  iseraltlem2  15731  bcxmas  15883  geo2sum2  15922  geomulcvg  15924  risefacval2  16058  fallfacval2  16059  zrisefaccl  16068  zfallfaccl  16069  fallrisefac  16073  bpolylem  16096  fsumkthpow  16104  esum  16128  ege2le3  16138  eftlcl  16155  reeftlcl  16156  eftlub  16157  effsumlt  16159  eirrlem  16252  dvds1  16367  dvdsext  16369  addmodlteqALT  16373  oddnn02np1  16396  oddge22np1  16397  nn0ehalf  16426  nn0o1gt2  16429  nno  16430  nn0o  16431  nn0oddm1d2  16433  divalglem4  16444  divalglem5  16445  modremain  16456  bitsinv1  16488  nn0gcdid0  16567  nn0seqcvgd  16617  algcvga  16626  eucalgf  16630  nonsq  16806  numdenexp  16807  odzdvds  16842  coprimeprodsq  16855  coprimeprodsq2  16856  oddprm  16857  iserodd  16882  pcexp  16906  pcidlem  16919  pc11  16927  dvdsprmpweqle  16933  difsqpwdvds  16934  pcfac  16946  prmunb  16961  hashbc2  17053  cshwshashlem2  17144  smndex1ibas  18935  smndex1iidm  18936  smndex2dnrinv  18950  smndex2dlinvh  18952  mulgaddcom  19138  mulginvcom  19139  mulgz  19142  mulgdirlem  19145  mulgass  19151  mndodcongi  19585  oddvdsnn0  19586  odeq  19592  odmulg  19598  efgsdmi  19774  cyggex2  19939  fincygsubgodd  20156  mulgass2  20332  chrrhm  21569  zncrng  21586  znzrh2  21587  zndvds  21591  znchr  21604  znunit  21605  chfacfisf  22881  chfacfisfcpmat  22882  chfacfscmulfsupp  22886  chfacfpmmulfsupp  22890  clmmulg  25153  itgcnlem  25845  degltlem1  26131  plyco0  26251  dgreq0  26325  plydivex  26357  aannenlem1  26388  abelthlem1  26493  abelthlem3  26495  abelthlem8  26501  abelthlem9  26502  advlogexp  26715  cxpexp  26728  leibpi  27003  log2cnv  27005  log2tlbnd  27006  basellem2  27143  sgmnncl  27208  chpp1  27216  bcmono  27339  bcmax  27340  bcp1ctr  27341  lgsneg1  27384  lgsdirnn0  27406  lgsdinn0  27407  2lgslem1c  27455  2lgslem3a1  27462  2lgslem3b1  27463  2lgslem3c1  27464  2lgsoddprmlem2  27471  2sq2  27495  2sqreultlem  27509  dchrisumlem1  27551  qabvle  27687  ostth2lem2  27696  tgldimor  28528  upgrewlkle2  29642  wlkv0  29687  redwlk  29708  pthdadjvtx  29766  pthdlem1  29802  wwlknvtx  29878  wlkiswwlks2lem3  29904  wwlksm1edg  29914  wwlksnred  29925  wwlksnext  29926  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a2  30025  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlk  30034  clwwisshclwwslem  30046  eucrctshift  30275  eucrct2eupth1  30276  eucrct2eupth  30277  numclwwlk5lem  30419  numclwwlk5  30420  numclwwlk7  30423  frgrreggt1  30425  nndiffz1  32791  xrge0mulgnn0  33001  hashf2  34048  signsvtn0  34547  nn0ltp1ne  35079  0nn0m1nnn0  35080  pthhashvtx  35095  fz0n  35693  bcneg1  35698  bccolsum  35701  faclimlem3  35707  faclim  35708  iprodfac  35709  poimirlem28  37608  mblfinlem1  37617  mblfinlem2  37618  lcmineqlem2  41987  sticksstones22  42125  gcdnn0id  42316  negexpidd  42638  nacsfix  42668  fzsplit1nn0  42710  eldioph2lem1  42716  fz1eqin  42725  diophin  42728  eq0rabdioph  42732  rexrabdioph  42750  rexzrexnn0  42760  irrapxlem4  42781  pell14qrss1234  42812  pell1qrss14  42824  monotoddzz  42900  rmxypos  42904  ltrmynn0  42905  ltrmxnn0  42906  lermxnn0  42907  rmxnn  42908  rmynn0  42914  jm2.17a  42917  jm2.17b  42918  rmygeid  42921  jm2.18  42945  jm2.19lem3  42948  jm2.19lem4  42949  jm2.22  42952  rmxdiophlem  42972  hbt  43087  proot1ex  43157  fzisoeu  45215  stirlinglem5  45999  elfzlble  47235  subsubelfzo0  47241  2ffzoeq  47242  fargshiftfo  47316  fmtnof1  47409  fmtnorec1  47411  goldbachthlem1  47419  odz2prm2pw  47437  flsqrt  47467  lighneallem4  47484  nn0eo  48262  nn0ofldiv2  48266  flnn0div2ge  48267  fllog2  48302  blenpw2  48312  blennngt2o2  48326  nn0digval  48334  dignn0fr  48335  digexp  48341  0dig2nn0e  48346  0dig2nn0o  48347  dig2bits  48348  dignn0flhalflem2  48350  dignn0ehalf  48351  dignn0flhalf  48352  nn0sumshdiglemB  48354