Theorem nn0z 12744

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℕ₀cn0 12633  ℤcz 12720

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-i2m1 11295  ax-1ne0 11296  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-neg 11571  df-nn 12363  df-n0 12634  df-z 12721

This theorem is used by:  nn0negz  12761  0nn0m1nnn0  12780  nn0ltp1le  12784  nn0leltp1  12785  nn0ltlem1  12786  nn0lt2  12789  nn0le2is012  12790  nn0lem1lt  12791  fnn0ind  12825  nn0pzuz  13059  nn0ge2m1nnALT  13096  fz1n  13702  ige2m1fz  13778  elfz2nn0  13779  fznn0  13780  elfz0add  13787  fzctr  13801  difelfzle  13802  fzoun  13858  fzofzim  13871  fzo1fzo0n0  13877  elincfzoext  13885  elfzodifsumelfzo  13893  fz0add1fz1  13897  zpnn0elfzo  13900  fzossfzop1  13905  ubmelm1fzo  13925  elfznelfzo  13935  flmulnn0  13994  quoremnn0  14023  zmodidfzoimp  14068  modmuladdnn0  14085  modfzo0difsn  14113  expdiv  14283  expnngt1  14412  faclbnd3  14463  bccmpl  14480  bcnp1n  14485  bcval5  14489  bcn2  14490  bcp1m1  14491  hashge2el2difr  14653  fi1uzind  14679  wrdred1  14732  wrdred1hash  14733  ccatalpha  14767  swrdnd0  14835  swrdfv2  14839  swrdsb0eq  14841  swrdsbslen  14842  swrdspsleq  14843  swrdlsw  14845  pfxnd  14865  pfxccatin12lem4  14903  pfxccatin12lem3  14909  pfxccat3  14911  swrdccat  14912  pfxccat3a  14915  revlen  14939  repswswrd  14963  repswccat  14965  cshwidxmodr  14983  cshf1  14989  2cshw  14992  cshweqrep  15000  cshwcshid  15006  cshwcsh2id  15007  cats1fv  15038  swrd2lsw  15134  2swrd2eqwrdeq  15135  isercoll  15864  iseraltlem2  15879  bcxmas  16033  geo2sum2  16072  geomulcvg  16074  risefacval2  16206  fallfacval2  16207  zrisefaccl  16216  zfallfaccl  16217  fallrisefac  16221  bpolylem  16243  fsumkthpow  16251  esum  16275  ege2le3  16285  eftlcl  16304  reeftlcl  16305  eftlub  16306  effsumlt  16308  eirrlem  16401  dvds1  16518  dvdsext  16520  addmodlteqALT  16524  oddnn02np1  16547  oddge22np1  16548  nn0ehalf  16577  nn0o1gt2  16580  nno  16581  nn0o  16582  nn0oddm1d2  16584  divalglem4  16595  divalglem5  16596  modremain  16607  bitsinv1  16641  nn0gcdid0  16722  gcdnn0id  16729  nn0seqcvgd  16774  algcvga  16783  eucalgf  16787  nonsq  16964  numdenexp  16966  odzdvds  17002  coprimeprodsq  17015  coprimeprodsq2  17016  oddprm  17017  iserodd  17042  pcexp  17066  pcidlem  17079  pc11  17087  dvdsprmpweqle  17093  difsqpwdvds  17094  pcfac  17106  prmunb  17121  hashbc2  17213  cshwshashlem2  17303  chnccat  18829  smndex1ibas  19125  smndex1iidm  19126  smndex2dnrinv  19143  smndex2dlinvh  19145  mulgaddcom  19337  mulginvcom  19338  mulgz  19341  mulgdirlem  19344  mulgass  19350  mndodcongi  19787  oddvdsnn0  19788  odeq  19794  odmulg  19800  efgsdmi  19976  cyggex2  20141  fincygsubgodd  20358  mulgass2  20570  chrrhm  21867  zncrng  21880  znzrh2  21881  zndvds  21885  znchr  21898  znunit  21899  chfacfisf  23202  chfacfisfcpmat  23203  chfacfscmulfsupp  23207  chfacfpmmulfsupp  23211  clmmulg  25452  itgcnlem  26140  degltlem1  26420  plyco0  26540  dgreq0  26614  plydivex  26648  aannenlem1  26685  abelthlem1  26788  abelthlem3  26790  abelthlem8  26796  abelthlem9  26797  advlogexp  27013  cxpexp  27026  leibpi  27300  log2cnv  27302  log2tlbnd  27303  basellem2  27439  sgmnncl  27504  chpp1  27512  bcmono  27634  bcmax  27635  bcp1ctr  27636  lgsneg1  27679  lgsdirnn0  27701  lgsdinn0  27702  2lgslem1c  27750  2lgslem3a1  27757  2lgslem3b1  27758  2lgslem3c1  27759  2lgsoddprmlem2  27766  2sq2  27790  2sqreultlem  27804  dchrisumlem1  27846  qabvle  27982  ostth2lem2  27991  fltoprmlem2  28024  tgldimor  28995  upgrewlkle2  30217  wlkv0  30260  redwlk  30281  pthdadjvtx  30343  pthhashvtx  30345  pthdlem1  30382  wwlknvtx  30464  wlkiswwlks2lem3  30490  wwlksm1edg  30500  wwlksnred  30511  wwlksnext  30512  clwlkclwwlklem2a1  30613  clwlkclwwlklem2a2  30614  clwlkclwwlklem2fv1  30616  clwlkclwwlklem2fv2  30617  clwlkclwwlklem2a4  30618  clwlkclwwlklem2a  30619  clwlkclwwlklem2  30621  clwlkclwwlk  30623  clwwisshclwwslem  30635  eucrctshift  30874  eucrct2eupth1  30875  eucrct2eupth  30876  numclwwlk5lem  31018  numclwwlk5  31019  numclwwlk7  31022  frgrreggt1  31024  nndiffz1  33448  nn0diffz0  33456  xrge0mulgnn0  33646  hashf2  34786  signsvtn0  35269  nn0ltp1ne  36059  fz0n  36674  bcneg1  36679  bccolsum  36682  faclimlem3  36688  faclim  36689  iprodfac  36690  poimirlem28  38758  mblfinlem1  38767  mblfinlem2  38768  lcmineqlem2  43272  sticksstones22  43410  negexpidd  43885  nacsfix  43916  fzsplit1nn0  43958  eldioph2lem1  43964  fz1eqin  43973  diophin  43976  eq0rabdioph  43980  rexrabdioph  43994  rexzrexnn0  44004  irrapxlem4  44025  pell14qrss1234  44056  pell1qrss14  44068  monotoddzz  44143  rmxypos  44147  ltrmynn0  44148  ltrmxnn0  44149  lermxnn0  44150  rmxnn  44151  rmynn0  44157  jm2.17a  44160  jm2.17b  44161  rmygeid  44164  jm2.18  44188  jm2.19lem3  44191  jm2.19lem4  44192  jm2.22  44195  rmxdiophlem  44215  hbt  44324  proot1ex  44390  k0004ss3  45345  fzisoeu  46521  stirlinglem5  47293  elfzlble  48595  subsubelfzo0  48602  2ffzoeq  48603  addmodne  48625  fargshiftfo  48729  fmtnof1  48825  fmtnorec1  48827  goldbachthlem1  48835  odz2prm2pw  48853  flsqrt  48883  lighneallem4  48900  nn0eo  49845  nn0ofldiv2  49849  flnn0div2ge  49850  fllog2  49885  blenpw2  49895  blennngt2o2  49909  nn0digval  49917  dignn0fr  49918  digexp  49924  0dig2nn0e  49929  0dig2nn0o  49930  dig2bits  49931  dignn0flhalflem2  49933  dignn0ehalf  49934  dignn0flhalf  49935  nn0sumshdiglemB  49937