Theorem nn0z 12524

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕ₀cn0 12413  ℤcz 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-neg 11379  df-nn 12158  df-n0 12414  df-z 12501

This theorem is referenced by:  nn0negz  12541  nn0ltp1le  12562  nn0leltp1  12563  nn0ltlem1  12564  nn0lt2  12567  nn0le2is012  12568  nn0lem1lt  12569  fnn0ind  12603  nn0pzuz  12830  nn0ge2m1nnALT  12867  fz1n  13470  ige2m1fz  13545  elfz2nn0  13546  fznn0  13547  elfz0add  13554  fzctr  13568  difelfzle  13569  fzoun  13624  fzofzim  13637  fzo1fzo0n0  13643  elincfzoext  13651  elfzodifsumelfzo  13659  fz0add1fz1  13663  zpnn0elfzo  13666  fzossfzop1  13671  ubmelm1fzo  13691  elfznelfzo  13701  flmulnn0  13759  quoremnn0  13788  zmodidfzoimp  13833  modmuladdnn0  13850  modfzo0difsn  13878  expdiv  14048  expnngt1  14176  faclbnd3  14227  bccmpl  14244  bcnp1n  14249  bcval5  14253  bcn2  14254  bcp1m1  14255  hashge2el2difr  14416  fi1uzind  14442  wrdred1  14495  wrdred1hash  14496  ccatalpha  14529  swrdnd0  14593  swrdfv2  14597  swrdsb0eq  14599  swrdsbslen  14600  swrdspsleq  14601  swrdlsw  14603  pfxnd  14623  pfxccatin12lem4  14661  pfxccatin12lem3  14667  pfxccat3  14669  swrdccat  14670  pfxccat3a  14673  revlen  14697  repswswrd  14719  repswccat  14721  cshwidxmodr  14739  cshf1  14745  2cshw  14748  cshweqrep  14756  cshwcshid  14762  cshwcsh2id  14763  cats1fv  14794  swrd2lsw  14887  2swrd2eqwrdeq  14888  isercoll  15603  iseraltlem2  15618  bcxmas  15770  geo2sum2  15809  geomulcvg  15811  risefacval2  15945  fallfacval2  15946  zrisefaccl  15955  zfallfaccl  15956  fallrisefac  15960  bpolylem  15983  fsumkthpow  15991  esum  16015  ege2le3  16025  eftlcl  16044  reeftlcl  16045  eftlub  16046  effsumlt  16048  eirrlem  16141  dvds1  16258  dvdsext  16260  addmodlteqALT  16264  oddnn02np1  16287  oddge22np1  16288  nn0ehalf  16317  nn0o1gt2  16320  nno  16321  nn0o  16322  nn0oddm1d2  16324  divalglem4  16335  divalglem5  16336  modremain  16347  bitsinv1  16381  nn0gcdid0  16460  nn0seqcvgd  16509  algcvga  16518  eucalgf  16522  nonsq  16698  numdenexp  16699  odzdvds  16735  coprimeprodsq  16748  coprimeprodsq2  16749  oddprm  16750  iserodd  16775  pcexp  16799  pcidlem  16812  pc11  16820  dvdsprmpweqle  16826  difsqpwdvds  16827  pcfac  16839  prmunb  16854  hashbc2  16946  cshwshashlem2  17036  chnccat  18561  smndex1ibas  18837  smndex1iidm  18838  smndex2dnrinv  18852  smndex2dlinvh  18854  mulgaddcom  19040  mulginvcom  19041  mulgz  19044  mulgdirlem  19047  mulgass  19053  mndodcongi  19484  oddvdsnn0  19485  odeq  19491  odmulg  19497  efgsdmi  19673  cyggex2  19838  fincygsubgodd  20055  mulgass2  20256  chrrhm  21498  zncrng  21511  znzrh2  21512  zndvds  21516  znchr  21529  znunit  21530  chfacfisf  22810  chfacfisfcpmat  22811  chfacfscmulfsupp  22815  chfacfpmmulfsupp  22819  clmmulg  25069  itgcnlem  25759  degltlem1  26045  plyco0  26165  dgreq0  26239  plydivex  26273  aannenlem1  26304  abelthlem1  26409  abelthlem3  26411  abelthlem8  26417  abelthlem9  26418  advlogexp  26632  cxpexp  26645  leibpi  26920  log2cnv  26922  log2tlbnd  26923  basellem2  27060  sgmnncl  27125  chpp1  27133  bcmono  27256  bcmax  27257  bcp1ctr  27258  lgsneg1  27301  lgsdirnn0  27323  lgsdinn0  27324  2lgslem1c  27372  2lgslem3a1  27379  2lgslem3b1  27380  2lgslem3c1  27381  2lgsoddprmlem2  27388  2sq2  27412  2sqreultlem  27426  dchrisumlem1  27468  qabvle  27604  ostth2lem2  27613  tgldimor  28586  upgrewlkle2  29692  wlkv0  29735  redwlk  29756  pthdadjvtx  29813  pthdlem1  29851  wwlknvtx  29930  wlkiswwlks2lem3  29956  wwlksm1edg  29966  wwlksnred  29977  wwlksnext  29978  clwlkclwwlklem2a1  30079  clwlkclwwlklem2a2  30080  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwlkclwwlk  30089  clwwisshclwwslem  30101  eucrctshift  30330  eucrct2eupth1  30331  eucrct2eupth  30332  numclwwlk5lem  30474  numclwwlk5  30475  numclwwlk7  30478  frgrreggt1  30480  nndiffz1  32876  nn0diffz0  32884  xrge0mulgnn0  33107  hashf2  34261  signsvtn0  34747  nn0ltp1ne  35325  0nn0m1nnn0  35326  pthhashvtx  35341  fz0n  35944  bcneg1  35949  bccolsum  35952  faclimlem3  35958  faclim  35959  iprodfac  35960  poimirlem28  37893  mblfinlem1  37902  mblfinlem2  37903  lcmineqlem2  42394  sticksstones22  42532  gcdnn0id  42693  negexpidd  43033  nacsfix  43063  fzsplit1nn0  43105  eldioph2lem1  43111  fz1eqin  43120  diophin  43123  eq0rabdioph  43127  rexrabdioph  43145  rexzrexnn0  43155  irrapxlem4  43176  pell14qrss1234  43207  pell1qrss14  43219  monotoddzz  43294  rmxypos  43298  ltrmynn0  43299  ltrmxnn0  43300  lermxnn0  43301  rmxnn  43302  rmynn0  43308  jm2.17a  43311  jm2.17b  43312  rmygeid  43315  jm2.18  43339  jm2.19lem3  43342  jm2.19lem4  43343  jm2.22  43346  rmxdiophlem  43366  hbt  43481  proot1ex  43547  fzisoeu  45656  stirlinglem5  46430  elfzlble  47674  subsubelfzo0  47680  2ffzoeq  47681  addmodne  47698  fargshiftfo  47796  fmtnof1  47889  fmtnorec1  47891  goldbachthlem1  47899  odz2prm2pw  47917  flsqrt  47947  lighneallem4  47964  nn0eo  48882  nn0ofldiv2  48886  flnn0div2ge  48887  fllog2  48922  blenpw2  48932  blennngt2o2  48946  nn0digval  48954  dignn0fr  48955  digexp  48961  0dig2nn0e  48966  0dig2nn0o  48967  dig2bits  48968  dignn0flhalflem2  48970  dignn0ehalf  48971  dignn0flhalf  48972  nn0sumshdiglemB  48974