Theorem nn0z 12718

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℕ₀cn0 12607  ℤcz 12694

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7752  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-addrcl 11262  ax-mulcl 11263  ax-mulrcl 11264  ax-i2m1 11269  ax-1ne0 11270  ax-rnegex 11272  ax-rrecex 11273  ax-cnre 11274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3900  df-un 3902  df-in 3904  df-ss 3915  df-pss 4035  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6305  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8300  df-wrecs 8331  df-recs 8380  df-rdg 8419  df-neg 11545  df-nn 12337  df-n0 12608  df-z 12695

This theorem is used by:  nn0negz  12735  0nn0m1nnn0  12754  nn0ltp1le  12758  nn0leltp1  12759  nn0ltlem1  12760  nn0lt2  12763  nn0le2is012  12764  nn0lem1lt  12765  fnn0ind  12799  nn0pzuz  13033  nn0ge2m1nnALT  13070  fz1n  13676  ige2m1fz  13752  elfz2nn0  13753  fznn0  13754  elfz0add  13761  fzctr  13775  difelfzle  13776  fzoun  13832  fzofzim  13845  fzo1fzo0n0  13851  elincfzoext  13859  elfzodifsumelfzo  13867  fz0add1fz1  13871  zpnn0elfzo  13874  fzossfzop1  13879  ubmelm1fzo  13899  elfznelfzo  13909  flmulnn0  13968  quoremnn0  13997  zmodidfzoimp  14042  modmuladdnn0  14059  modfzo0difsn  14087  expdiv  14257  expnngt1  14386  faclbnd3  14437  bccmpl  14454  bcnp1n  14459  bcval5  14463  bcn2  14464  bcp1m1  14465  hashge2el2difr  14627  fi1uzind  14653  wrdred1  14706  wrdred1hash  14707  ccatalpha  14741  swrdnd0  14808  swrdfv2  14812  swrdsb0eq  14814  swrdsbslen  14815  swrdspsleq  14816  swrdlsw  14818  pfxnd  14838  pfxccatin12lem4  14876  pfxccatin12lem3  14882  pfxccat3  14884  swrdccat  14885  pfxccat3a  14888  revlen  14912  repswswrd  14936  repswccat  14938  cshwidxmodr  14956  cshf1  14962  2cshw  14965  cshweqrep  14973  cshwcshid  14979  cshwcsh2id  14980  cats1fv  15011  swrd2lsw  15106  2swrd2eqwrdeq  15107  isercoll  15836  iseraltlem2  15851  bcxmas  16005  geo2sum2  16044  geomulcvg  16046  risefacval2  16178  fallfacval2  16179  zrisefaccl  16188  zfallfaccl  16189  fallrisefac  16193  bpolylem  16215  fsumkthpow  16223  esum  16247  ege2le3  16257  eftlcl  16276  reeftlcl  16277  eftlub  16278  effsumlt  16280  eirrlem  16373  dvds1  16490  dvdsext  16492  addmodlteqALT  16496  oddnn02np1  16519  oddge22np1  16520  nn0ehalf  16549  nn0o1gt2  16552  nno  16553  nn0o  16554  nn0oddm1d2  16556  divalglem4  16567  divalglem5  16568  modremain  16579  bitsinv1  16613  nn0gcdid0  16694  gcdnn0id  16701  nn0seqcvgd  16746  algcvga  16755  eucalgf  16759  nonsq  16936  numdenexp  16938  odzdvds  16974  coprimeprodsq  16987  coprimeprodsq2  16988  oddprm  16989  iserodd  17014  pcexp  17038  pcidlem  17051  pc11  17059  dvdsprmpweqle  17065  difsqpwdvds  17066  pcfac  17078  prmunb  17093  hashbc2  17185  cshwshashlem2  17275  chnccat  18801  smndex1ibas  19097  smndex1iidm  19098  smndex2dnrinv  19115  smndex2dlinvh  19117  mulgaddcom  19309  mulginvcom  19310  mulgz  19313  mulgdirlem  19316  mulgass  19322  mndodcongi  19758  oddvdsnn0  19759  odeq  19765  odmulg  19771  efgsdmi  19947  cyggex2  20112  fincygsubgodd  20329  mulgass2  20541  chrrhm  21838  zncrng  21851  znzrh2  21852  zndvds  21856  znchr  21869  znunit  21870  chfacfisf  23173  chfacfisfcpmat  23174  chfacfscmulfsupp  23178  chfacfpmmulfsupp  23182  clmmulg  25423  itgcnlem  26111  degltlem1  26391  plyco0  26511  dgreq0  26585  plydivex  26619  aannenlem1  26656  abelthlem1  26759  abelthlem3  26761  abelthlem8  26767  abelthlem9  26768  advlogexp  26984  cxpexp  26997  leibpi  27271  log2cnv  27273  log2tlbnd  27274  basellem2  27410  sgmnncl  27475  chpp1  27483  bcmono  27605  bcmax  27606  bcp1ctr  27607  lgsneg1  27650  lgsdirnn0  27672  lgsdinn0  27673  2lgslem1c  27721  2lgslem3a1  27728  2lgslem3b1  27729  2lgslem3c1  27730  2lgsoddprmlem2  27737  2sq2  27761  2sqreultlem  27775  dchrisumlem1  27817  qabvle  27953  ostth2lem2  27962  fltoprmlem2  27995  tgldimor  28966  upgrewlkle2  30188  wlkv0  30231  redwlk  30252  pthdadjvtx  30314  pthhashvtx  30316  pthdlem1  30353  wwlknvtx  30435  wlkiswwlks2lem3  30461  wwlksm1edg  30471  wwlksnred  30482  wwlksnext  30483  clwlkclwwlklem2a1  30584  clwlkclwwlklem2a2  30585  clwlkclwwlklem2fv1  30587  clwlkclwwlklem2fv2  30588  clwlkclwwlklem2a4  30589  clwlkclwwlklem2a  30590  clwlkclwwlklem2  30592  clwlkclwwlk  30594  clwwisshclwwslem  30606  eucrctshift  30845  eucrct2eupth1  30846  eucrct2eupth  30847  numclwwlk5lem  30989  numclwwlk5  30990  numclwwlk7  30993  frgrreggt1  30995  nndiffz1  33379  nn0diffz0  33387  xrge0mulgnn0  33577  hashf2  34717  signsvtn0  35200  nn0ltp1ne  35903  fz0n  36497  bcneg1  36502  bccolsum  36505  faclimlem3  36511  faclim  36512  iprodfac  36513  poimirlem28  38568  mblfinlem1  38577  mblfinlem2  38578  lcmineqlem2  43082  sticksstones22  43220  negexpidd  43694  nacsfix  43724  fzsplit1nn0  43766  eldioph2lem1  43772  fz1eqin  43781  diophin  43784  eq0rabdioph  43788  rexrabdioph  43802  rexzrexnn0  43812  irrapxlem4  43833  pell14qrss1234  43864  pell1qrss14  43876  monotoddzz  43951  rmxypos  43955  ltrmynn0  43956  ltrmxnn0  43957  lermxnn0  43958  rmxnn  43959  rmynn0  43965  jm2.17a  43968  jm2.17b  43969  rmygeid  43972  jm2.18  43996  jm2.19lem3  43999  jm2.19lem4  44000  jm2.22  44003  rmxdiophlem  44023  hbt  44133  proot1ex  44199  fzisoeu  46317  stirlinglem5  47089  elfzlble  48391  subsubelfzo0  48398  2ffzoeq  48399  addmodne  48421  fargshiftfo  48525  fmtnof1  48621  fmtnorec1  48623  goldbachthlem1  48631  odz2prm2pw  48649  flsqrt  48679  lighneallem4  48696  nn0eo  49641  nn0ofldiv2  49645  flnn0div2ge  49646  fllog2  49681  blenpw2  49691  blennngt2o2  49705  nn0digval  49713  dignn0fr  49714  digexp  49720  0dig2nn0e  49725  0dig2nn0o  49726  dig2bits  49727  dignn0flhalflem2  49729  dignn0ehalf  49730  dignn0flhalf  49731  nn0sumshdiglemB  49733