Theorem nn0z 9303

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

Syntax hints:   -> wi 4   e. wcel 2160   NN0cn0 9206   ZZcz 9283

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-cnex 7932  ax-resscn 7933  ax-1cn 7934  ax-1re 7935  ax-icn 7936  ax-addcl 7937  ax-addrcl 7938  ax-mulcl 7939  ax-addcom 7941  ax-addass 7943  ax-distr 7945  ax-i2m1 7946  ax-0lt1 7947  ax-0id 7949  ax-rnegex 7950  ax-cnre 7952  ax-pre-ltirr 7953  ax-pre-ltwlin 7954  ax-pre-lttrn 7955  ax-pre-ltadd 7957

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-opab 4080  df-id 4311  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-iota 5196  df-fun 5237  df-fv 5243  df-riota 5852  df-ov 5899  df-oprab 5900  df-mpo 5901  df-pnf 8024  df-mnf 8025  df-xr 8026  df-ltxr 8027  df-le 8028  df-sub 8160  df-neg 8161  df-inn 8950  df-n0 9207  df-z 9284

This theorem is referenced by:  nn0negz  9317  nn0ltp1le  9345  nn0leltp1  9346  nn0ltlem1  9347  nn0sub  9349  nn0n0n1ge2b  9362  nn0lt10b  9363  nn0lt2  9364  nn0le2is012  9365  nn0lem1lt  9366  fnn0ind  9399  nn0pzuz  9617  nn01to3  9647  nn0ge2m1nnALT  9648  fz1n  10074  ige2m1fz  10140  elfz2nn0  10142  fznn0  10143  elfz0add  10150  fzctr  10163  difelfzle  10164  fzo1fzo0n0  10213  fzofzim  10218  elfzodifsumelfzo  10231  zpnn0elfzo  10237  fzossfzop1  10242  ubmelm1fzo  10256  adddivflid  10323  fldivnn0  10326  divfl0  10327  flqmulnn0  10330  fldivnn0le  10334  zmodidfzoimp  10385  modqmuladdnn0  10399  modifeq2int  10417  modfzo0difsn  10426  uzennn  10467  expdivap  10602  faclbnd3  10755  bccmpl  10766  bcnp1n  10771  bcn2  10776  bcp1m1  10777  modfsummodlemstep  11497  bcxmas  11529  geo2sum2  11555  mertenslemi1  11575  mertensabs  11577  esum  11702  efcvgfsum  11707  ege2le3  11711  eftlcl  11728  reeftlcl  11729  eftlub  11730  effsumlt  11732  eirraplem  11816  dvds1  11891  dvdsext  11893  addmodlteqALT  11897  oddnn02np1  11917  oddge22np1  11918  nn0ehalf  11940  nn0o1gt2  11942  nno  11943  nn0o  11944  nn0oddm1d2  11946  modremain  11966  gcdn0gt0  12011  nn0gcdid0  12014  bezoutlemmain  12031  nn0seqcvgd  12073  algcvgblem  12081  algcvga  12083  eucalgf  12087  prmndvdsfaclt  12188  nn0sqrtelqelz  12238  nonsq  12239  crth  12256  odzdvds  12277  coprimeprodsq  12289  coprimeprodsq2  12290  oddprm  12291  pcexp  12341  pcdvdsb  12352  pc11  12363  dvdsprmpweqle  12369  difsqpwdvds  12370  pcfac  12382  prmunb  12394  4sqexercise1  12430  4sqexercise2  12431  4sqlemsdc  12432  mulgaddcom  13086  mulginvcom  13087  mulgz  13090  mulgdirlem  13093  mulgass  13099  mulgass2  13410  zncrng  13940  lgsneg1  14884  lgsdirnn0  14906  lgsdinn0  14907  2lgsoddprmlem2  14912