Theorem nn0z 12635

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℕ₀cn0 12523  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-neg 11492  df-nn 12264  df-n0 12524  df-z 12611

This theorem is referenced by:  nn0negz  12652  nn0ltp1le  12673  nn0leltp1  12674  nn0ltlem1  12675  nn0lt2  12678  nn0le2is012  12679  nn0lem1lt  12680  fnn0ind  12714  nn0pzuz  12944  nn0ge2m1nnALT  12981  fz1n  13578  ige2m1fz  13653  elfz2nn0  13654  fznn0  13655  elfz0add  13662  fzctr  13676  difelfzle  13677  fzoun  13732  fzofzim  13745  fzo1fzo0n0  13750  elincfzoext  13758  elfzodifsumelfzo  13766  fz0add1fz1  13770  zpnn0elfzo  13773  fzossfzop1  13778  ubmelm1fzo  13798  elfznelfzo  13807  flmulnn0  13863  quoremnn0  13892  zmodidfzoimp  13937  modmuladdnn0  13952  modfzo0difsn  13980  expdiv  14150  expnngt1  14276  faclbnd3  14327  bccmpl  14344  bcnp1n  14349  bcval5  14353  bcn2  14354  bcp1m1  14355  hashge2el2difr  14516  fi1uzind  14542  wrdred1  14594  wrdred1hash  14595  ccatalpha  14627  swrdnd0  14691  swrdfv2  14695  swrdsb0eq  14697  swrdsbslen  14698  swrdspsleq  14699  swrdlsw  14701  pfxnd  14721  pfxccatin12lem4  14760  pfxccatin12lem3  14766  pfxccat3  14768  swrdccat  14769  pfxccat3a  14772  revlen  14796  repswswrd  14818  repswccat  14820  cshwidxmodr  14838  cshf1  14844  2cshw  14847  cshweqrep  14855  cshwcshid  14862  cshwcsh2id  14863  cats1fv  14894  swrd2lsw  14987  2swrd2eqwrdeq  14988  isercoll  15700  iseraltlem2  15715  bcxmas  15867  geo2sum2  15906  geomulcvg  15908  risefacval2  16042  fallfacval2  16043  zrisefaccl  16052  zfallfaccl  16053  fallrisefac  16057  bpolylem  16080  fsumkthpow  16088  esum  16112  ege2le3  16122  eftlcl  16139  reeftlcl  16140  eftlub  16141  effsumlt  16143  eirrlem  16236  dvds1  16352  dvdsext  16354  addmodlteqALT  16358  oddnn02np1  16381  oddge22np1  16382  nn0ehalf  16411  nn0o1gt2  16414  nno  16415  nn0o  16416  nn0oddm1d2  16418  divalglem4  16429  divalglem5  16430  modremain  16441  bitsinv1  16475  nn0gcdid0  16554  nn0seqcvgd  16603  algcvga  16612  eucalgf  16616  nonsq  16792  numdenexp  16793  odzdvds  16828  coprimeprodsq  16841  coprimeprodsq2  16842  oddprm  16843  iserodd  16868  pcexp  16892  pcidlem  16905  pc11  16913  dvdsprmpweqle  16919  difsqpwdvds  16920  pcfac  16932  prmunb  16947  hashbc2  17039  cshwshashlem2  17130  smndex1ibas  18925  smndex1iidm  18926  smndex2dnrinv  18940  smndex2dlinvh  18942  mulgaddcom  19128  mulginvcom  19129  mulgz  19132  mulgdirlem  19135  mulgass  19141  mndodcongi  19575  oddvdsnn0  19576  odeq  19582  odmulg  19588  efgsdmi  19764  cyggex2  19929  fincygsubgodd  20146  mulgass2  20322  chrrhm  21563  zncrng  21580  znzrh2  21581  zndvds  21585  znchr  21598  znunit  21599  chfacfisf  22875  chfacfisfcpmat  22876  chfacfscmulfsupp  22880  chfacfpmmulfsupp  22884  clmmulg  25147  itgcnlem  25839  degltlem1  26125  plyco0  26245  dgreq0  26319  plydivex  26353  aannenlem1  26384  abelthlem1  26489  abelthlem3  26491  abelthlem8  26497  abelthlem9  26498  advlogexp  26711  cxpexp  26724  leibpi  26999  log2cnv  27001  log2tlbnd  27002  basellem2  27139  sgmnncl  27204  chpp1  27212  bcmono  27335  bcmax  27336  bcp1ctr  27337  lgsneg1  27380  lgsdirnn0  27402  lgsdinn0  27403  2lgslem1c  27451  2lgslem3a1  27458  2lgslem3b1  27459  2lgslem3c1  27460  2lgsoddprmlem2  27467  2sq2  27491  2sqreultlem  27505  dchrisumlem1  27547  qabvle  27683  ostth2lem2  27692  tgldimor  28524  upgrewlkle2  29638  wlkv0  29683  redwlk  29704  pthdadjvtx  29762  pthdlem1  29798  wwlknvtx  29874  wlkiswwlks2lem3  29900  wwlksm1edg  29910  wwlksnred  29921  wwlksnext  29922  clwlkclwwlklem2a1  30020  clwlkclwwlklem2a2  30021  clwlkclwwlklem2fv1  30023  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwlkclwwlk  30030  clwwisshclwwslem  30042  eucrctshift  30271  eucrct2eupth1  30272  eucrct2eupth  30273  numclwwlk5lem  30415  numclwwlk5  30416  numclwwlk7  30419  frgrreggt1  30421  nndiffz1  32794  xrge0mulgnn0  33002  hashf2  34064  signsvtn0  34563  nn0ltp1ne  35095  0nn0m1nnn0  35096  pthhashvtx  35111  fz0n  35710  bcneg1  35715  bccolsum  35718  faclimlem3  35724  faclim  35725  iprodfac  35726  poimirlem28  37634  mblfinlem1  37643  mblfinlem2  37644  lcmineqlem2  42011  sticksstones22  42149  gcdnn0id  42342  negexpidd  42669  nacsfix  42699  fzsplit1nn0  42741  eldioph2lem1  42747  fz1eqin  42756  diophin  42759  eq0rabdioph  42763  rexrabdioph  42781  rexzrexnn0  42791  irrapxlem4  42812  pell14qrss1234  42843  pell1qrss14  42855  monotoddzz  42931  rmxypos  42935  ltrmynn0  42936  ltrmxnn0  42937  lermxnn0  42938  rmxnn  42939  rmynn0  42945  jm2.17a  42948  jm2.17b  42949  rmygeid  42952  jm2.18  42976  jm2.19lem3  42979  jm2.19lem4  42980  jm2.22  42983  rmxdiophlem  43003  hbt  43118  proot1ex  43184  fzisoeu  45250  stirlinglem5  46033  elfzlble  47269  subsubelfzo0  47275  2ffzoeq  47276  addmodne  47283  fargshiftfo  47366  fmtnof1  47459  fmtnorec1  47461  goldbachthlem1  47469  odz2prm2pw  47487  flsqrt  47517  lighneallem4  47534  nn0eo  48377  nn0ofldiv2  48381  flnn0div2ge  48382  fllog2  48417  blenpw2  48427  blennngt2o2  48441  nn0digval  48449  dignn0fr  48450  digexp  48456  0dig2nn0e  48461  0dig2nn0o  48462  dig2bits  48463  dignn0flhalflem2  48465  dignn0ehalf  48466  dignn0flhalf  48467  nn0sumshdiglemB  48469