Theorem nn0z 11818

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

Syntax hints:   → wi 4   ∈ wcel 2050  ℕ₀cn0 11707  ℤcz 11793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-i2m1 10403  ax-1ne0 10404  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-ov 6979  df-om 7397  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-neg 10673  df-nn 11440  df-n0 11708  df-z 11794

This theorem is referenced by:  nn0negz  11833  nn0ltp1le  11853  nn0leltp1  11854  nn0ltlem1  11855  nn0lt2  11858  nn0le2is012  11859  nn0lem1lt  11860  fnn0ind  11894  nn0pzuz  12119  nn0ge2m1nnALT  12156  fz1n  12741  ige2m1fz  12813  elfz2nn0  12814  fznn0  12815  elfz0add  12822  fzctr  12835  difelfzle  12836  fzoun  12889  fzofzim  12899  fzo1fzo0n0  12903  elincfzoext  12910  elfzodifsumelfzo  12918  fz0add1fz1  12922  zpnn0elfzo  12925  fzossfzop1  12930  ubmelm1fzo  12948  elfznelfzo  12957  flmulnn0  13012  quoremnn0  13039  zmodidfzoimp  13084  modmuladdnn0  13098  modfzo0difsn  13126  expdiv  13295  expnngt1  13417  faclbnd3  13467  bccmpl  13484  bcnp1n  13489  bcval5  13493  bcn2  13494  bcp1m1  13495  hashge2el2difr  13650  fi1uzind  13666  wrdred1  13723  wrdred1hash  13724  ccatalpha  13756  swrdnd0  13825  swrdfv2  13838  swrdsb0eq  13840  swrdsbslen  13841  swrdspsleq  13842  swrdlsw  13845  2swrd1eqwrdeqOLD  13847  pfxnd  13869  swrdccatin12lem1  13925  swrdccatin12lem3  13933  pfxccat3  13936  swrdccat3OLD  13937  swrdccat  13938  swrdccatOLD  13939  pfxccat3a  13942  revlen  13981  repswswrd  14003  repswccat  14005  cshwidxmodr  14028  cshf1  14034  2cshw  14037  cshweqrep  14045  cshwcshid  14051  cshwcsh2id  14052  cats1fv  14083  swrd2lsw  14176  2swrd2eqwrdeq  14177  2swrd2eqwrdeqOLD  14178  isercoll  14885  iseraltlem2  14900  bcxmas  15050  geo2sum2  15090  geomulcvg  15092  risefacval2  15224  fallfacval2  15225  zrisefaccl  15234  zfallfaccl  15235  fallrisefac  15239  bpolylem  15262  fsumkthpow  15270  esum  15294  ege2le3  15303  eftlcl  15320  reeftlcl  15321  eftlub  15322  effsumlt  15324  eirrlem  15417  dvds1  15529  dvdsext  15531  addmodlteqALT  15535  oddnn02np1  15557  oddge22np1  15558  nn0ehalf  15589  nn0o1gt2  15592  nno  15593  nn0o  15594  nn0oddm1d2  15596  divalglem4  15607  divalglem5  15608  modremain  15619  bitsinv1  15651  nn0gcdid0  15729  nn0seqcvgd  15770  algcvga  15779  eucalgf  15783  nonsq  15955  odzdvds  15988  coprimeprodsq  16001  coprimeprodsq2  16002  oddprm  16003  iserodd  16028  pcexp  16052  pcidlem  16064  pc11  16072  dvdsprmpweqle  16078  difsqpwdvds  16079  pcfac  16091  prmunb  16106  hashbc2  16198  cshwshashlem2  16286  mulgaddcom  18035  mulginvcom  18036  mulgz  18039  mulgdirlem  18042  mulgass  18048  mndodcongi  18433  oddvdsnn0  18434  odeq  18440  odmulg  18444  efgsdmi  18616  cyggex2  18771  mulgass2  19074  chrrhm  20380  zncrng  20393  znzrh2  20394  zndvds  20398  znchr  20411  znunit  20412  chfacfisf  21166  chfacfisfcpmat  21167  chfacfscmulfsupp  21171  chfacfpmmulfsupp  21175  clmmulg  23408  itgcnlem  24093  degltlem1  24369  plyco0  24485  dgreq0  24558  plydivex  24589  aannenlem1  24620  abelthlem1  24722  abelthlem3  24724  abelthlem8  24730  abelthlem9  24731  advlogexp  24939  cxpexp  24952  leibpilem1OLD  25220  leibpi  25222  log2cnv  25224  log2tlbnd  25225  basellem2  25361  sgmnncl  25426  chpp1  25434  bcmono  25555  bcmax  25556  bcp1ctr  25557  lgsneg1  25600  lgsdirnn0  25622  lgsdinn0  25623  2lgslem1c  25671  2lgslem3a1  25678  2lgslem3b1  25679  2lgslem3c1  25680  2lgsoddprmlem2  25687  2sq2  25711  2sqreultlem  25725  dchrisumlem1  25767  qabvle  25903  ostth2lem2  25912  tgldimor  25990  upgrewlkle2  27091  wlkv0  27135  redwlk  27160  pthdadjvtx  27219  pthdlem1  27255  wwlknvtx  27331  wlkiswwlks2lem3  27357  wwlksm1edg  27367  wwlksm1edgOLD  27368  wwlksnred  27379  wwlksnredOLD  27380  wwlksnext  27381  clwlkclwwlklem2a1  27498  clwlkclwwlklem2a2  27499  clwlkclwwlklem2fv1  27501  clwlkclwwlklem2fv2  27502  clwlkclwwlklem2a4  27503  clwlkclwwlklem2a  27504  clwlkclwwlklem2  27506  clwlkclwwlk  27508  clwlkclwwlkOLD  27509  clwwisshclwwslem  27529  eucrctshift  27773  eucrct2eupth1  27774  eucrct2eupth1OLD  27775  eucrct2eupthOLD  27776  eucrct2eupth  27777  numclwwlk5lem  27944  numclwwlk5  27945  numclwwlk7  27948  frgrreggt1  27950  nndiffz1  30268  xrge0mulgnn0  30414  hashf2  30993  signsvtn0  31492  signsvtn0OLD  31493  fz0n  32488  bcneg1  32494  bccolsum  32497  faclimlem3  32503  faclim  32504  iprodfac  32505  poimirlem28  34367  mblfinlem1  34376  mblfinlem2  34377  numdenexp  38624  nacsfix  38710  fzsplit1nn0  38752  eldioph2lem1  38758  fz1eqin  38767  diophin  38771  eq0rabdioph  38775  rexrabdioph  38793  rexzrexnn0  38803  irrapxlem4  38824  pell14qrss1234  38855  pell1qrss14  38867  monotoddzz  38942  rmxypos  38946  ltrmynn0  38947  ltrmxnn0  38948  lermxnn0  38949  rmxnn  38950  rmynn0  38956  jm2.17a  38959  jm2.17b  38960  rmygeid  38963  jm2.18  38987  jm2.19lem3  38990  jm2.19lem4  38991  jm2.22  38994  rmxdiophlem  39014  hbt  39132  proot1ex  39203  fincygsubgodd  40053  fzisoeu  41002  stirlinglem5  41800  elfzlble  42932  subsubelfzo0  42938  2ffzoeq  42940  fargshiftfo  42980  fmtnof1  43071  fmtnorec1  43073  goldbachthlem1  43081  odz2prm2pw  43099  flsqrt  43130  lighneallem4  43149  nn0eo  43962  nn0ofldiv2  43966  flnn0div2ge  43967  fllog2  44002  blenpw2  44012  blennngt2o2  44026  nn0digval  44034  dignn0fr  44035  digexp  44041  0dig2nn0e  44046  0dig2nn0o  44047  dig2bits  44048  dignn0flhalflem2  44050  dignn0ehalf  44051  dignn0flhalf  44052  nn0sumshdiglemB  44054