Theorem nn0z 11686

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

Syntax hints:   → wi 4   ∈ wcel 2157  ℕ₀cn0 11579  ℤcz 11663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307  ax-pre-mulgt0 10308

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-om 7306  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-er 7989  df-en 8203  df-dom 8204  df-sdom 8205  df-pnf 10371  df-mnf 10372  df-xr 10373  df-ltxr 10374  df-le 10375  df-sub 10563  df-neg 10564  df-nn 11316  df-n0 11580  df-z 11664

This theorem is referenced by:  nn0negz  11701  nn0ltp1le  11721  nn0leltp1  11722  nn0ltlem1  11723  nn0lt2  11726  nn0le2is012  11727  nn0lem1lt  11728  fnn0ind  11762  nn0pzuz  11983  nn0ge2m1nnALT  12021  fz1n  12602  ige2m1fz  12673  elfz2nn0  12674  fznn0  12675  elfz0add  12682  fzctr  12695  difelfzle  12696  fzoun  12749  fzofzim  12759  fzo1fzo0n0  12763  elincfzoext  12770  elfzodifsumelfzo  12778  fz0add1fz1  12782  zpnn0elfzo  12785  fzossfzop1  12790  ubmelm1fzo  12808  elfznelfzo  12817  flmulnn0  12872  quoremnn0  12899  zmodidfzoimp  12944  modmuladdnn0  12958  modfzo0difsn  12986  expdiv  13154  faclbnd3  13319  bccmpl  13336  bcnp1n  13341  bcval5  13345  bcn2  13346  bcp1m1  13347  hashge2el2difr  13500  fi1uzind  13516  wrdred1  13581  wrdred1hash  13582  ccatalpha  13610  swrdfv2  13690  swrdsb0eq  13691  swrdsbslen  13692  swrdspsleq  13693  swrdlsw  13696  2swrd1eqwrdeq  13698  swrdccatin12lem1  13728  swrdccatin12lem3  13734  swrdccat3  13736  swrdccat  13737  revlen  13755  repswswrd  13775  repswccat  13776  cshwidxmodr  13794  cshf1  13800  2cshw  13803  cshweqrep  13811  cshwcshid  13817  cshwcsh2id  13818  cats1fv  13848  swrd2lsw  13940  2swrd2eqwrdeq  13941  isercoll  14641  iseraltlem2  14656  bcxmas  14809  geo2sum2  14847  geomulcvg  14849  risefacval2  14981  fallfacval2  14982  zrisefaccl  14991  zfallfaccl  14992  fallrisefac  14996  bpolylem  15019  fsumkthpow  15027  esum  15051  ege2le3  15060  eftlcl  15077  reeftlcl  15078  eftlub  15079  effsumlt  15081  eirrlem  15172  dvds1  15284  dvdsext  15286  addmodlteqALT  15290  oddnn02np1  15312  oddge22np1  15313  nn0ehalf  15335  nn0o1gt2  15337  nno  15338  nn0o  15339  nn0oddm1d2  15341  divalglem4  15359  divalglem5  15360  modremain  15371  bitsinv1  15403  nn0gcdid0  15481  nn0seqcvgd  15522  algcvga  15531  eucalgf  15535  nonsq  15704  odzdvds  15737  coprimeprodsq  15750  coprimeprodsq2  15751  oddprm  15752  iserodd  15777  pcexp  15801  pcidlem  15813  pc11  15821  dvdsprmpweqle  15827  difsqpwdvds  15828  pcfac  15840  prmunb  15855  hashbc2  15947  cshwshashlem2  16035  mulgaddcom  17788  mulginvcom  17789  mulgz  17792  mulgdirlem  17795  mulgass  17801  mndodcongi  18183  oddvdsnn0  18184  odeq  18190  odmulg  18194  efgsdmi  18366  cyggex2  18519  mulgass2  18823  chrrhm  20107  zncrng  20120  znzrh2  20121  zndvds  20125  znchr  20138  znunit  20139  chfacfisf  20893  chfacfisfcpmat  20894  chfacfscmulfsupp  20898  chfacfpmmulfsupp  20902  clmmulg  23134  itgcnlem  23793  degltlem1  24069  plyco0  24185  dgreq0  24258  plydivex  24289  aannenlem1  24320  abelthlem1  24422  abelthlem3  24424  abelthlem8  24430  abelthlem9  24431  advlogexp  24638  cxpexp  24651  leibpilem1  24904  leibpi  24906  log2cnv  24908  log2tlbnd  24909  basellem2  25045  sgmnncl  25110  chpp1  25118  bcmono  25239  bcmax  25240  bcp1ctr  25241  lgsneg1  25284  lgsdirnn0  25306  lgsdinn0  25307  2lgslem1c  25355  2lgslem3a1  25362  2lgslem3b1  25363  2lgslem3c1  25364  2lgsoddprmlem2  25371  dchrisumlem1  25415  qabvle  25551  ostth2lem2  25560  tgldimor  25634  upgrewlkle2  26753  wlkv0  26798  redwlk  26820  pthdadjvtx  26877  pthdlem1  26913  wwlknvtx  26989  wlkiswwlks2lem3  27021  wwlksm1edg  27031  wwlksnred  27052  wwlksnext  27053  clwlkclwwlklem2a1  27158  clwlkclwwlklem2a2  27159  clwlkclwwlklem2fv1  27161  clwlkclwwlklem2fv2  27162  clwlkclwwlklem2a4  27163  clwlkclwwlklem2a  27164  clwlkclwwlklem2  27166  clwlkclwwlk  27168  clwwisshclwwslem  27180  clwlksfclwwlk2wrdOLD  27255  clwlksfclwwlkOLD  27259  clwlksf1clwwlklem3OLD  27264  eucrctshift  27439  eucrct2eupth1  27440  eucrct2eupth  27441  numclwwlk5lem  27598  numclwwlk5  27599  numclwwlk7  27602  frgrreggt1  27604  nndiffz1  29898  xrge0mulgnn0  30037  hashf2  30494  signsvtn0  30995  fz0n  31960  bcneg1  31966  bccolsum  31969  faclimlem3  31975  faclim  31976  iprodfac  31977  poimirlem28  33769  mblfinlem1  33778  mblfinlem2  33779  nacsfix  37795  fzsplit1nn0  37837  eldioph2lem1  37843  fz1eqin  37852  diophin  37856  eq0rabdioph  37860  rexrabdioph  37878  rexzrexnn0  37888  irrapxlem4  37909  pell14qrss1234  37940  pell1qrss14  37952  monotoddzz  38027  rmxypos  38033  ltrmynn0  38034  ltrmxnn0  38035  lermxnn0  38036  rmxnn  38037  rmynn0  38043  jm2.17a  38046  jm2.17b  38047  rmygeid  38050  jm2.18  38074  jm2.19lem3  38077  jm2.19lem4  38078  jm2.22  38081  rmxdiophlem  38101  hbt  38219  proot1ex  38298  fzisoeu  40013  stirlinglem5  40792  elfzlble  41923  subsubelfzo0  41929  2ffzoeq  41931  fargshiftfo  41971  pfxnd  41988  pfxccat3  42019  pfxccat3a  42022  fmtnof1  42040  fmtnorec1  42042  goldbachthlem1  42050  odz2prm2pw  42068  flsqrt  42101  lighneallem4  42120  nn0eo  42908  nn0ofldiv2  42912  flnn0div2ge  42913  fllog2  42948  blenpw2  42958  blennngt2o2  42972  nn0digval  42980  dignn0fr  42981  digexp  42987  0dig2nn0e  42992  0dig2nn0o  42993  dig2bits  42994  dignn0flhalflem2  42996  dignn0ehalf  42997  dignn0flhalf  42998  nn0sumshdiglemB  43000