Theorem nn0z 12514

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕ₀cn0 12402  ℤcz 12489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-neg 11368  df-nn 12147  df-n0 12403  df-z 12490

This theorem is referenced by:  nn0negz  12531  nn0ltp1le  12552  nn0leltp1  12553  nn0ltlem1  12554  nn0lt2  12557  nn0le2is012  12558  nn0lem1lt  12559  fnn0ind  12593  nn0pzuz  12824  nn0ge2m1nnALT  12861  fz1n  13463  ige2m1fz  13538  elfz2nn0  13539  fznn0  13540  elfz0add  13547  fzctr  13561  difelfzle  13562  fzoun  13617  fzofzim  13630  fzo1fzo0n0  13636  elincfzoext  13644  elfzodifsumelfzo  13652  fz0add1fz1  13656  zpnn0elfzo  13659  fzossfzop1  13664  ubmelm1fzo  13684  elfznelfzo  13693  flmulnn0  13749  quoremnn0  13778  zmodidfzoimp  13823  modmuladdnn0  13840  modfzo0difsn  13868  expdiv  14038  expnngt1  14166  faclbnd3  14217  bccmpl  14234  bcnp1n  14239  bcval5  14243  bcn2  14244  bcp1m1  14245  hashge2el2difr  14406  fi1uzind  14432  wrdred1  14485  wrdred1hash  14486  ccatalpha  14518  swrdnd0  14582  swrdfv2  14586  swrdsb0eq  14588  swrdsbslen  14589  swrdspsleq  14590  swrdlsw  14592  pfxnd  14612  pfxccatin12lem4  14650  pfxccatin12lem3  14656  pfxccat3  14658  swrdccat  14659  pfxccat3a  14662  revlen  14686  repswswrd  14708  repswccat  14710  cshwidxmodr  14728  cshf1  14734  2cshw  14737  cshweqrep  14745  cshwcshid  14752  cshwcsh2id  14753  cats1fv  14784  swrd2lsw  14877  2swrd2eqwrdeq  14878  isercoll  15593  iseraltlem2  15608  bcxmas  15760  geo2sum2  15799  geomulcvg  15801  risefacval2  15935  fallfacval2  15936  zrisefaccl  15945  zfallfaccl  15946  fallrisefac  15950  bpolylem  15973  fsumkthpow  15981  esum  16005  ege2le3  16015  eftlcl  16034  reeftlcl  16035  eftlub  16036  effsumlt  16038  eirrlem  16131  dvds1  16248  dvdsext  16250  addmodlteqALT  16254  oddnn02np1  16277  oddge22np1  16278  nn0ehalf  16307  nn0o1gt2  16310  nno  16311  nn0o  16312  nn0oddm1d2  16314  divalglem4  16325  divalglem5  16326  modremain  16337  bitsinv1  16371  nn0gcdid0  16450  nn0seqcvgd  16499  algcvga  16508  eucalgf  16512  nonsq  16688  numdenexp  16689  odzdvds  16725  coprimeprodsq  16738  coprimeprodsq2  16739  oddprm  16740  iserodd  16765  pcexp  16789  pcidlem  16802  pc11  16810  dvdsprmpweqle  16816  difsqpwdvds  16817  pcfac  16829  prmunb  16844  hashbc2  16936  cshwshashlem2  17026  smndex1ibas  18792  smndex1iidm  18793  smndex2dnrinv  18807  smndex2dlinvh  18809  mulgaddcom  18995  mulginvcom  18996  mulgz  18999  mulgdirlem  19002  mulgass  19008  mndodcongi  19440  oddvdsnn0  19441  odeq  19447  odmulg  19453  efgsdmi  19629  cyggex2  19794  fincygsubgodd  20011  mulgass2  20212  chrrhm  21456  zncrng  21469  znzrh2  21470  zndvds  21474  znchr  21487  znunit  21488  chfacfisf  22757  chfacfisfcpmat  22758  chfacfscmulfsupp  22762  chfacfpmmulfsupp  22766  clmmulg  25017  itgcnlem  25707  degltlem1  25993  plyco0  26113  dgreq0  26187  plydivex  26221  aannenlem1  26252  abelthlem1  26357  abelthlem3  26359  abelthlem8  26365  abelthlem9  26366  advlogexp  26580  cxpexp  26593  leibpi  26868  log2cnv  26870  log2tlbnd  26871  basellem2  27008  sgmnncl  27073  chpp1  27081  bcmono  27204  bcmax  27205  bcp1ctr  27206  lgsneg1  27249  lgsdirnn0  27271  lgsdinn0  27272  2lgslem1c  27320  2lgslem3a1  27327  2lgslem3b1  27328  2lgslem3c1  27329  2lgsoddprmlem2  27336  2sq2  27360  2sqreultlem  27374  dchrisumlem1  27416  qabvle  27552  ostth2lem2  27561  tgldimor  28465  upgrewlkle2  29570  wlkv0  29613  redwlk  29634  pthdadjvtx  29691  pthdlem1  29729  wwlknvtx  29808  wlkiswwlks2lem3  29834  wwlksm1edg  29844  wwlksnred  29855  wwlksnext  29856  clwlkclwwlklem2a1  29954  clwlkclwwlklem2a2  29955  clwlkclwwlklem2fv1  29957  clwlkclwwlklem2fv2  29958  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  clwlkclwwlklem2  29962  clwlkclwwlk  29964  clwwisshclwwslem  29976  eucrctshift  30205  eucrct2eupth1  30206  eucrct2eupth  30207  numclwwlk5lem  30349  numclwwlk5  30350  numclwwlk7  30353  frgrreggt1  30355  nndiffz1  32742  xrge0mulgnn0  32982  hashf2  34050  signsvtn0  34537  nn0ltp1ne  35084  0nn0m1nnn0  35085  pthhashvtx  35100  fz0n  35703  bcneg1  35708  bccolsum  35711  faclimlem3  35717  faclim  35718  iprodfac  35719  poimirlem28  37627  mblfinlem1  37636  mblfinlem2  37637  lcmineqlem2  42003  sticksstones22  42141  gcdnn0id  42302  negexpidd  42655  nacsfix  42685  fzsplit1nn0  42727  eldioph2lem1  42733  fz1eqin  42742  diophin  42745  eq0rabdioph  42749  rexrabdioph  42767  rexzrexnn0  42777  irrapxlem4  42798  pell14qrss1234  42829  pell1qrss14  42841  monotoddzz  42916  rmxypos  42920  ltrmynn0  42921  ltrmxnn0  42922  lermxnn0  42923  rmxnn  42924  rmynn0  42930  jm2.17a  42933  jm2.17b  42934  rmygeid  42937  jm2.18  42961  jm2.19lem3  42964  jm2.19lem4  42965  jm2.22  42968  rmxdiophlem  42988  hbt  43103  proot1ex  43169  fzisoeu  45282  stirlinglem5  46060  elfzlble  47305  subsubelfzo0  47311  2ffzoeq  47312  addmodne  47329  fargshiftfo  47427  fmtnof1  47520  fmtnorec1  47522  goldbachthlem1  47530  odz2prm2pw  47548  flsqrt  47578  lighneallem4  47595  nn0eo  48514  nn0ofldiv2  48518  flnn0div2ge  48519  fllog2  48554  blenpw2  48564  blennngt2o2  48578  nn0digval  48586  dignn0fr  48587  digexp  48593  0dig2nn0e  48598  0dig2nn0o  48599  dig2bits  48600  dignn0flhalflem2  48602  dignn0ehalf  48603  dignn0flhalf  48604  nn0sumshdiglemB  48606