Theorem nn0z 9340

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

Syntax hints:   -> wi 4   e. wcel 2164   NN0cn0 9243   ZZcz 9320

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 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-addcom 7974  ax-addass 7976  ax-distr 7978  ax-i2m1 7979  ax-0lt1 7980  ax-0id 7982  ax-rnegex 7983  ax-cnre 7985  ax-pre-ltirr 7986  ax-pre-ltwlin 7987  ax-pre-lttrn 7988  ax-pre-ltadd 7990

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 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-int 3872  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263  df-riota 5874  df-ov 5922  df-oprab 5923  df-mpo 5924  df-pnf 8058  df-mnf 8059  df-xr 8060  df-ltxr 8061  df-le 8062  df-sub 8194  df-neg 8195  df-inn 8985  df-n0 9244  df-z 9321

This theorem is referenced by:  nn0negz  9354  nn0ltp1le  9382  nn0leltp1  9383  nn0ltlem1  9384  nn0sub  9386  nn0n0n1ge2b  9399  nn0lt10b  9400  nn0lt2  9401  nn0le2is012  9402  nn0lem1lt  9403  fnn0ind  9436  nn0pzuz  9655  nn01to3  9685  nn0ge2m1nnALT  9686  fz1n  10113  ige2m1fz  10179  elfz2nn0  10181  fznn0  10182  elfz0add  10189  fzctr  10202  difelfzle  10203  fzo1fzo0n0  10253  fzofzim  10258  elfzodifsumelfzo  10271  zpnn0elfzo  10277  fzossfzop1  10282  ubmelm1fzo  10296  adddivflid  10364  fldivnn0  10367  divfl0  10368  flqmulnn0  10371  fldivnn0le  10375  zmodidfzoimp  10428  modqmuladdnn0  10442  modifeq2int  10460  modfzo0difsn  10469  uzennn  10510  expdivap  10664  faclbnd3  10817  bccmpl  10828  bcnp1n  10833  bcn2  10838  bcp1m1  10839  iswrd  10919  wrdval  10920  wrdexg  10928  wrdnval  10947  wrdred1  10959  wrdred1hash  10960  modfsummodlemstep  11603  bcxmas  11635  geo2sum2  11661  mertenslemi1  11681  mertensabs  11683  esum  11808  efcvgfsum  11813  ege2le3  11817  eftlcl  11834  reeftlcl  11835  eftlub  11836  effsumlt  11838  eirraplem  11923  dvds1  11998  dvdsext  12000  addmodlteqALT  12004  oddnn02np1  12024  oddge22np1  12025  nn0ehalf  12047  nn0o1gt2  12049  nno  12050  nn0o  12051  nn0oddm1d2  12053  modremain  12073  gcdn0gt0  12118  nn0gcdid0  12121  bezoutlemmain  12138  nn0seqcvgd  12182  algcvgblem  12190  algcvga  12192  eucalgf  12196  prmndvdsfaclt  12297  nn0sqrtelqelz  12347  nonsq  12348  crth  12365  odzdvds  12386  coprimeprodsq  12398  coprimeprodsq2  12399  oddprm  12400  pcexp  12450  pcdvdsb  12461  pc11  12472  dvdsprmpweqle  12478  difsqpwdvds  12479  pcfac  12491  prmunb  12503  4sqexercise1  12539  4sqexercise2  12540  4sqlemsdc  12541  mulgaddcom  13219  mulginvcom  13220  mulgz  13223  mulgdirlem  13226  mulgass  13232  mulgass2  13557  zncrng  14144  znzrh2  14145  zndvds  14148  znf1o  14150  znunit  14158  elply2  14914  elplyd  14920  lgsneg1  15182  lgsdirnn0  15204  lgsdinn0  15205  2lgslem1c  15247  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgsoddprmlem2  15263