Theorem nn0z 12638

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕ₀cn0 12526  ℤcz 12613

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614

This theorem is referenced by:  nn0negz  12655  nn0ltp1le  12676  nn0leltp1  12677  nn0ltlem1  12678  nn0lt2  12681  nn0le2is012  12682  nn0lem1lt  12683  fnn0ind  12717  nn0pzuz  12947  nn0ge2m1nnALT  12984  fz1n  13582  ige2m1fz  13657  elfz2nn0  13658  fznn0  13659  elfz0add  13666  fzctr  13680  difelfzle  13681  fzoun  13736  fzofzim  13749  fzo1fzo0n0  13754  elincfzoext  13762  elfzodifsumelfzo  13770  fz0add1fz1  13774  zpnn0elfzo  13777  fzossfzop1  13782  ubmelm1fzo  13802  elfznelfzo  13811  flmulnn0  13867  quoremnn0  13896  zmodidfzoimp  13941  modmuladdnn0  13956  modfzo0difsn  13984  expdiv  14154  expnngt1  14280  faclbnd3  14331  bccmpl  14348  bcnp1n  14353  bcval5  14357  bcn2  14358  bcp1m1  14359  hashge2el2difr  14520  fi1uzind  14546  wrdred1  14598  wrdred1hash  14599  ccatalpha  14631  swrdnd0  14695  swrdfv2  14699  swrdsb0eq  14701  swrdsbslen  14702  swrdspsleq  14703  swrdlsw  14705  pfxnd  14725  pfxccatin12lem4  14764  pfxccatin12lem3  14770  pfxccat3  14772  swrdccat  14773  pfxccat3a  14776  revlen  14800  repswswrd  14822  repswccat  14824  cshwidxmodr  14842  cshf1  14848  2cshw  14851  cshweqrep  14859  cshwcshid  14866  cshwcsh2id  14867  cats1fv  14898  swrd2lsw  14991  2swrd2eqwrdeq  14992  isercoll  15704  iseraltlem2  15719  bcxmas  15871  geo2sum2  15910  geomulcvg  15912  risefacval2  16046  fallfacval2  16047  zrisefaccl  16056  zfallfaccl  16057  fallrisefac  16061  bpolylem  16084  fsumkthpow  16092  esum  16116  ege2le3  16126  eftlcl  16143  reeftlcl  16144  eftlub  16145  effsumlt  16147  eirrlem  16240  dvds1  16356  dvdsext  16358  addmodlteqALT  16362  oddnn02np1  16385  oddge22np1  16386  nn0ehalf  16415  nn0o1gt2  16418  nno  16419  nn0o  16420  nn0oddm1d2  16422  divalglem4  16433  divalglem5  16434  modremain  16445  bitsinv1  16479  nn0gcdid0  16558  nn0seqcvgd  16607  algcvga  16616  eucalgf  16620  nonsq  16796  numdenexp  16797  odzdvds  16833  coprimeprodsq  16846  coprimeprodsq2  16847  oddprm  16848  iserodd  16873  pcexp  16897  pcidlem  16910  pc11  16918  dvdsprmpweqle  16924  difsqpwdvds  16925  pcfac  16937  prmunb  16952  hashbc2  17044  cshwshashlem2  17134  smndex1ibas  18913  smndex1iidm  18914  smndex2dnrinv  18928  smndex2dlinvh  18930  mulgaddcom  19116  mulginvcom  19117  mulgz  19120  mulgdirlem  19123  mulgass  19129  mndodcongi  19561  oddvdsnn0  19562  odeq  19568  odmulg  19574  efgsdmi  19750  cyggex2  19915  fincygsubgodd  20132  mulgass2  20306  chrrhm  21546  zncrng  21563  znzrh2  21564  zndvds  21568  znchr  21581  znunit  21582  chfacfisf  22860  chfacfisfcpmat  22861  chfacfscmulfsupp  22865  chfacfpmmulfsupp  22869  clmmulg  25134  itgcnlem  25825  degltlem1  26111  plyco0  26231  dgreq0  26305  plydivex  26339  aannenlem1  26370  abelthlem1  26475  abelthlem3  26477  abelthlem8  26483  abelthlem9  26484  advlogexp  26697  cxpexp  26710  leibpi  26985  log2cnv  26987  log2tlbnd  26988  basellem2  27125  sgmnncl  27190  chpp1  27198  bcmono  27321  bcmax  27322  bcp1ctr  27323  lgsneg1  27366  lgsdirnn0  27388  lgsdinn0  27389  2lgslem1c  27437  2lgslem3a1  27444  2lgslem3b1  27445  2lgslem3c1  27446  2lgsoddprmlem2  27453  2sq2  27477  2sqreultlem  27491  dchrisumlem1  27533  qabvle  27669  ostth2lem2  27678  tgldimor  28510  upgrewlkle2  29624  wlkv0  29669  redwlk  29690  pthdadjvtx  29748  pthdlem1  29786  wwlknvtx  29865  wlkiswwlks2lem3  29891  wwlksm1edg  29901  wwlksnred  29912  wwlksnext  29913  clwlkclwwlklem2a1  30011  clwlkclwwlklem2a2  30012  clwlkclwwlklem2fv1  30014  clwlkclwwlklem2fv2  30015  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwlkclwwlk  30021  clwwisshclwwslem  30033  eucrctshift  30262  eucrct2eupth1  30263  eucrct2eupth  30264  numclwwlk5lem  30406  numclwwlk5  30407  numclwwlk7  30410  frgrreggt1  30412  nndiffz1  32788  xrge0mulgnn0  33020  hashf2  34085  signsvtn0  34585  nn0ltp1ne  35117  0nn0m1nnn0  35118  pthhashvtx  35133  fz0n  35731  bcneg1  35736  bccolsum  35739  faclimlem3  35745  faclim  35746  iprodfac  35747  poimirlem28  37655  mblfinlem1  37664  mblfinlem2  37665  lcmineqlem2  42031  sticksstones22  42169  gcdnn0id  42364  negexpidd  42693  nacsfix  42723  fzsplit1nn0  42765  eldioph2lem1  42771  fz1eqin  42780  diophin  42783  eq0rabdioph  42787  rexrabdioph  42805  rexzrexnn0  42815  irrapxlem4  42836  pell14qrss1234  42867  pell1qrss14  42879  monotoddzz  42955  rmxypos  42959  ltrmynn0  42960  ltrmxnn0  42961  lermxnn0  42962  rmxnn  42963  rmynn0  42969  jm2.17a  42972  jm2.17b  42973  rmygeid  42976  jm2.18  43000  jm2.19lem3  43003  jm2.19lem4  43004  jm2.22  43007  rmxdiophlem  43027  hbt  43142  proot1ex  43208  fzisoeu  45312  stirlinglem5  46093  elfzlble  47332  subsubelfzo0  47338  2ffzoeq  47339  addmodne  47346  fargshiftfo  47429  fmtnof1  47522  fmtnorec1  47524  goldbachthlem1  47532  odz2prm2pw  47550  flsqrt  47580  lighneallem4  47597  nn0eo  48449  nn0ofldiv2  48453  flnn0div2ge  48454  fllog2  48489  blenpw2  48499  blennngt2o2  48513  nn0digval  48521  dignn0fr  48522  digexp  48528  0dig2nn0e  48533  0dig2nn0o  48534  dig2bits  48535  dignn0flhalflem2  48537  dignn0ehalf  48538  dignn0flhalf  48539  nn0sumshdiglemB  48541