Theorem nn0z 9489

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 9487	. 2 |- NN0 C_ ZZ
2	1	sseli 3221	1 |- ( N e. NN0 -> N e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2200   NN0cn0 9392   ZZcz 9469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8113  ax-resscn 8114  ax-1cn 8115  ax-1re 8116  ax-icn 8117  ax-addcl 8118  ax-addrcl 8119  ax-mulcl 8120  ax-addcom 8122  ax-addass 8124  ax-distr 8126  ax-i2m1 8127  ax-0lt1 8128  ax-0id 8130  ax-rnegex 8131  ax-cnre 8133  ax-pre-ltirr 8134  ax-pre-ltwlin 8135  ax-pre-lttrn 8136  ax-pre-ltadd 8138

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-pnf 8206  df-mnf 8207  df-xr 8208  df-ltxr 8209  df-le 8210  df-sub 8342  df-neg 8343  df-inn 9134  df-n0 9393  df-z 9470

This theorem is referenced by:  nn0negz  9503  nn0ltp1le  9532  nn0leltp1  9533  nn0ltlem1  9534  nn0sub  9536  nn0n0n1ge2b  9549  nn0lt10b  9550  nn0lt2  9551  nn0le2is012  9552  nn0lem1lt  9553  fnn0ind  9586  nn0pzuz  9811  nn01to3  9841  nn0ge2m1nnALT  9842  fz1n  10269  ige2m1fz  10335  elfz2nn0  10337  fznn0  10338  elfz0add  10345  fzctr  10358  difelfzle  10359  fzoun  10408  fzo1fzo0n0  10412  fzofzim  10417  elincfzoext  10428  elfzodifsumelfzo  10436  zpnn0elfzo  10442  fzossfzop1  10447  ubmelm1fzo  10461  adddivflid  10542  fldivnn0  10545  divfl0  10546  flqmulnn0  10549  fldivnn0le  10553  zmodidfzoimp  10606  modqmuladdnn0  10620  modifeq2int  10638  modfzo0difsn  10647  uzennn  10688  expdivap  10842  faclbnd3  10995  bccmpl  11006  bcnp1n  11011  bcn2  11016  bcp1m1  11017  iswrd  11105  wrdval  11106  wrdexg  11114  ffz0iswrdnn0  11130  wrdnval  11134  wrdred1  11146  wrdred1hash  11147  ccatalpha  11180  swrdfv2  11234  swrdsb0eq  11236  swrdsbslen  11237  swrdspsleq  11238  swrdlsw  11240  pfx0g  11247  fnpfx  11248  pfxclg  11249  pfxnd  11260  pfxwrdsymbg  11261  pfxccatin12lem4  11297  pfxccatin12lem3  11303  pfxccat3  11305  swrdccat  11306  pfxccat3a  11309  cats1fvd  11337  nn0maxcl  11776  modfsummodlemstep  12008  bcxmas  12040  geo2sum2  12066  mertenslemi1  12086  mertensabs  12088  esum  12213  efcvgfsum  12218  ege2le3  12222  eftlcl  12239  reeftlcl  12240  eftlub  12241  effsumlt  12243  eirraplem  12328  dvds1  12404  dvdsext  12406  addmodlteqALT  12410  3dvds  12415  oddnn02np1  12431  oddge22np1  12432  nn0ehalf  12454  nn0o1gt2  12456  nno  12457  nn0o  12458  nn0oddm1d2  12460  modremain  12480  bitsmod  12507  bitsinv1  12513  gcdn0gt0  12539  nn0gcdid0  12542  bezoutlemmain  12559  nn0seqcvgd  12603  algcvgblem  12611  algcvga  12613  eucalgf  12617  prmndvdsfaclt  12718  nn0sqrtelqelz  12768  nonsq  12769  crth  12786  odzdvds  12808  coprimeprodsq  12820  coprimeprodsq2  12821  oddprm  12822  pcexp  12872  pcdvdsb  12883  pc11  12894  dvdsprmpweqle  12900  difsqpwdvds  12901  pcfac  12913  prmunb  12925  4sqexercise1  12961  4sqexercise2  12962  4sqlemsdc  12963  modxai  12979  mulgaddcom  13723  mulginvcom  13724  mulgz  13727  mulgdirlem  13730  mulgass  13736  mulgass2  14061  zncrng  14649  znzrh2  14650  zndvds  14653  znf1o  14655  znunit  14663  elply2  15449  elplyd  15455  dvply2g  15480  sgmnncl  15702  0sgmppw  15707  lgsneg1  15744  lgsdirnn0  15766  lgsdinn0  15767  2lgslem1c  15809  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgsoddprmlem2  15825  wlkv0  16166