Theorem nn0z 12389

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

Syntax hints:   → wi 4   ∈ wcel 2104  ℕ₀cn0 12279  ℤcz 12365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-i2m1 10985  ax-1ne0 10986  ax-rnegex 10988  ax-rrecex 10989  ax-cnre 10990

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-neg 11254  df-nn 12020  df-n0 12280  df-z 12366

This theorem is referenced by:  nn0negz  12404  nn0ltp1le  12424  nn0leltp1  12425  nn0ltlem1  12426  nn0lt2  12429  nn0le2is012  12430  nn0lem1lt  12431  fnn0ind  12465  nn0pzuz  12691  nn0ge2m1nnALT  12728  fz1n  13320  ige2m1fz  13392  elfz2nn0  13393  fznn0  13394  elfz0add  13401  fzctr  13414  difelfzle  13415  fzoun  13470  fzofzim  13480  fzo1fzo0n0  13484  elincfzoext  13491  elfzodifsumelfzo  13499  fz0add1fz1  13503  zpnn0elfzo  13506  fzossfzop1  13511  ubmelm1fzo  13529  elfznelfzo  13538  flmulnn0  13593  quoremnn0  13622  zmodidfzoimp  13667  modmuladdnn0  13681  modfzo0difsn  13709  expdiv  13880  expnngt1  14002  faclbnd3  14052  bccmpl  14069  bcnp1n  14074  bcval5  14078  bcn2  14079  bcp1m1  14080  hashge2el2difr  14240  fi1uzind  14256  wrdred1  14308  wrdred1hash  14309  ccatalpha  14343  swrdnd0  14415  swrdfv2  14419  swrdsb0eq  14421  swrdsbslen  14422  swrdspsleq  14423  swrdlsw  14425  pfxnd  14445  pfxccatin12lem4  14484  pfxccatin12lem3  14490  pfxccat3  14492  swrdccat  14493  pfxccat3a  14496  revlen  14520  repswswrd  14542  repswccat  14544  cshwidxmodr  14562  cshf1  14568  2cshw  14571  cshweqrep  14579  cshwcshid  14585  cshwcsh2id  14586  cats1fv  14617  swrd2lsw  14710  2swrd2eqwrdeq  14711  isercoll  15424  iseraltlem2  15439  bcxmas  15592  geo2sum2  15631  geomulcvg  15633  risefacval2  15765  fallfacval2  15766  zrisefaccl  15775  zfallfaccl  15776  fallrisefac  15780  bpolylem  15803  fsumkthpow  15811  esum  15835  ege2le3  15844  eftlcl  15861  reeftlcl  15862  eftlub  15863  effsumlt  15865  eirrlem  15958  dvds1  16073  dvdsext  16075  addmodlteqALT  16079  oddnn02np1  16102  oddge22np1  16103  nn0ehalf  16132  nn0o1gt2  16135  nno  16136  nn0o  16137  nn0oddm1d2  16139  divalglem4  16150  divalglem5  16151  modremain  16162  bitsinv1  16194  nn0gcdid0  16273  nn0seqcvgd  16320  algcvga  16329  eucalgf  16333  nonsq  16508  odzdvds  16541  coprimeprodsq  16554  coprimeprodsq2  16555  oddprm  16556  iserodd  16581  pcexp  16605  pcidlem  16618  pc11  16626  dvdsprmpweqle  16632  difsqpwdvds  16633  pcfac  16645  prmunb  16660  hashbc2  16752  cshwshashlem2  16843  smndex1ibas  18584  smndex1iidm  18585  smndex2dnrinv  18599  smndex2dlinvh  18601  mulgaddcom  18772  mulginvcom  18773  mulgz  18776  mulgdirlem  18779  mulgass  18785  mndodcongi  19196  oddvdsnn0  19197  odeq  19203  odmulg  19208  efgsdmi  19383  cyggex2  19543  fincygsubgodd  19760  mulgass2  19885  chrrhm  20780  zncrng  20797  znzrh2  20798  zndvds  20802  znchr  20815  znunit  20816  chfacfisf  22048  chfacfisfcpmat  22049  chfacfscmulfsupp  22053  chfacfpmmulfsupp  22057  clmmulg  24309  itgcnlem  24999  degltlem1  25282  plyco0  25398  dgreq0  25471  plydivex  25502  aannenlem1  25533  abelthlem1  25635  abelthlem3  25637  abelthlem8  25643  abelthlem9  25644  advlogexp  25855  cxpexp  25868  leibpi  26137  log2cnv  26139  log2tlbnd  26140  basellem2  26276  sgmnncl  26341  chpp1  26349  bcmono  26470  bcmax  26471  bcp1ctr  26472  lgsneg1  26515  lgsdirnn0  26537  lgsdinn0  26538  2lgslem1c  26586  2lgslem3a1  26593  2lgslem3b1  26594  2lgslem3c1  26595  2lgsoddprmlem2  26602  2sq2  26626  2sqreultlem  26640  dchrisumlem1  26682  qabvle  26818  ostth2lem2  26827  tgldimor  26908  upgrewlkle2  28018  wlkv0  28063  redwlk  28085  pthdadjvtx  28143  pthdlem1  28179  wwlknvtx  28255  wlkiswwlks2lem3  28281  wwlksm1edg  28291  wwlksnred  28302  wwlksnext  28303  clwlkclwwlklem2a1  28401  clwlkclwwlklem2a2  28402  clwlkclwwlklem2fv1  28404  clwlkclwwlklem2fv2  28405  clwlkclwwlklem2a4  28406  clwlkclwwlklem2a  28407  clwlkclwwlklem2  28409  clwlkclwwlk  28411  clwwisshclwwslem  28423  eucrctshift  28652  eucrct2eupth1  28653  eucrct2eupth  28654  numclwwlk5lem  28796  numclwwlk5  28797  numclwwlk7  28800  frgrreggt1  28802  nndiffz1  31152  xrge0mulgnn0  31343  hashf2  32097  signsvtn0  32594  nn0ltp1ne  33115  0nn0m1nnn0  33116  pthhashvtx  33134  fz0n  33741  bcneg1  33747  bccolsum  33750  faclimlem3  33756  faclim  33757  iprodfac  33758  poimirlem28  35849  mblfinlem1  35858  mblfinlem2  35859  lcmineqlem2  40080  sticksstones22  40166  gcdnn0id  40366  numdenexp  40374  negexpidd  40541  nacsfix  40571  fzsplit1nn0  40613  eldioph2lem1  40619  fz1eqin  40628  diophin  40631  eq0rabdioph  40635  rexrabdioph  40653  rexzrexnn0  40663  irrapxlem4  40684  pell14qrss1234  40715  pell1qrss14  40727  monotoddzz  40803  rmxypos  40807  ltrmynn0  40808  ltrmxnn0  40809  lermxnn0  40810  rmxnn  40811  rmynn0  40817  jm2.17a  40820  jm2.17b  40821  rmygeid  40824  jm2.18  40848  jm2.19lem3  40851  jm2.19lem4  40852  jm2.22  40855  rmxdiophlem  40875  hbt  40993  proot1ex  41064  fzisoeu  42887  stirlinglem5  43668  elfzlble  44870  subsubelfzo0  44876  2ffzoeq  44878  fargshiftfo  44952  fmtnof1  45045  fmtnorec1  45047  goldbachthlem1  45055  odz2prm2pw  45073  flsqrt  45103  lighneallem4  45120  nn0eo  45932  nn0ofldiv2  45936  flnn0div2ge  45937  fllog2  45972  blenpw2  45982  blennngt2o2  45996  nn0digval  46004  dignn0fr  46005  digexp  46011  0dig2nn0e  46016  0dig2nn0o  46017  dig2bits  46018  dignn0flhalflem2  46020  dignn0ehalf  46021  dignn0flhalf  46022  nn0sumshdiglemB  46024