Theorem nn0z 12165

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

Syntax hints:   → wi 4   ∈ wcel 2112  ℕ₀cn0 12055  ℤcz 12141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-i2m1 10762  ax-1ne0 10763  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-neg 11030  df-nn 11796  df-n0 12056  df-z 12142

This theorem is referenced by:  nn0negz  12180  nn0ltp1le  12200  nn0leltp1  12201  nn0ltlem1  12202  nn0lt2  12205  nn0le2is012  12206  nn0lem1lt  12207  fnn0ind  12241  nn0pzuz  12466  nn0ge2m1nnALT  12503  fz1n  13095  ige2m1fz  13167  elfz2nn0  13168  fznn0  13169  elfz0add  13176  fzctr  13189  difelfzle  13190  fzoun  13244  fzofzim  13254  fzo1fzo0n0  13258  elincfzoext  13265  elfzodifsumelfzo  13273  fz0add1fz1  13277  zpnn0elfzo  13280  fzossfzop1  13285  ubmelm1fzo  13303  elfznelfzo  13312  flmulnn0  13367  quoremnn0  13394  zmodidfzoimp  13439  modmuladdnn0  13453  modfzo0difsn  13481  expdiv  13651  expnngt1  13773  faclbnd3  13823  bccmpl  13840  bcnp1n  13845  bcval5  13849  bcn2  13850  bcp1m1  13851  hashge2el2difr  14012  fi1uzind  14028  wrdred1  14080  wrdred1hash  14081  ccatalpha  14115  swrdnd0  14187  swrdfv2  14191  swrdsb0eq  14193  swrdsbslen  14194  swrdspsleq  14195  swrdlsw  14197  pfxnd  14217  pfxccatin12lem4  14256  pfxccatin12lem3  14262  pfxccat3  14264  swrdccat  14265  pfxccat3a  14268  revlen  14292  repswswrd  14314  repswccat  14316  cshwidxmodr  14334  cshf1  14340  2cshw  14343  cshweqrep  14351  cshwcshid  14357  cshwcsh2id  14358  cats1fv  14389  swrd2lsw  14482  2swrd2eqwrdeq  14483  isercoll  15196  iseraltlem2  15211  bcxmas  15362  geo2sum2  15401  geomulcvg  15403  risefacval2  15535  fallfacval2  15536  zrisefaccl  15545  zfallfaccl  15546  fallrisefac  15550  bpolylem  15573  fsumkthpow  15581  esum  15605  ege2le3  15614  eftlcl  15631  reeftlcl  15632  eftlub  15633  effsumlt  15635  eirrlem  15728  dvds1  15843  dvdsext  15845  addmodlteqALT  15849  oddnn02np1  15872  oddge22np1  15873  nn0ehalf  15902  nn0o1gt2  15905  nno  15906  nn0o  15907  nn0oddm1d2  15909  divalglem4  15920  divalglem5  15921  modremain  15932  bitsinv1  15964  nn0gcdid0  16043  nn0seqcvgd  16090  algcvga  16099  eucalgf  16103  nonsq  16278  odzdvds  16311  coprimeprodsq  16324  coprimeprodsq2  16325  oddprm  16326  iserodd  16351  pcexp  16375  pcidlem  16388  pc11  16396  dvdsprmpweqle  16402  difsqpwdvds  16403  pcfac  16415  prmunb  16430  hashbc2  16522  cshwshashlem2  16613  smndex1ibas  18281  smndex1iidm  18282  smndex2dnrinv  18296  smndex2dlinvh  18298  mulgaddcom  18469  mulginvcom  18470  mulgz  18473  mulgdirlem  18476  mulgass  18482  mndodcongi  18889  oddvdsnn0  18890  odeq  18896  odmulg  18901  efgsdmi  19076  cyggex2  19236  fincygsubgodd  19453  mulgass2  19573  chrrhm  20450  zncrng  20463  znzrh2  20464  zndvds  20468  znchr  20481  znunit  20482  chfacfisf  21705  chfacfisfcpmat  21706  chfacfscmulfsupp  21710  chfacfpmmulfsupp  21714  clmmulg  23952  itgcnlem  24641  degltlem1  24924  plyco0  25040  dgreq0  25113  plydivex  25144  aannenlem1  25175  abelthlem1  25277  abelthlem3  25279  abelthlem8  25285  abelthlem9  25286  advlogexp  25497  cxpexp  25510  leibpi  25779  log2cnv  25781  log2tlbnd  25782  basellem2  25918  sgmnncl  25983  chpp1  25991  bcmono  26112  bcmax  26113  bcp1ctr  26114  lgsneg1  26157  lgsdirnn0  26179  lgsdinn0  26180  2lgslem1c  26228  2lgslem3a1  26235  2lgslem3b1  26236  2lgslem3c1  26237  2lgsoddprmlem2  26244  2sq2  26268  2sqreultlem  26282  dchrisumlem1  26324  qabvle  26460  ostth2lem2  26469  tgldimor  26547  upgrewlkle2  27648  wlkv0  27692  redwlk  27714  pthdadjvtx  27771  pthdlem1  27807  wwlknvtx  27883  wlkiswwlks2lem3  27909  wwlksm1edg  27919  wwlksnred  27930  wwlksnext  27931  clwlkclwwlklem2a1  28029  clwlkclwwlklem2a2  28030  clwlkclwwlklem2fv1  28032  clwlkclwwlklem2fv2  28033  clwlkclwwlklem2a4  28034  clwlkclwwlklem2a  28035  clwlkclwwlklem2  28037  clwlkclwwlk  28039  clwwisshclwwslem  28051  eucrctshift  28280  eucrct2eupth1  28281  eucrct2eupth  28282  numclwwlk5lem  28424  numclwwlk5  28425  numclwwlk7  28428  frgrreggt1  28430  nndiffz1  30781  xrge0mulgnn0  30971  hashf2  31718  signsvtn0  32215  nn0ltp1ne  32737  0nn0m1nnn0  32738  pthhashvtx  32756  fz0n  33365  bcneg1  33371  bccolsum  33374  faclimlem3  33380  faclim  33381  iprodfac  33382  poimirlem28  35491  mblfinlem1  35500  mblfinlem2  35501  lcmineqlem2  39721  gcdnn0id  39978  numdenexp  39986  negexpidd  40148  nacsfix  40178  fzsplit1nn0  40220  eldioph2lem1  40226  fz1eqin  40235  diophin  40238  eq0rabdioph  40242  rexrabdioph  40260  rexzrexnn0  40270  irrapxlem4  40291  pell14qrss1234  40322  pell1qrss14  40334  monotoddzz  40409  rmxypos  40413  ltrmynn0  40414  ltrmxnn0  40415  lermxnn0  40416  rmxnn  40417  rmynn0  40423  jm2.17a  40426  jm2.17b  40427  rmygeid  40430  jm2.18  40454  jm2.19lem3  40457  jm2.19lem4  40458  jm2.22  40461  rmxdiophlem  40481  hbt  40599  proot1ex  40670  fzisoeu  42453  stirlinglem5  43237  elfzlble  44428  subsubelfzo0  44434  2ffzoeq  44436  fargshiftfo  44510  fmtnof1  44603  fmtnorec1  44605  goldbachthlem1  44613  odz2prm2pw  44631  flsqrt  44661  lighneallem4  44678  nn0eo  45490  nn0ofldiv2  45494  flnn0div2ge  45495  fllog2  45530  blenpw2  45540  blennngt2o2  45554  nn0digval  45562  dignn0fr  45563  digexp  45569  0dig2nn0e  45574  0dig2nn0o  45575  dig2bits  45576  dignn0flhalflem2  45578  dignn0ehalf  45579  dignn0flhalf  45580  nn0sumshdiglemB  45582