Theorem nn0z 11400

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

Syntax hints:   → wi 4   ∈ wcel 1990  ℕ₀cn0 11292  ℤcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378

This theorem is referenced by:  nn0negz  11415  nn0ltp1le  11435  nn0leltp1  11436  nn0ltlem1  11437  nn0lt2  11440  nn0le2is012  11441  nn0lem1lt  11442  fnn0ind  11476  nn0pzuz  11745  nn0ge2m1nnALT  11782  fz1n  12359  ige2m1fz  12430  elfz2nn0  12431  fznn0  12432  elfz0add  12438  fzctr  12451  difelfzle  12452  fzofzim  12514  fzo1fzo0n0  12518  elincfzoext  12525  elfzodifsumelfzo  12533  fz0add1fz1  12537  zpnn0elfzo  12540  fzossfzop1  12545  ubmelm1fzo  12564  elfznelfzo  12573  flmulnn0  12628  quoremnn0  12655  zmodidfzoimp  12700  modmuladdnn0  12714  modfzo0difsn  12742  expdiv  12911  faclbnd3  13079  bccmpl  13096  bcnp1n  13101  bcval5  13105  bcn2  13106  bcp1m1  13107  hashge2el2difr  13263  fi1uzind  13279  fi1uzindOLD  13285  wrdred1  13349  wrdred1hash  13350  ccatalpha  13375  swrdfv2  13446  swrdsb0eq  13447  swrdsbslen  13448  swrdspsleq  13449  swrdlsw  13452  2swrd1eqwrdeq  13454  swrdccatin12lem1  13484  swrdccatin12lem3  13490  swrdccat3  13492  swrdccat  13493  revlen  13511  repswswrd  13531  repswccat  13532  cshwidxmodr  13550  cshf1  13556  2cshw  13559  cshweqrep  13567  cshwcshid  13573  cshwcsh2id  13574  cats1fv  13604  swrd2lsw  13695  2swrd2eqwrdeq  13696  isercoll  14398  iseraltlem2  14413  bcxmas  14567  geo2sum2  14605  geomulcvg  14607  risefacval2  14741  fallfacval2  14742  zrisefaccl  14751  zfallfaccl  14752  fallrisefac  14756  bpolylem  14779  fsumkthpow  14787  esum  14811  ege2le3  14820  eftlcl  14837  reeftlcl  14838  eftlub  14839  effsumlt  14841  eirrlem  14932  dvds1  15041  dvdsext  15043  addmodlteqALT  15047  oddnn02np1  15072  oddge22np1  15073  nn0ehalf  15095  nn0o1gt2  15097  nno  15098  nn0o  15099  nn0oddm1d2  15101  divalglem4  15119  divalglem5  15120  modremain  15132  bitsinv1  15164  nn0gcdid0  15242  nn0seqcvgd  15283  algcvga  15292  eucalgf  15296  nonsq  15467  odzdvds  15500  coprimeprodsq  15513  coprimeprodsq2  15514  oddprm  15515  iserodd  15540  pcexp  15564  pcidlem  15576  pc11  15584  dvdsprmpweqle  15590  difsqpwdvds  15591  pcfac  15603  prmunb  15618  hashbc2  15710  cshwshashlem2  15803  mulgaddcom  17564  mulginvcom  17565  mulgz  17568  mulgdirlem  17572  mulgass  17579  mndodcongi  17962  oddvdsnn0  17963  odeq  17969  odmulg  17973  efgsdmi  18145  cyggex2  18298  mulgass2  18601  chrrhm  19879  zncrng  19893  znzrh2  19894  zndvds  19898  znchr  19911  znunit  19912  chfacfisf  20659  chfacfisfcpmat  20660  chfacfscmulfsupp  20664  chfacfpmmulfsupp  20668  clmmulg  22901  itgcnlem  23556  degltlem1  23832  plyco0  23948  dgreq0  24021  plydivex  24052  aannenlem1  24083  abelthlem1  24185  abelthlem3  24187  abelthlem8  24193  abelthlem9  24194  advlogexp  24401  cxpexp  24414  leibpilem1  24667  leibpi  24669  log2cnv  24671  log2tlbnd  24672  basellem2  24808  sgmnncl  24873  chpp1  24881  bcmono  25002  bcmax  25003  bcp1ctr  25004  lgsneg1  25047  lgsdirnn0  25069  lgsdinn0  25070  2lgslem1c  25118  2lgslem3a1  25125  2lgslem3b1  25126  2lgslem3c1  25127  2lgsoddprmlem2  25134  dchrisumlem1  25178  qabvle  25314  ostth2lem2  25323  tgldimor  25397  upgrewlkle2  26502  wlkv0  26547  redwlk  26569  pthdadjvtx  26626  pthdlem1  26662  wlkiswwlks2lem3  26757  wwlksm1edg  26767  wwlksnred  26787  wwlksnext  26788  clwlkclwwlklem2a1  26893  clwlkclwwlklem2a2  26894  clwlkclwwlklem2fv1  26896  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwlkclwwlk  26903  clwwisshclwwslem  26927  clwlksfclwwlk2wrd  26958  clwlksfclwwlk  26962  clwlksf1clwwlklem3  26967  eucrctshift  27103  eucrct2eupth1  27104  eucrct2eupth  27105  numclwwlk5lem  27245  numclwwlk5  27246  numclwwlk7  27249  frgrreggt1  27251  nndiffz1  29548  xrge0mulgnn0  29689  hashf2  30146  signsvtn0  30647  fz0n  31616  bcneg1  31622  bccolsum  31625  faclimlem3  31631  faclim  31632  iprodfac  31633  poimirlem28  33437  mblfinlem1  33446  mblfinlem2  33447  nacsfix  37275  fzsplit1nn0  37317  eldioph2lem1  37323  fz1eqin  37332  diophin  37336  eq0rabdioph  37340  rexrabdioph  37358  rexzrexnn0  37368  irrapxlem4  37389  pell14qrss1234  37420  pell1qrss14  37432  monotoddzz  37508  rmxypos  37514  ltrmynn0  37515  ltrmxnn0  37516  lermxnn0  37517  rmxnn  37518  rmynn0  37524  jm2.17a  37527  jm2.17b  37528  rmygeid  37531  jm2.18  37555  jm2.19lem3  37558  jm2.19lem4  37559  jm2.22  37562  rmxdiophlem  37582  hbt  37700  proot1ex  37779  fzisoeu  39514  stirlinglem5  40295  elfzlble  41330  subsubelfzo0  41336  2ffzoeq  41338  fargshiftfo  41378  pfxnd  41395  pfxccat3  41426  pfxccat3a  41429  fmtnof1  41447  fmtnorec1  41449  goldbachthlem1  41457  odz2prm2pw  41475  flsqrt  41508  lighneallem4  41527  nn0eo  42322  nn0ofldiv2  42326  flnn0div2ge  42327  fllog2  42362  blenpw2  42372  blennngt2o2  42386  nn0digval  42394  dignn0fr  42395  digexp  42401  0dig2nn0e  42406  0dig2nn0o  42407  dig2bits  42408  dignn0flhalflem2  42410  dignn0ehalf  42411  dignn0flhalf  42412  nn0sumshdiglemB  42414