Theorem nn0z 12512

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℕ₀cn0 12401  ℤcz 12488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-neg 11367  df-nn 12146  df-n0 12402  df-z 12489

This theorem is referenced by:  nn0negz  12529  nn0ltp1le  12550  nn0leltp1  12551  nn0ltlem1  12552  nn0lt2  12555  nn0le2is012  12556  nn0lem1lt  12557  fnn0ind  12591  nn0pzuz  12818  nn0ge2m1nnALT  12855  fz1n  13458  ige2m1fz  13533  elfz2nn0  13534  fznn0  13535  elfz0add  13542  fzctr  13556  difelfzle  13557  fzoun  13612  fzofzim  13625  fzo1fzo0n0  13631  elincfzoext  13639  elfzodifsumelfzo  13647  fz0add1fz1  13651  zpnn0elfzo  13654  fzossfzop1  13659  ubmelm1fzo  13679  elfznelfzo  13689  flmulnn0  13747  quoremnn0  13776  zmodidfzoimp  13821  modmuladdnn0  13838  modfzo0difsn  13866  expdiv  14036  expnngt1  14164  faclbnd3  14215  bccmpl  14232  bcnp1n  14237  bcval5  14241  bcn2  14242  bcp1m1  14243  hashge2el2difr  14404  fi1uzind  14430  wrdred1  14483  wrdred1hash  14484  ccatalpha  14517  swrdnd0  14581  swrdfv2  14585  swrdsb0eq  14587  swrdsbslen  14588  swrdspsleq  14589  swrdlsw  14591  pfxnd  14611  pfxccatin12lem4  14649  pfxccatin12lem3  14655  pfxccat3  14657  swrdccat  14658  pfxccat3a  14661  revlen  14685  repswswrd  14707  repswccat  14709  cshwidxmodr  14727  cshf1  14733  2cshw  14736  cshweqrep  14744  cshwcshid  14750  cshwcsh2id  14751  cats1fv  14782  swrd2lsw  14875  2swrd2eqwrdeq  14876  isercoll  15591  iseraltlem2  15606  bcxmas  15758  geo2sum2  15797  geomulcvg  15799  risefacval2  15933  fallfacval2  15934  zrisefaccl  15943  zfallfaccl  15944  fallrisefac  15948  bpolylem  15971  fsumkthpow  15979  esum  16003  ege2le3  16013  eftlcl  16032  reeftlcl  16033  eftlub  16034  effsumlt  16036  eirrlem  16129  dvds1  16246  dvdsext  16248  addmodlteqALT  16252  oddnn02np1  16275  oddge22np1  16276  nn0ehalf  16305  nn0o1gt2  16308  nno  16309  nn0o  16310  nn0oddm1d2  16312  divalglem4  16323  divalglem5  16324  modremain  16335  bitsinv1  16369  nn0gcdid0  16448  nn0seqcvgd  16497  algcvga  16506  eucalgf  16510  nonsq  16686  numdenexp  16687  odzdvds  16723  coprimeprodsq  16736  coprimeprodsq2  16737  oddprm  16738  iserodd  16763  pcexp  16787  pcidlem  16800  pc11  16808  dvdsprmpweqle  16814  difsqpwdvds  16815  pcfac  16827  prmunb  16842  hashbc2  16934  cshwshashlem2  17024  chnccat  18549  smndex1ibas  18825  smndex1iidm  18826  smndex2dnrinv  18840  smndex2dlinvh  18842  mulgaddcom  19028  mulginvcom  19029  mulgz  19032  mulgdirlem  19035  mulgass  19041  mndodcongi  19472  oddvdsnn0  19473  odeq  19479  odmulg  19485  efgsdmi  19661  cyggex2  19826  fincygsubgodd  20043  mulgass2  20244  chrrhm  21486  zncrng  21499  znzrh2  21500  zndvds  21504  znchr  21517  znunit  21518  chfacfisf  22798  chfacfisfcpmat  22799  chfacfscmulfsupp  22803  chfacfpmmulfsupp  22807  clmmulg  25057  itgcnlem  25747  degltlem1  26033  plyco0  26153  dgreq0  26227  plydivex  26261  aannenlem1  26292  abelthlem1  26397  abelthlem3  26399  abelthlem8  26405  abelthlem9  26406  advlogexp  26620  cxpexp  26633  leibpi  26908  log2cnv  26910  log2tlbnd  26911  basellem2  27048  sgmnncl  27113  chpp1  27121  bcmono  27244  bcmax  27245  bcp1ctr  27246  lgsneg1  27289  lgsdirnn0  27311  lgsdinn0  27312  2lgslem1c  27360  2lgslem3a1  27367  2lgslem3b1  27368  2lgslem3c1  27369  2lgsoddprmlem2  27376  2sq2  27400  2sqreultlem  27414  dchrisumlem1  27456  qabvle  27592  ostth2lem2  27601  tgldimor  28574  upgrewlkle2  29680  wlkv0  29723  redwlk  29744  pthdadjvtx  29801  pthdlem1  29839  wwlknvtx  29918  wlkiswwlks2lem3  29944  wwlksm1edg  29954  wwlksnred  29965  wwlksnext  29966  clwlkclwwlklem2a1  30067  clwlkclwwlklem2a2  30068  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwlkclwwlk  30077  clwwisshclwwslem  30089  eucrctshift  30318  eucrct2eupth1  30319  eucrct2eupth  30320  numclwwlk5lem  30462  numclwwlk5  30463  numclwwlk7  30466  frgrreggt1  30468  nndiffz1  32866  nn0diffz0  32874  xrge0mulgnn0  33097  hashf2  34241  signsvtn0  34727  nn0ltp1ne  35306  0nn0m1nnn0  35307  pthhashvtx  35322  fz0n  35925  bcneg1  35930  bccolsum  35933  faclimlem3  35939  faclim  35940  iprodfac  35941  poimirlem28  37845  mblfinlem1  37854  mblfinlem2  37855  lcmineqlem2  42280  sticksstones22  42418  gcdnn0id  42580  negexpidd  42920  nacsfix  42950  fzsplit1nn0  42992  eldioph2lem1  42998  fz1eqin  43007  diophin  43010  eq0rabdioph  43014  rexrabdioph  43032  rexzrexnn0  43042  irrapxlem4  43063  pell14qrss1234  43094  pell1qrss14  43106  monotoddzz  43181  rmxypos  43185  ltrmynn0  43186  ltrmxnn0  43187  lermxnn0  43188  rmxnn  43189  rmynn0  43195  jm2.17a  43198  jm2.17b  43199  rmygeid  43202  jm2.18  43226  jm2.19lem3  43229  jm2.19lem4  43230  jm2.22  43233  rmxdiophlem  43253  hbt  43368  proot1ex  43434  fzisoeu  45544  stirlinglem5  46318  elfzlble  47562  subsubelfzo0  47568  2ffzoeq  47569  addmodne  47586  fargshiftfo  47684  fmtnof1  47777  fmtnorec1  47779  goldbachthlem1  47787  odz2prm2pw  47805  flsqrt  47835  lighneallem4  47852  nn0eo  48770  nn0ofldiv2  48774  flnn0div2ge  48775  fllog2  48810  blenpw2  48820  blennngt2o2  48834  nn0digval  48842  dignn0fr  48843  digexp  48849  0dig2nn0e  48854  0dig2nn0o  48855  dig2bits  48856  dignn0flhalflem2  48858  dignn0ehalf  48859  dignn0flhalf  48860  nn0sumshdiglemB  48862