Theorem nn0z 12548

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕ₀cn0 12437  ℤcz 12524

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525

This theorem is referenced by:  nn0negz  12565  nn0ltp1le  12587  nn0leltp1  12588  nn0ltlem1  12589  nn0lt2  12592  nn0le2is012  12593  nn0lem1lt  12594  fnn0ind  12628  nn0pzuz  12855  nn0ge2m1nnALT  12892  fz1n  13496  ige2m1fz  13571  elfz2nn0  13572  fznn0  13573  elfz0add  13580  fzctr  13594  difelfzle  13595  fzoun  13651  fzofzim  13664  fzo1fzo0n0  13670  elincfzoext  13678  elfzodifsumelfzo  13686  fz0add1fz1  13690  zpnn0elfzo  13693  fzossfzop1  13698  ubmelm1fzo  13718  elfznelfzo  13728  flmulnn0  13786  quoremnn0  13815  zmodidfzoimp  13860  modmuladdnn0  13877  modfzo0difsn  13905  expdiv  14075  expnngt1  14203  faclbnd3  14254  bccmpl  14271  bcnp1n  14276  bcval5  14280  bcn2  14281  bcp1m1  14282  hashge2el2difr  14443  fi1uzind  14469  wrdred1  14522  wrdred1hash  14523  ccatalpha  14556  swrdnd0  14620  swrdfv2  14624  swrdsb0eq  14626  swrdsbslen  14627  swrdspsleq  14628  swrdlsw  14630  pfxnd  14650  pfxccatin12lem4  14688  pfxccatin12lem3  14694  pfxccat3  14696  swrdccat  14697  pfxccat3a  14700  revlen  14724  repswswrd  14746  repswccat  14748  cshwidxmodr  14766  cshf1  14772  2cshw  14775  cshweqrep  14783  cshwcshid  14789  cshwcsh2id  14790  cats1fv  14821  swrd2lsw  14914  2swrd2eqwrdeq  14915  isercoll  15630  iseraltlem2  15645  bcxmas  15800  geo2sum2  15839  geomulcvg  15841  risefacval2  15975  fallfacval2  15976  zrisefaccl  15985  zfallfaccl  15986  fallrisefac  15990  bpolylem  16013  fsumkthpow  16021  esum  16045  ege2le3  16055  eftlcl  16074  reeftlcl  16075  eftlub  16076  effsumlt  16078  eirrlem  16171  dvds1  16288  dvdsext  16290  addmodlteqALT  16294  oddnn02np1  16317  oddge22np1  16318  nn0ehalf  16347  nn0o1gt2  16350  nno  16351  nn0o  16352  nn0oddm1d2  16354  divalglem4  16365  divalglem5  16366  modremain  16377  bitsinv1  16411  nn0gcdid0  16490  nn0seqcvgd  16539  algcvga  16548  eucalgf  16552  nonsq  16729  numdenexp  16730  odzdvds  16766  coprimeprodsq  16779  coprimeprodsq2  16780  oddprm  16781  iserodd  16806  pcexp  16830  pcidlem  16843  pc11  16851  dvdsprmpweqle  16857  difsqpwdvds  16858  pcfac  16870  prmunb  16885  hashbc2  16977  cshwshashlem2  17067  chnccat  18592  smndex1ibas  18868  smndex1iidm  18869  smndex2dnrinv  18886  smndex2dlinvh  18888  mulgaddcom  19074  mulginvcom  19075  mulgz  19078  mulgdirlem  19081  mulgass  19087  mndodcongi  19518  oddvdsnn0  19519  odeq  19525  odmulg  19531  efgsdmi  19707  cyggex2  19872  fincygsubgodd  20089  mulgass2  20290  chrrhm  21511  zncrng  21524  znzrh2  21525  zndvds  21529  znchr  21542  znunit  21543  chfacfisf  22819  chfacfisfcpmat  22820  chfacfscmulfsupp  22824  chfacfpmmulfsupp  22828  clmmulg  25068  itgcnlem  25757  degltlem1  26037  plyco0  26157  dgreq0  26230  plydivex  26263  aannenlem1  26294  abelthlem1  26396  abelthlem3  26398  abelthlem8  26404  abelthlem9  26405  advlogexp  26619  cxpexp  26632  leibpi  26906  log2cnv  26908  log2tlbnd  26909  basellem2  27045  sgmnncl  27110  chpp1  27118  bcmono  27240  bcmax  27241  bcp1ctr  27242  lgsneg1  27285  lgsdirnn0  27307  lgsdinn0  27308  2lgslem1c  27356  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgsoddprmlem2  27372  2sq2  27396  2sqreultlem  27410  dchrisumlem1  27452  qabvle  27588  ostth2lem2  27597  tgldimor  28570  upgrewlkle2  29675  wlkv0  29718  redwlk  29739  pthdadjvtx  29796  pthdlem1  29834  wwlknvtx  29913  wlkiswwlks2lem3  29939  wwlksm1edg  29949  wwlksnred  29960  wwlksnext  29961  clwlkclwwlklem2a1  30062  clwlkclwwlklem2a2  30063  clwlkclwwlklem2fv1  30065  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlk  30072  clwwisshclwwslem  30084  eucrctshift  30313  eucrct2eupth1  30314  eucrct2eupth  30315  numclwwlk5lem  30457  numclwwlk5  30458  numclwwlk7  30461  frgrreggt1  30463  nndiffz1  32859  nn0diffz0  32867  xrge0mulgnn0  33075  hashf2  34228  signsvtn0  34714  nn0ltp1ne  35294  0nn0m1nnn0  35295  pthhashvtx  35310  fz0n  35913  bcneg1  35918  bccolsum  35921  faclimlem3  35927  faclim  35928  iprodfac  35929  poimirlem28  37969  mblfinlem1  37978  mblfinlem2  37979  lcmineqlem2  42469  sticksstones22  42607  gcdnn0id  42761  negexpidd  43114  nacsfix  43144  fzsplit1nn0  43186  eldioph2lem1  43192  fz1eqin  43201  diophin  43204  eq0rabdioph  43208  rexrabdioph  43222  rexzrexnn0  43232  irrapxlem4  43253  pell14qrss1234  43284  pell1qrss14  43296  monotoddzz  43371  rmxypos  43375  ltrmynn0  43376  ltrmxnn0  43377  lermxnn0  43378  rmxnn  43379  rmynn0  43385  jm2.17a  43388  jm2.17b  43389  rmygeid  43392  jm2.18  43416  jm2.19lem3  43419  jm2.19lem4  43420  jm2.22  43423  rmxdiophlem  43443  hbt  43558  proot1ex  43624  fzisoeu  45733  stirlinglem5  46506  elfzlble  47768  subsubelfzo0  47775  2ffzoeq  47776  addmodne  47798  fargshiftfo  47902  fmtnof1  47998  fmtnorec1  48000  goldbachthlem1  48008  odz2prm2pw  48026  flsqrt  48056  lighneallem4  48073  nn0eo  49004  nn0ofldiv2  49008  flnn0div2ge  49009  fllog2  49044  blenpw2  49054  blennngt2o2  49068  nn0digval  49076  dignn0fr  49077  digexp  49083  0dig2nn0e  49088  0dig2nn0o  49089  dig2bits  49090  dignn0flhalflem2  49092  dignn0ehalf  49093  dignn0flhalf  49094  nn0sumshdiglemB  49096