Theorem nn0z 9674

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℕ₀cn0 9575  ℤcz 9654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-cnex 8277  ax-resscn 8278  ax-1cn 8279  ax-1re 8280  ax-icn 8281  ax-addcl 8282  ax-addrcl 8283  ax-mulcl 8284  ax-addcom 8286  ax-addass 8288  ax-distr 8290  ax-i2m1 8291  ax-0lt1 8292  ax-0id 8294  ax-rnegex 8295  ax-cnre 8297  ax-pre-ltirr 8298  ax-pre-ltwlin 8299  ax-pre-lttrn 8300  ax-pre-ltadd 8302

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4132  df-opab 4194  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-pnf 8369  df-mnf 8370  df-xr 8371  df-ltxr 8372  df-le 8373  df-sub 8507  df-neg 8508  df-inn 9315  df-n0 9576  df-z 9655

This theorem is used by:  nn0negz  9688  nn0ltp1le  9717  nn0leltp1  9718  nn0ltlem1  9719  nn0sub  9721  nn0n0n1ge2b  9735  nn0lt10b  9736  nn0lt2  9737  nn0le2is012  9738  nn0lem1lt  9739  fcdmnn0fsuppfi  9744  fnn0ind  9773  nn0pzuz  10003  nn01to3  10033  nn0ge2m1nnALT  10034  fz1n  10465  ige2m1fz  10534  elfz2nn0  10536  fznn0  10537  elfz0add  10544  fzctr  10557  difelfzle  10558  fzoun  10607  fzo1fzo0n0  10612  fzofzim  10617  elincfzoext  10628  elfzodifsumelfzo  10636  zpnn0elfzo  10642  fzossfzop1  10647  ubmelm1fzo  10661  adddivflid  10748  fldivnn0  10751  divfl0  10752  flqmulnn0  10755  fldivnn0le  10759  zmodidfzoimp  10812  modqmuladdnn0  10826  modifeq2int  10844  modfzo0difsn  10853  uzennn  10894  expdivap  11048  nn0sqdc  11168  faclbnd3  11203  bccmpl  11214  bcnp1n  11219  bcn2  11224  bcp1m1  11225  iswrd  11328  wrdval  11329  wrdexg  11337  ffz0iswrdnn0  11353  wrdnval  11357  wrdred1  11369  wrdred1hash  11370  ccatalpha  11403  swrdfv2  11457  swrdsb0eq  11459  swrdsbslen  11460  swrdspsleq  11461  swrdlsw  11463  pfx0g  11470  fnpfx  11471  pfxclg  11472  pfxnd  11483  pfxwrdsymbg  11484  pfxccatin12lem4  11520  pfxccatin12lem3  11526  pfxccat3  11528  swrdccat  11529  pfxccat3a  11532  cats1fvd  11560  nn0maxcl  12014  modfsummodlemstep  12249  bcxmas  12281  geo2sum2  12307  mertenslemi1  12327  mertensabs  12329  esum  12454  efcvgfsum  12459  ege2le3  12463  eftlcl  12480  reeftlcl  12481  eftlub  12482  effsumlt  12484  eirraplem  12569  dvds1  12645  dvdsext  12647  addmodlteqALT  12651  3dvds  12656  oddnn02np1  12672  oddge22np1  12673  nn0ehalf  12695  nn0o1gt2  12697  nno  12698  nn0o  12699  nn0oddm1d2  12701  modremain  12721  bitsmod  12748  bitsinv1  12754  gcdn0gt0  12780  nn0gcdid0  12783  bezoutlemmain  12800  nn0seqcvgd  12844  algcvgblem  12852  algcvga  12854  eucalgf  12858  prmndvdsfaclt  12960  nn0sqrtelqelz  13011  nonsq  13012  sqrtrirr  13014  crth  13031  odzdvds  13053  coprimeprodsq  13065  coprimeprodsq2  13066  oddprm  13067  pcexp  13117  pcdvdsb  13128  pc11  13139  dvdsprmpweqle  13145  difsqpwdvds  13146  pcfac  13158  prmunb  13170  4sqexercise1  13206  4sqexercise2  13207  4sqlemsdc  13208  modxai  13224  mulgaddcom  14008  mulginvcom  14009  mulgz  14012  mulgdirlem  14015  mulgass  14021  mulgass2  14470  zncrng  15089  znzrh2  15090  zndvds  15093  znf1o  15095  znunit  15103  elply2  15994  elplyd  16000  dvply2g  16025  log2tlbndlog2  16253  birthdaylem1g  16258  birthdaylem3  16260  sgmnncl  16290  0sgmppw  16320  bcmono  16337  bcmax  16338  bcp1ctr  16339  lgsneg1  16382  lgsdirnn0  16404  lgsdinn0  16405  2lgslem1c  16447  2lgslem3a1  16454  2lgslem3b1  16455  2lgslem3c1  16456  2lgsoddprmlem2  16463  wlkv0  16848