Theorem nn0z 9427

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

Syntax hints:   -> wi 4   e. wcel 2178   NN0cn0 9330   ZZcz 9407

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-un 4498  ax-setind 4603  ax-cnex 8051  ax-resscn 8052  ax-1cn 8053  ax-1re 8054  ax-icn 8055  ax-addcl 8056  ax-addrcl 8057  ax-mulcl 8058  ax-addcom 8060  ax-addass 8062  ax-distr 8064  ax-i2m1 8065  ax-0lt1 8066  ax-0id 8068  ax-rnegex 8069  ax-cnre 8071  ax-pre-ltirr 8072  ax-pre-ltwlin 8073  ax-pre-lttrn 8074  ax-pre-ltadd 8076

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-nel 2474  df-ral 2491  df-rex 2492  df-reu 2493  df-rab 2495  df-v 2778  df-sbc 3006  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-br 4060  df-opab 4122  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-iota 5251  df-fun 5292  df-fv 5298  df-riota 5922  df-ov 5970  df-oprab 5971  df-mpo 5972  df-pnf 8144  df-mnf 8145  df-xr 8146  df-ltxr 8147  df-le 8148  df-sub 8280  df-neg 8281  df-inn 9072  df-n0 9331  df-z 9408

This theorem is referenced by:  nn0negz  9441  nn0ltp1le  9470  nn0leltp1  9471  nn0ltlem1  9472  nn0sub  9474  nn0n0n1ge2b  9487  nn0lt10b  9488  nn0lt2  9489  nn0le2is012  9490  nn0lem1lt  9491  fnn0ind  9524  nn0pzuz  9743  nn01to3  9773  nn0ge2m1nnALT  9774  fz1n  10201  ige2m1fz  10267  elfz2nn0  10269  fznn0  10270  elfz0add  10277  fzctr  10290  difelfzle  10291  fzoun  10340  fzo1fzo0n0  10344  fzofzim  10349  elincfzoext  10359  elfzodifsumelfzo  10367  zpnn0elfzo  10373  fzossfzop1  10378  ubmelm1fzo  10392  adddivflid  10472  fldivnn0  10475  divfl0  10476  flqmulnn0  10479  fldivnn0le  10483  zmodidfzoimp  10536  modqmuladdnn0  10550  modifeq2int  10568  modfzo0difsn  10577  uzennn  10618  expdivap  10772  faclbnd3  10925  bccmpl  10936  bcnp1n  10941  bcn2  10946  bcp1m1  10947  iswrd  11033  wrdval  11034  wrdexg  11042  wrdnval  11061  wrdred1  11073  wrdred1hash  11074  swrdfv2  11154  swrdsb0eq  11156  swrdsbslen  11157  swrdspsleq  11158  swrdlsw  11160  pfx0g  11167  fnpfx  11168  pfxclg  11169  pfxnd  11180  pfxwrdsymbg  11181  pfxccatin12lem4  11217  pfxccatin12lem3  11223  pfxccat3  11225  swrdccat  11226  pfxccat3a  11229  nn0maxcl  11651  modfsummodlemstep  11883  bcxmas  11915  geo2sum2  11941  mertenslemi1  11961  mertensabs  11963  esum  12088  efcvgfsum  12093  ege2le3  12097  eftlcl  12114  reeftlcl  12115  eftlub  12116  effsumlt  12118  eirraplem  12203  dvds1  12279  dvdsext  12281  addmodlteqALT  12285  3dvds  12290  oddnn02np1  12306  oddge22np1  12307  nn0ehalf  12329  nn0o1gt2  12331  nno  12332  nn0o  12333  nn0oddm1d2  12335  modremain  12355  bitsmod  12382  bitsinv1  12388  gcdn0gt0  12414  nn0gcdid0  12417  bezoutlemmain  12434  nn0seqcvgd  12478  algcvgblem  12486  algcvga  12488  eucalgf  12492  prmndvdsfaclt  12593  nn0sqrtelqelz  12643  nonsq  12644  crth  12661  odzdvds  12683  coprimeprodsq  12695  coprimeprodsq2  12696  oddprm  12697  pcexp  12747  pcdvdsb  12758  pc11  12769  dvdsprmpweqle  12775  difsqpwdvds  12776  pcfac  12788  prmunb  12800  4sqexercise1  12836  4sqexercise2  12837  4sqlemsdc  12838  modxai  12854  mulgaddcom  13597  mulginvcom  13598  mulgz  13601  mulgdirlem  13604  mulgass  13610  mulgass2  13935  zncrng  14522  znzrh2  14523  zndvds  14526  znf1o  14528  znunit  14536  elply2  15322  elplyd  15328  dvply2g  15353  sgmnncl  15575  0sgmppw  15580  lgsneg1  15617  lgsdirnn0  15639  lgsdinn0  15640  2lgslem1c  15682  2lgslem3a1  15689  2lgslem3b1  15690  2lgslem3c1  15691  2lgsoddprmlem2  15698