Theorem nn0z 12643

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℕ₀cn0 12532  ℤcz 12619

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-i2m1 11196  ax-1ne0 11197  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-neg 11472  df-nn 12262  df-n0 12533  df-z 12620

This theorem is used by:  nn0negz  12660  0nn0m1nnn0  12679  nn0ltp1le  12683  nn0leltp1  12684  nn0ltlem1  12685  nn0lt2  12688  nn0le2is012  12689  nn0lem1lt  12690  fnn0ind  12724  nn0pzuz  12958  nn0ge2m1nnALT  12995  fz1n  13600  ige2m1fz  13676  elfz2nn0  13677  fznn0  13678  elfz0add  13685  fzctr  13699  difelfzle  13700  fzoun  13756  fzofzim  13769  fzo1fzo0n0  13775  elincfzoext  13783  elfzodifsumelfzo  13791  fz0add1fz1  13795  zpnn0elfzo  13798  fzossfzop1  13803  ubmelm1fzo  13823  elfznelfzo  13833  flmulnn0  13892  quoremnn0  13921  zmodidfzoimp  13966  modmuladdnn0  13983  modfzo0difsn  14011  expdiv  14181  expnngt1  14309  faclbnd3  14360  bccmpl  14377  bcnp1n  14382  bcval5  14386  bcn2  14387  bcp1m1  14388  hashge2el2difr  14550  fi1uzind  14576  wrdred1  14629  wrdred1hash  14630  ccatalpha  14664  swrdnd0  14731  swrdfv2  14735  swrdsb0eq  14737  swrdsbslen  14738  swrdspsleq  14739  swrdlsw  14741  pfxnd  14761  pfxccatin12lem4  14799  pfxccatin12lem3  14805  pfxccat3  14807  swrdccat  14808  pfxccat3a  14811  revlen  14835  repswswrd  14859  repswccat  14861  cshwidxmodr  14879  cshf1  14885  2cshw  14888  cshweqrep  14896  cshwcshid  14902  cshwcsh2id  14903  cats1fv  14934  swrd2lsw  15029  2swrd2eqwrdeq  15030  isercoll  15759  iseraltlem2  15774  bcxmas  15928  geo2sum2  15967  geomulcvg  15969  risefacval2  16103  fallfacval2  16104  zrisefaccl  16113  zfallfaccl  16114  fallrisefac  16118  bpolylem  16140  fsumkthpow  16148  esum  16172  ege2le3  16182  eftlcl  16201  reeftlcl  16202  eftlub  16203  effsumlt  16205  eirrlem  16298  dvds1  16415  dvdsext  16417  addmodlteqALT  16421  oddnn02np1  16444  oddge22np1  16445  nn0ehalf  16474  nn0o1gt2  16477  nno  16478  nn0o  16479  nn0oddm1d2  16481  divalglem4  16492  divalglem5  16493  modremain  16504  bitsinv1  16538  nn0gcdid0  16617  nn0seqcvgd  16666  algcvga  16675  eucalgf  16679  nonsq  16856  numdenexp  16857  odzdvds  16893  coprimeprodsq  16906  coprimeprodsq2  16907  oddprm  16908  iserodd  16933  pcexp  16957  pcidlem  16970  pc11  16978  dvdsprmpweqle  16984  difsqpwdvds  16985  pcfac  16997  prmunb  17012  hashbc2  17104  cshwshashlem2  17194  chnccat  18720  smndex1ibas  19015  smndex1iidm  19016  smndex2dnrinv  19033  smndex2dlinvh  19035  mulgaddcom  19227  mulginvcom  19228  mulgz  19231  mulgdirlem  19234  mulgass  19240  mndodcongi  19676  oddvdsnn0  19677  odeq  19683  odmulg  19689  efgsdmi  19865  cyggex2  20030  fincygsubgodd  20247  mulgass2  20457  chrrhm  21750  zncrng  21763  znzrh2  21764  zndvds  21768  znchr  21781  znunit  21782  chfacfisf  23085  chfacfisfcpmat  23086  chfacfscmulfsupp  23090  chfacfpmmulfsupp  23094  clmmulg  25335  itgcnlem  26024  degltlem1  26304  plyco0  26424  dgreq0  26498  plydivex  26534  aannenlem1  26571  abelthlem1  26674  abelthlem3  26676  abelthlem8  26682  abelthlem9  26683  advlogexp  26900  cxpexp  26913  leibpi  27187  log2cnv  27189  log2tlbnd  27190  basellem2  27326  sgmnncl  27391  chpp1  27399  bcmono  27521  bcmax  27522  bcp1ctr  27523  lgsneg1  27566  lgsdirnn0  27588  lgsdinn0  27589  2lgslem1c  27637  2lgslem3a1  27644  2lgslem3b1  27645  2lgslem3c1  27646  2lgsoddprmlem2  27653  2sq2  27677  2sqreultlem  27691  dchrisumlem1  27733  qabvle  27869  ostth2lem2  27878  tgldimor  28852  upgrewlkle2  30074  wlkv0  30117  redwlk  30138  pthdadjvtx  30200  pthhashvtx  30202  pthdlem1  30239  wwlknvtx  30321  wlkiswwlks2lem3  30347  wwlksm1edg  30357  wwlksnred  30368  wwlksnext  30369  clwlkclwwlklem2a1  30470  clwlkclwwlklem2a2  30471  clwlkclwwlklem2fv1  30473  clwlkclwwlklem2fv2  30474  clwlkclwwlklem2a4  30475  clwlkclwwlklem2a  30476  clwlkclwwlklem2  30478  clwlkclwwlk  30480  clwwisshclwwslem  30492  eucrctshift  30731  eucrct2eupth1  30732  eucrct2eupth  30733  numclwwlk5lem  30875  numclwwlk5  30876  numclwwlk7  30879  frgrreggt1  30881  nndiffz1  33265  nn0diffz0  33273  xrge0mulgnn0  33463  hashf2  34602  signsvtn0  35086  nn0ltp1ne  35724  fz0n  36318  bcneg1  36323  bccolsum  36326  faclimlem3  36332  faclim  36333  iprodfac  36334  poimirlem28  38405  mblfinlem1  38414  mblfinlem2  38415  lcmineqlem2  42904  sticksstones22  43042  gcdnn0id  43212  negexpidd  43535  nacsfix  43565  fzsplit1nn0  43607  eldioph2lem1  43613  fz1eqin  43622  diophin  43625  eq0rabdioph  43629  rexrabdioph  43643  rexzrexnn0  43653  irrapxlem4  43674  pell14qrss1234  43705  pell1qrss14  43717  monotoddzz  43792  rmxypos  43796  ltrmynn0  43797  ltrmxnn0  43798  lermxnn0  43799  rmxnn  43800  rmynn0  43806  jm2.17a  43809  jm2.17b  43810  rmygeid  43813  jm2.18  43837  jm2.19lem3  43840  jm2.19lem4  43841  jm2.22  43844  rmxdiophlem  43864  hbt  43979  proot1ex  44045  fzisoeu  46141  stirlinglem5  46914  elfzlble  48216  subsubelfzo0  48223  2ffzoeq  48224  addmodne  48246  fargshiftfo  48350  fmtnof1  48446  fmtnorec1  48448  goldbachthlem1  48456  odz2prm2pw  48474  flsqrt  48504  lighneallem4  48521  nn0eo  49466  nn0ofldiv2  49470  flnn0div2ge  49471  fllog2  49506  blenpw2  49516  blennngt2o2  49530  nn0digval  49538  dignn0fr  49539  digexp  49545  0dig2nn0e  49550  0dig2nn0o  49551  dig2bits  49552  dignn0flhalflem2  49554  dignn0ehalf  49555  dignn0flhalf  49556  nn0sumshdiglemB  49558