Theorem nn0z 9673

Description: A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0z	|- ( N e. NN0 -> N e. ZZ )

Proof of Theorem nn0z

Step	Hyp	Ref	Expression
1		nn0ssz 9671	. 2 |- NN0 C_ ZZ
2	1	sseli 3244	1 |- ( N e. NN0 -> N e. ZZ )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   NN0cn0 9574   ZZcz 9653

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 8276  ax-resscn 8277  ax-1cn 8278  ax-1re 8279  ax-icn 8280  ax-addcl 8281  ax-addrcl 8282  ax-mulcl 8283  ax-addcom 8285  ax-addass 8287  ax-distr 8289  ax-i2m1 8290  ax-0lt1 8291  ax-0id 8293  ax-rnegex 8294  ax-cnre 8296  ax-pre-ltirr 8297  ax-pre-ltwlin 8298  ax-pre-lttrn 8299  ax-pre-ltadd 8301

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 8368  df-mnf 8369  df-xr 8370  df-ltxr 8371  df-le 8372  df-sub 8506  df-neg 8507  df-inn 9314  df-n0 9575  df-z 9654

This theorem is used by:  nn0negz  9687  nn0ltp1le  9716  nn0leltp1  9717  nn0ltlem1  9718  nn0sub  9720  nn0n0n1ge2b  9734  nn0lt10b  9735  nn0lt2  9736  nn0le2is012  9737  nn0lem1lt  9738  fcdmnn0fsuppfi  9743  fnn0ind  9772  nn0pzuz  10002  nn01to3  10032  nn0ge2m1nnALT  10033  fz1n  10464  ige2m1fz  10533  elfz2nn0  10535  fznn0  10536  elfz0add  10543  fzctr  10556  difelfzle  10557  fzoun  10606  fzo1fzo0n0  10611  fzofzim  10616  elincfzoext  10627  elfzodifsumelfzo  10635  zpnn0elfzo  10641  fzossfzop1  10646  ubmelm1fzo  10660  adddivflid  10747  fldivnn0  10750  divfl0  10751  flqmulnn0  10754  fldivnn0le  10758  zmodidfzoimp  10811  modqmuladdnn0  10825  modifeq2int  10843  modfzo0difsn  10852  uzennn  10893  expdivap  11047  nn0sqdc  11167  faclbnd3  11202  bccmpl  11213  bcnp1n  11218  bcn2  11223  bcp1m1  11224  iswrd  11327  wrdval  11328  wrdexg  11336  ffz0iswrdnn0  11352  wrdnval  11356  wrdred1  11368  wrdred1hash  11369  ccatalpha  11402  swrdfv2  11456  swrdsb0eq  11458  swrdsbslen  11459  swrdspsleq  11460  swrdlsw  11462  pfx0g  11469  fnpfx  11470  pfxclg  11471  pfxnd  11482  pfxwrdsymbg  11483  pfxccatin12lem4  11519  pfxccatin12lem3  11525  pfxccat3  11527  swrdccat  11528  pfxccat3a  11531  cats1fvd  11559  nn0maxcl  12013  modfsummodlemstep  12248  bcxmas  12280  geo2sum2  12306  mertenslemi1  12326  mertensabs  12328  esum  12453  efcvgfsum  12458  ege2le3  12462  eftlcl  12479  reeftlcl  12480  eftlub  12481  effsumlt  12483  eirraplem  12568  dvds1  12644  dvdsext  12646  addmodlteqALT  12650  3dvds  12655  oddnn02np1  12671  oddge22np1  12672  nn0ehalf  12694  nn0o1gt2  12696  nno  12697  nn0o  12698  nn0oddm1d2  12700  modremain  12720  bitsmod  12747  bitsinv1  12753  gcdn0gt0  12779  nn0gcdid0  12782  bezoutlemmain  12799  nn0seqcvgd  12843  algcvgblem  12851  algcvga  12853  eucalgf  12857  prmndvdsfaclt  12959  nn0sqrtelqelz  13010  nonsq  13011  sqrtrirr  13013  crth  13030  odzdvds  13052  coprimeprodsq  13064  coprimeprodsq2  13065  oddprm  13066  pcexp  13116  pcdvdsb  13127  pc11  13138  dvdsprmpweqle  13144  difsqpwdvds  13145  pcfac  13157  prmunb  13169  4sqexercise1  13205  4sqexercise2  13206  4sqlemsdc  13207  modxai  13223  mulgaddcom  14007  mulginvcom  14008  mulgz  14011  mulgdirlem  14014  mulgass  14020  mulgass2  14469  zncrng  15088  znzrh2  15089  zndvds  15092  znf1o  15094  znunit  15102  elply2  15978  elplyd  15984  dvply2g  16009  log2tlbndlog2  16237  birthdaylem1g  16242  birthdaylem3  16244  sgmnncl  16274  0sgmppw  16304  bcmono  16321  bcmax  16322  bcp1ctr  16323  lgsneg1  16366  lgsdirnn0  16388  lgsdinn0  16389  2lgslem1c  16431  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgsoddprmlem2  16447  wlkv0  16832