Theorem nn0z 12326

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕ₀cn0 12216  ℤcz 12302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-i2m1 10923  ax-1ne0 10924  ax-rnegex 10926  ax-rrecex 10927  ax-cnre 10928

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-om 7701  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-neg 11191  df-nn 11957  df-n0 12217  df-z 12303

This theorem is referenced by:  nn0negz  12341  nn0ltp1le  12361  nn0leltp1  12362  nn0ltlem1  12363  nn0lt2  12366  nn0le2is012  12367  nn0lem1lt  12368  fnn0ind  12402  nn0pzuz  12627  nn0ge2m1nnALT  12664  fz1n  13256  ige2m1fz  13328  elfz2nn0  13329  fznn0  13330  elfz0add  13337  fzctr  13350  difelfzle  13351  fzoun  13405  fzofzim  13415  fzo1fzo0n0  13419  elincfzoext  13426  elfzodifsumelfzo  13434  fz0add1fz1  13438  zpnn0elfzo  13441  fzossfzop1  13446  ubmelm1fzo  13464  elfznelfzo  13473  flmulnn0  13528  quoremnn0  13557  zmodidfzoimp  13602  modmuladdnn0  13616  modfzo0difsn  13644  expdiv  13815  expnngt1  13937  faclbnd3  13987  bccmpl  14004  bcnp1n  14009  bcval5  14013  bcn2  14014  bcp1m1  14015  hashge2el2difr  14176  fi1uzind  14192  wrdred1  14244  wrdred1hash  14245  ccatalpha  14279  swrdnd0  14351  swrdfv2  14355  swrdsb0eq  14357  swrdsbslen  14358  swrdspsleq  14359  swrdlsw  14361  pfxnd  14381  pfxccatin12lem4  14420  pfxccatin12lem3  14426  pfxccat3  14428  swrdccat  14429  pfxccat3a  14432  revlen  14456  repswswrd  14478  repswccat  14480  cshwidxmodr  14498  cshf1  14504  2cshw  14507  cshweqrep  14515  cshwcshid  14521  cshwcsh2id  14522  cats1fv  14553  swrd2lsw  14646  2swrd2eqwrdeq  14647  isercoll  15360  iseraltlem2  15375  bcxmas  15528  geo2sum2  15567  geomulcvg  15569  risefacval2  15701  fallfacval2  15702  zrisefaccl  15711  zfallfaccl  15712  fallrisefac  15716  bpolylem  15739  fsumkthpow  15747  esum  15771  ege2le3  15780  eftlcl  15797  reeftlcl  15798  eftlub  15799  effsumlt  15801  eirrlem  15894  dvds1  16009  dvdsext  16011  addmodlteqALT  16015  oddnn02np1  16038  oddge22np1  16039  nn0ehalf  16068  nn0o1gt2  16071  nno  16072  nn0o  16073  nn0oddm1d2  16075  divalglem4  16086  divalglem5  16087  modremain  16098  bitsinv1  16130  nn0gcdid0  16209  nn0seqcvgd  16256  algcvga  16265  eucalgf  16269  nonsq  16444  odzdvds  16477  coprimeprodsq  16490  coprimeprodsq2  16491  oddprm  16492  iserodd  16517  pcexp  16541  pcidlem  16554  pc11  16562  dvdsprmpweqle  16568  difsqpwdvds  16569  pcfac  16581  prmunb  16596  hashbc2  16688  cshwshashlem2  16779  smndex1ibas  18520  smndex1iidm  18521  smndex2dnrinv  18535  smndex2dlinvh  18537  mulgaddcom  18708  mulginvcom  18709  mulgz  18712  mulgdirlem  18715  mulgass  18721  mndodcongi  19132  oddvdsnn0  19133  odeq  19139  odmulg  19144  efgsdmi  19319  cyggex2  19479  fincygsubgodd  19696  mulgass2  19821  chrrhm  20716  zncrng  20733  znzrh2  20734  zndvds  20738  znchr  20751  znunit  20752  chfacfisf  21984  chfacfisfcpmat  21985  chfacfscmulfsupp  21989  chfacfpmmulfsupp  21993  clmmulg  24245  itgcnlem  24935  degltlem1  25218  plyco0  25334  dgreq0  25407  plydivex  25438  aannenlem1  25469  abelthlem1  25571  abelthlem3  25573  abelthlem8  25579  abelthlem9  25580  advlogexp  25791  cxpexp  25804  leibpi  26073  log2cnv  26075  log2tlbnd  26076  basellem2  26212  sgmnncl  26277  chpp1  26285  bcmono  26406  bcmax  26407  bcp1ctr  26408  lgsneg1  26451  lgsdirnn0  26473  lgsdinn0  26474  2lgslem1c  26522  2lgslem3a1  26529  2lgslem3b1  26530  2lgslem3c1  26531  2lgsoddprmlem2  26538  2sq2  26562  2sqreultlem  26576  dchrisumlem1  26618  qabvle  26754  ostth2lem2  26763  tgldimor  26844  upgrewlkle2  27954  wlkv0  27998  redwlk  28020  pthdadjvtx  28077  pthdlem1  28113  wwlknvtx  28189  wlkiswwlks2lem3  28215  wwlksm1edg  28225  wwlksnred  28236  wwlksnext  28237  clwlkclwwlklem2a1  28335  clwlkclwwlklem2a2  28336  clwlkclwwlklem2fv1  28338  clwlkclwwlklem2fv2  28339  clwlkclwwlklem2a4  28340  clwlkclwwlklem2a  28341  clwlkclwwlklem2  28343  clwlkclwwlk  28345  clwwisshclwwslem  28357  eucrctshift  28586  eucrct2eupth1  28587  eucrct2eupth  28588  numclwwlk5lem  28730  numclwwlk5  28731  numclwwlk7  28734  frgrreggt1  28736  nndiffz1  31086  xrge0mulgnn0  31277  hashf2  32031  signsvtn0  32528  nn0ltp1ne  33049  0nn0m1nnn0  33050  pthhashvtx  33068  fz0n  33675  bcneg1  33681  bccolsum  33684  faclimlem3  33690  faclim  33691  iprodfac  33692  poimirlem28  35784  mblfinlem1  35793  mblfinlem2  35794  lcmineqlem2  40018  sticksstones22  40104  gcdnn0id  40309  numdenexp  40317  negexpidd  40484  nacsfix  40514  fzsplit1nn0  40556  eldioph2lem1  40562  fz1eqin  40571  diophin  40574  eq0rabdioph  40578  rexrabdioph  40596  rexzrexnn0  40606  irrapxlem4  40627  pell14qrss1234  40658  pell1qrss14  40670  monotoddzz  40745  rmxypos  40749  ltrmynn0  40750  ltrmxnn0  40751  lermxnn0  40752  rmxnn  40753  rmynn0  40759  jm2.17a  40762  jm2.17b  40763  rmygeid  40766  jm2.18  40790  jm2.19lem3  40793  jm2.19lem4  40794  jm2.22  40797  rmxdiophlem  40817  hbt  40935  proot1ex  41006  fzisoeu  42793  stirlinglem5  43573  elfzlble  44764  subsubelfzo0  44770  2ffzoeq  44772  fargshiftfo  44846  fmtnof1  44939  fmtnorec1  44941  goldbachthlem1  44949  odz2prm2pw  44967  flsqrt  44997  lighneallem4  45014  nn0eo  45826  nn0ofldiv2  45830  flnn0div2ge  45831  fllog2  45866  blenpw2  45876  blennngt2o2  45890  nn0digval  45898  dignn0fr  45899  digexp  45905  0dig2nn0e  45910  0dig2nn0o  45911  dig2bits  45912  dignn0flhalflem2  45914  dignn0ehalf  45915  dignn0flhalf  45916  nn0sumshdiglemB  45918