Theorem nn0z 12533

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℕ₀cn0 12422  ℤcz 12508

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-i2m1 11128  ax-1ne0 11129  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-neg 11397  df-nn 12163  df-n0 12423  df-z 12509

This theorem is referenced by:  nn0negz  12550  nn0ltp1le  12570  nn0leltp1  12571  nn0ltlem1  12572  nn0lt2  12575  nn0le2is012  12576  nn0lem1lt  12577  fnn0ind  12611  nn0pzuz  12839  nn0ge2m1nnALT  12876  fz1n  13469  ige2m1fz  13541  elfz2nn0  13542  fznn0  13543  elfz0add  13550  fzctr  13563  difelfzle  13564  fzoun  13619  fzofzim  13629  fzo1fzo0n0  13633  elincfzoext  13640  elfzodifsumelfzo  13648  fz0add1fz1  13652  zpnn0elfzo  13655  fzossfzop1  13660  ubmelm1fzo  13678  elfznelfzo  13687  flmulnn0  13742  quoremnn0  13771  zmodidfzoimp  13816  modmuladdnn0  13830  modfzo0difsn  13858  expdiv  14029  expnngt1  14154  faclbnd3  14202  bccmpl  14219  bcnp1n  14224  bcval5  14228  bcn2  14229  bcp1m1  14230  hashge2el2difr  14392  fi1uzind  14408  wrdred1  14460  wrdred1hash  14461  ccatalpha  14493  swrdnd0  14557  swrdfv2  14561  swrdsb0eq  14563  swrdsbslen  14564  swrdspsleq  14565  swrdlsw  14567  pfxnd  14587  pfxccatin12lem4  14626  pfxccatin12lem3  14632  pfxccat3  14634  swrdccat  14635  pfxccat3a  14638  revlen  14662  repswswrd  14684  repswccat  14686  cshwidxmodr  14704  cshf1  14710  2cshw  14713  cshweqrep  14721  cshwcshid  14728  cshwcsh2id  14729  cats1fv  14760  swrd2lsw  14853  2swrd2eqwrdeq  14854  isercoll  15564  iseraltlem2  15579  bcxmas  15731  geo2sum2  15770  geomulcvg  15772  risefacval2  15904  fallfacval2  15905  zrisefaccl  15914  zfallfaccl  15915  fallrisefac  15919  bpolylem  15942  fsumkthpow  15950  esum  15974  ege2le3  15983  eftlcl  16000  reeftlcl  16001  eftlub  16002  effsumlt  16004  eirrlem  16097  dvds1  16212  dvdsext  16214  addmodlteqALT  16218  oddnn02np1  16241  oddge22np1  16242  nn0ehalf  16271  nn0o1gt2  16274  nno  16275  nn0o  16276  nn0oddm1d2  16278  divalglem4  16289  divalglem5  16290  modremain  16301  bitsinv1  16333  nn0gcdid0  16412  nn0seqcvgd  16457  algcvga  16466  eucalgf  16470  nonsq  16645  odzdvds  16678  coprimeprodsq  16691  coprimeprodsq2  16692  oddprm  16693  iserodd  16718  pcexp  16742  pcidlem  16755  pc11  16763  dvdsprmpweqle  16769  difsqpwdvds  16770  pcfac  16782  prmunb  16797  hashbc2  16889  cshwshashlem2  16980  smndex1ibas  18724  smndex1iidm  18725  smndex2dnrinv  18739  smndex2dlinvh  18741  mulgaddcom  18914  mulginvcom  18915  mulgz  18918  mulgdirlem  18921  mulgass  18927  mndodcongi  19339  oddvdsnn0  19340  odeq  19346  odmulg  19352  efgsdmi  19528  cyggex2  19688  fincygsubgodd  19905  mulgass2  20039  chrrhm  20971  zncrng  20988  znzrh2  20989  zndvds  20993  znchr  21006  znunit  21007  chfacfisf  22240  chfacfisfcpmat  22241  chfacfscmulfsupp  22245  chfacfpmmulfsupp  22249  clmmulg  24501  itgcnlem  25191  degltlem1  25474  plyco0  25590  dgreq0  25663  plydivex  25694  aannenlem1  25725  abelthlem1  25827  abelthlem3  25829  abelthlem8  25835  abelthlem9  25836  advlogexp  26047  cxpexp  26060  leibpi  26329  log2cnv  26331  log2tlbnd  26332  basellem2  26468  sgmnncl  26533  chpp1  26541  bcmono  26662  bcmax  26663  bcp1ctr  26664  lgsneg1  26707  lgsdirnn0  26729  lgsdinn0  26730  2lgslem1c  26778  2lgslem3a1  26785  2lgslem3b1  26786  2lgslem3c1  26787  2lgsoddprmlem2  26794  2sq2  26818  2sqreultlem  26832  dchrisumlem1  26874  qabvle  27010  ostth2lem2  27019  tgldimor  27507  upgrewlkle2  28617  wlkv0  28662  redwlk  28683  pthdadjvtx  28741  pthdlem1  28777  wwlknvtx  28853  wlkiswwlks2lem3  28879  wwlksm1edg  28889  wwlksnred  28900  wwlksnext  28901  clwlkclwwlklem2a1  28999  clwlkclwwlklem2a2  29000  clwlkclwwlklem2fv1  29002  clwlkclwwlklem2fv2  29003  clwlkclwwlklem2a4  29004  clwlkclwwlklem2a  29005  clwlkclwwlklem2  29007  clwlkclwwlk  29009  clwwisshclwwslem  29021  eucrctshift  29250  eucrct2eupth1  29251  eucrct2eupth  29252  numclwwlk5lem  29394  numclwwlk5  29395  numclwwlk7  29398  frgrreggt1  29400  nndiffz1  31757  xrge0mulgnn0  31950  hashf2  32772  signsvtn0  33271  nn0ltp1ne  33791  0nn0m1nnn0  33792  pthhashvtx  33808  fz0n  34389  bcneg1  34395  bccolsum  34398  faclimlem3  34404  faclim  34405  iprodfac  34406  poimirlem28  36179  mblfinlem1  36188  mblfinlem2  36189  lcmineqlem2  40560  sticksstones22  40649  gcdnn0id  40873  numdenexp  40881  negexpidd  41063  nacsfix  41093  fzsplit1nn0  41135  eldioph2lem1  41141  fz1eqin  41150  diophin  41153  eq0rabdioph  41157  rexrabdioph  41175  rexzrexnn0  41185  irrapxlem4  41206  pell14qrss1234  41237  pell1qrss14  41249  monotoddzz  41325  rmxypos  41329  ltrmynn0  41330  ltrmxnn0  41331  lermxnn0  41332  rmxnn  41333  rmynn0  41339  jm2.17a  41342  jm2.17b  41343  rmygeid  41346  jm2.18  41370  jm2.19lem3  41373  jm2.19lem4  41374  jm2.22  41377  rmxdiophlem  41397  hbt  41515  proot1ex  41586  fzisoeu  43655  stirlinglem5  44439  elfzlble  45672  subsubelfzo0  45678  2ffzoeq  45680  fargshiftfo  45754  fmtnof1  45847  fmtnorec1  45849  goldbachthlem1  45857  odz2prm2pw  45875  flsqrt  45905  lighneallem4  45922  nn0eo  46734  nn0ofldiv2  46738  flnn0div2ge  46739  fllog2  46774  blenpw2  46784  blennngt2o2  46798  nn0digval  46806  dignn0fr  46807  digexp  46813  0dig2nn0e  46818  0dig2nn0o  46819  dig2bits  46820  dignn0flhalflem2  46822  dignn0ehalf  46823  dignn0flhalf  46824  nn0sumshdiglemB  46826