Theorem nn0z 12490

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℕ₀cn0 12378  ℤcz 12465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-1cn 11061  ax-icn 11062  ax-addcl 11063  ax-addrcl 11064  ax-mulcl 11065  ax-mulrcl 11066  ax-i2m1 11071  ax-1ne0 11072  ax-rnegex 11074  ax-rrecex 11075  ax-cnre 11076

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-neg 11344  df-nn 12123  df-n0 12379  df-z 12466

This theorem is referenced by:  nn0negz  12507  nn0ltp1le  12528  nn0leltp1  12529  nn0ltlem1  12530  nn0lt2  12533  nn0le2is012  12534  nn0lem1lt  12535  fnn0ind  12569  nn0pzuz  12800  nn0ge2m1nnALT  12837  fz1n  13439  ige2m1fz  13514  elfz2nn0  13515  fznn0  13516  elfz0add  13523  fzctr  13537  difelfzle  13538  fzoun  13593  fzofzim  13606  fzo1fzo0n0  13612  elincfzoext  13620  elfzodifsumelfzo  13628  fz0add1fz1  13632  zpnn0elfzo  13635  fzossfzop1  13640  ubmelm1fzo  13660  elfznelfzo  13670  flmulnn0  13728  quoremnn0  13757  zmodidfzoimp  13802  modmuladdnn0  13819  modfzo0difsn  13847  expdiv  14017  expnngt1  14145  faclbnd3  14196  bccmpl  14213  bcnp1n  14218  bcval5  14222  bcn2  14223  bcp1m1  14224  hashge2el2difr  14385  fi1uzind  14411  wrdred1  14464  wrdred1hash  14465  ccatalpha  14498  swrdnd0  14562  swrdfv2  14566  swrdsb0eq  14568  swrdsbslen  14569  swrdspsleq  14570  swrdlsw  14572  pfxnd  14592  pfxccatin12lem4  14630  pfxccatin12lem3  14636  pfxccat3  14638  swrdccat  14639  pfxccat3a  14642  revlen  14666  repswswrd  14688  repswccat  14690  cshwidxmodr  14708  cshf1  14714  2cshw  14717  cshweqrep  14725  cshwcshid  14731  cshwcsh2id  14732  cats1fv  14763  swrd2lsw  14856  2swrd2eqwrdeq  14857  isercoll  15572  iseraltlem2  15587  bcxmas  15739  geo2sum2  15778  geomulcvg  15780  risefacval2  15914  fallfacval2  15915  zrisefaccl  15924  zfallfaccl  15925  fallrisefac  15929  bpolylem  15952  fsumkthpow  15960  esum  15984  ege2le3  15994  eftlcl  16013  reeftlcl  16014  eftlub  16015  effsumlt  16017  eirrlem  16110  dvds1  16227  dvdsext  16229  addmodlteqALT  16233  oddnn02np1  16256  oddge22np1  16257  nn0ehalf  16286  nn0o1gt2  16289  nno  16290  nn0o  16291  nn0oddm1d2  16293  divalglem4  16304  divalglem5  16305  modremain  16316  bitsinv1  16350  nn0gcdid0  16429  nn0seqcvgd  16478  algcvga  16487  eucalgf  16491  nonsq  16667  numdenexp  16668  odzdvds  16704  coprimeprodsq  16717  coprimeprodsq2  16718  oddprm  16719  iserodd  16744  pcexp  16768  pcidlem  16781  pc11  16789  dvdsprmpweqle  16795  difsqpwdvds  16796  pcfac  16808  prmunb  16823  hashbc2  16915  cshwshashlem2  17005  chnccat  18529  smndex1ibas  18805  smndex1iidm  18806  smndex2dnrinv  18820  smndex2dlinvh  18822  mulgaddcom  19008  mulginvcom  19009  mulgz  19012  mulgdirlem  19015  mulgass  19021  mndodcongi  19453  oddvdsnn0  19454  odeq  19460  odmulg  19466  efgsdmi  19642  cyggex2  19807  fincygsubgodd  20024  mulgass2  20225  chrrhm  21466  zncrng  21479  znzrh2  21480  zndvds  21484  znchr  21497  znunit  21498  chfacfisf  22767  chfacfisfcpmat  22768  chfacfscmulfsupp  22772  chfacfpmmulfsupp  22776  clmmulg  25026  itgcnlem  25716  degltlem1  26002  plyco0  26122  dgreq0  26196  plydivex  26230  aannenlem1  26261  abelthlem1  26366  abelthlem3  26368  abelthlem8  26374  abelthlem9  26375  advlogexp  26589  cxpexp  26602  leibpi  26877  log2cnv  26879  log2tlbnd  26880  basellem2  27017  sgmnncl  27082  chpp1  27090  bcmono  27213  bcmax  27214  bcp1ctr  27215  lgsneg1  27258  lgsdirnn0  27280  lgsdinn0  27281  2lgslem1c  27329  2lgslem3a1  27336  2lgslem3b1  27337  2lgslem3c1  27338  2lgsoddprmlem2  27345  2sq2  27369  2sqreultlem  27383  dchrisumlem1  27425  qabvle  27561  ostth2lem2  27570  tgldimor  28478  upgrewlkle2  29583  wlkv0  29626  redwlk  29647  pthdadjvtx  29704  pthdlem1  29742  wwlknvtx  29821  wlkiswwlks2lem3  29847  wwlksm1edg  29857  wwlksnred  29868  wwlksnext  29869  clwlkclwwlklem2a1  29967  clwlkclwwlklem2a2  29968  clwlkclwwlklem2fv1  29970  clwlkclwwlklem2fv2  29971  clwlkclwwlklem2a4  29972  clwlkclwwlklem2a  29973  clwlkclwwlklem2  29975  clwlkclwwlk  29977  clwwisshclwwslem  29989  eucrctshift  30218  eucrct2eupth1  30219  eucrct2eupth  30220  numclwwlk5lem  30362  numclwwlk5  30363  numclwwlk7  30366  frgrreggt1  30368  nndiffz1  32764  xrge0mulgnn0  32991  hashf2  34092  signsvtn0  34578  nn0ltp1ne  35144  0nn0m1nnn0  35145  pthhashvtx  35160  fz0n  35763  bcneg1  35768  bccolsum  35771  faclimlem3  35777  faclim  35778  iprodfac  35779  poimirlem28  37687  mblfinlem1  37696  mblfinlem2  37697  lcmineqlem2  42062  sticksstones22  42200  gcdnn0id  42361  negexpidd  42714  nacsfix  42744  fzsplit1nn0  42786  eldioph2lem1  42792  fz1eqin  42801  diophin  42804  eq0rabdioph  42808  rexrabdioph  42826  rexzrexnn0  42836  irrapxlem4  42857  pell14qrss1234  42888  pell1qrss14  42900  monotoddzz  42975  rmxypos  42979  ltrmynn0  42980  ltrmxnn0  42981  lermxnn0  42982  rmxnn  42983  rmynn0  42989  jm2.17a  42992  jm2.17b  42993  rmygeid  42996  jm2.18  43020  jm2.19lem3  43023  jm2.19lem4  43024  jm2.22  43027  rmxdiophlem  43047  hbt  43162  proot1ex  43228  fzisoeu  45340  stirlinglem5  46115  elfzlble  47350  subsubelfzo0  47356  2ffzoeq  47357  addmodne  47374  fargshiftfo  47472  fmtnof1  47565  fmtnorec1  47567  goldbachthlem1  47575  odz2prm2pw  47593  flsqrt  47623  lighneallem4  47640  nn0eo  48559  nn0ofldiv2  48563  flnn0div2ge  48564  fllog2  48599  blenpw2  48609  blennngt2o2  48623  nn0digval  48631  dignn0fr  48632  digexp  48638  0dig2nn0e  48643  0dig2nn0o  48644  dig2bits  48645  dignn0flhalflem2  48647  dignn0ehalf  48648  dignn0flhalf  48649  nn0sumshdiglemB  48651