Theorem nn0z 12720

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℕ₀cn0 12609  ℤcz 12696

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-i2m1 11271  ax-1ne0 11272  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-neg 11547  df-nn 12339  df-n0 12610  df-z 12697

This theorem is used by:  nn0negz  12737  0nn0m1nnn0  12756  nn0ltp1le  12760  nn0leltp1  12761  nn0ltlem1  12762  nn0lt2  12765  nn0le2is012  12766  nn0lem1lt  12767  fnn0ind  12801  nn0pzuz  13035  nn0ge2m1nnALT  13072  fz1n  13678  ige2m1fz  13754  elfz2nn0  13755  fznn0  13756  elfz0add  13763  fzctr  13777  difelfzle  13778  fzoun  13834  fzofzim  13847  fzo1fzo0n0  13853  elincfzoext  13861  elfzodifsumelfzo  13869  fz0add1fz1  13873  zpnn0elfzo  13876  fzossfzop1  13881  ubmelm1fzo  13901  elfznelfzo  13911  flmulnn0  13970  quoremnn0  13999  zmodidfzoimp  14044  modmuladdnn0  14061  modfzo0difsn  14089  expdiv  14259  expnngt1  14388  faclbnd3  14439  bccmpl  14456  bcnp1n  14461  bcval5  14465  bcn2  14466  bcp1m1  14467  hashge2el2difr  14629  fi1uzind  14655  wrdred1  14708  wrdred1hash  14709  ccatalpha  14743  swrdnd0  14811  swrdfv2  14815  swrdsb0eq  14817  swrdsbslen  14818  swrdspsleq  14819  swrdlsw  14821  pfxnd  14841  pfxccatin12lem4  14879  pfxccatin12lem3  14885  pfxccat3  14887  swrdccat  14888  pfxccat3a  14891  revlen  14915  repswswrd  14939  repswccat  14941  cshwidxmodr  14959  cshf1  14965  2cshw  14968  cshweqrep  14976  cshwcshid  14982  cshwcsh2id  14983  cats1fv  15014  swrd2lsw  15110  2swrd2eqwrdeq  15111  isercoll  15840  iseraltlem2  15855  bcxmas  16009  geo2sum2  16048  geomulcvg  16050  risefacval2  16182  fallfacval2  16183  zrisefaccl  16192  zfallfaccl  16193  fallrisefac  16197  bpolylem  16219  fsumkthpow  16227  esum  16251  ege2le3  16261  eftlcl  16280  reeftlcl  16281  eftlub  16282  effsumlt  16284  eirrlem  16377  dvds1  16494  dvdsext  16496  addmodlteqALT  16500  oddnn02np1  16523  oddge22np1  16524  nn0ehalf  16553  nn0o1gt2  16556  nno  16557  nn0o  16558  nn0oddm1d2  16560  divalglem4  16571  divalglem5  16572  modremain  16583  bitsinv1  16617  nn0gcdid0  16698  gcdnn0id  16705  nn0seqcvgd  16750  algcvga  16759  eucalgf  16763  nonsq  16940  numdenexp  16942  odzdvds  16978  coprimeprodsq  16991  coprimeprodsq2  16992  oddprm  16993  iserodd  17018  pcexp  17042  pcidlem  17055  pc11  17063  dvdsprmpweqle  17069  difsqpwdvds  17070  pcfac  17082  prmunb  17097  hashbc2  17189  cshwshashlem2  17279  chnccat  18805  smndex1ibas  19101  smndex1iidm  19102  smndex2dnrinv  19119  smndex2dlinvh  19121  mulgaddcom  19313  mulginvcom  19314  mulgz  19317  mulgdirlem  19320  mulgass  19326  mndodcongi  19762  oddvdsnn0  19763  odeq  19769  odmulg  19775  efgsdmi  19951  cyggex2  20116  fincygsubgodd  20333  mulgass2  20545  chrrhm  21842  zncrng  21855  znzrh2  21856  zndvds  21860  znchr  21873  znunit  21874  chfacfisf  23177  chfacfisfcpmat  23178  chfacfscmulfsupp  23182  chfacfpmmulfsupp  23186  clmmulg  25427  itgcnlem  26115  degltlem1  26395  plyco0  26515  dgreq0  26589  plydivex  26623  aannenlem1  26660  abelthlem1  26763  abelthlem3  26765  abelthlem8  26771  abelthlem9  26772  advlogexp  26988  cxpexp  27001  leibpi  27275  log2cnv  27277  log2tlbnd  27278  basellem2  27414  sgmnncl  27479  chpp1  27487  bcmono  27609  bcmax  27610  bcp1ctr  27611  lgsneg1  27654  lgsdirnn0  27676  lgsdinn0  27677  2lgslem1c  27725  2lgslem3a1  27732  2lgslem3b1  27733  2lgslem3c1  27734  2lgsoddprmlem2  27741  2sq2  27765  2sqreultlem  27779  dchrisumlem1  27821  qabvle  27957  ostth2lem2  27966  fltoprmlem2  27999  tgldimor  28970  upgrewlkle2  30192  wlkv0  30235  redwlk  30256  pthdadjvtx  30318  pthhashvtx  30320  pthdlem1  30357  wwlknvtx  30439  wlkiswwlks2lem3  30465  wwlksm1edg  30475  wwlksnred  30486  wwlksnext  30487  clwlkclwwlklem2a1  30588  clwlkclwwlklem2a2  30589  clwlkclwwlklem2fv1  30591  clwlkclwwlklem2fv2  30592  clwlkclwwlklem2a4  30593  clwlkclwwlklem2a  30594  clwlkclwwlklem2  30596  clwlkclwwlk  30598  clwwisshclwwslem  30610  eucrctshift  30849  eucrct2eupth1  30850  eucrct2eupth  30851  numclwwlk5lem  30993  numclwwlk5  30994  numclwwlk7  30997  frgrreggt1  30999  nndiffz1  33424  nn0diffz0  33432  xrge0mulgnn0  33622  hashf2  34762  signsvtn0  35245  nn0ltp1ne  35978  fz0n  36588  bcneg1  36593  bccolsum  36596  faclimlem3  36602  faclim  36603  iprodfac  36604  poimirlem28  38659  mblfinlem1  38668  mblfinlem2  38669  lcmineqlem2  43173  sticksstones22  43311  negexpidd  43785  nacsfix  43816  fzsplit1nn0  43858  eldioph2lem1  43864  fz1eqin  43873  diophin  43876  eq0rabdioph  43880  rexrabdioph  43894  rexzrexnn0  43904  irrapxlem4  43925  pell14qrss1234  43956  pell1qrss14  43968  monotoddzz  44043  rmxypos  44047  ltrmynn0  44048  ltrmxnn0  44049  lermxnn0  44050  rmxnn  44051  rmynn0  44057  jm2.17a  44060  jm2.17b  44061  rmygeid  44064  jm2.18  44088  jm2.19lem3  44091  jm2.19lem4  44092  jm2.22  44095  rmxdiophlem  44115  hbt  44225  proot1ex  44291  k0004ss3  45246  fzisoeu  46409  stirlinglem5  47181  elfzlble  48483  subsubelfzo0  48490  2ffzoeq  48491  addmodne  48513  fargshiftfo  48617  fmtnof1  48713  fmtnorec1  48715  goldbachthlem1  48723  odz2prm2pw  48741  flsqrt  48771  lighneallem4  48788  nn0eo  49733  nn0ofldiv2  49737  flnn0div2ge  49738  fllog2  49773  blenpw2  49783  blennngt2o2  49797  nn0digval  49805  dignn0fr  49806  digexp  49812  0dig2nn0e  49817  0dig2nn0o  49818  dig2bits  49819  dignn0flhalflem2  49821  dignn0ehalf  49822  dignn0flhalf  49823  nn0sumshdiglemB  49825