MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnz Structured version   Unicode version

Theorem nnz 10959
Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nnz  |-  ( N  e.  NN  ->  N  e.  ZZ )

Proof of Theorem nnz
StepHypRef Expression
1 nnssz 10957 . 2  |-  NN  C_  ZZ
21sseli 3466 1  |-  ( N  e.  NN  ->  N  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   NNcn 10609   ZZcz 10937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-nn 10610  df-z 10938
This theorem is referenced by:  elnnz1  10963  znegcl  10972  nnleltp1  10991  nnltp1le  10992  nnlem1lt  11002  nnltlem1  11003  nnm1ge0  11004  prime  11016  nneo  11019  zeo  11021  btwnz  11037  eluz2b2  11231  qaddcl  11280  qreccl  11284  elfz1end  11827  fznatpl1  11848  fznn  11861  elfz1b  11862  elfzo0  11954  fzo1fzo0n0  11955  elfzo0z  11956  elfzo1  11962  ubmelm1fzo  12004  quoremz  12079  intfracq  12083  fznnfl  12086  zmodcl  12113  zmodfz  12115  zmodfzo  12116  modidmul0OLD  12120  zmodid2  12122  zmodidfzo  12123  expnnval  12272  mulexpz  12309  nnesq  12393  expnlbnd  12399  expnlbnd2  12400  digit2  12402  faclbnd  12472  bc0k  12493  bcval5  12500  fz1isolem  12619  seqcoll  12621  lswccatn0lsw  12721  cshwidxmod  12890  cshwidxn  12895  absexpz  13347  climuni  13594  isercoll  13709  climcnds  13887  arisum  13896  trireciplem  13898  expcnv  13900  geo2sum  13907  geo2lim  13909  0.999...  13915  geoihalfsum  13916  rpnnen2lem6  14250  rpnnen2lem9  14253  rpnnen2lem10  14254  dvdsval3  14287  nndivdvds  14289  dvdsle  14328  dvdseq  14330  fzm1ndvds  14335  dvdsfac  14338  oexpneg  14346  divalg2  14361  divalgmod  14362  ndvdsadd  14364  nndvdslegcd  14453  modgcd  14474  gcddiv  14488  gcdmultiple  14489  gcdmultiplez  14490  gcdeq  14491  rpmulgcd  14494  rplpwr  14495  rppwr  14496  sqgcd  14497  dvdssqlem  14498  dvdssq  14499  eucalginv  14514  lcmgcdlem  14542  lcmgcdnn  14547  lcmass  14550  lcmftp  14580  lcmfunsnlem2lem1  14582  1idssfct  14601  isprm3  14604  prmind2  14606  divgcdodd  14624  coprmgcdb  14625  qredeq  14634  qredeu  14635  isprm6  14637  ncoprmlnprm  14648  coprmprod  14649  coprmproddvdslem  14650  coprmproddvds  14651  divnumden  14668  divdenle  14669  nn0gcdsq  14672  phicl2  14685  phiprmpw  14693  eulerthlem2  14699  pythagtriplem3  14731  pythagtriplem4  14732  pythagtriplem6  14734  pythagtriplem7  14735  pythagtriplem8  14736  pythagtriplem9  14737  pythagtriplem11  14738  pythagtriplem13  14740  pythagtriplem15  14742  pythagtriplem19  14746  pythagtrip  14747  iserodd  14748  pclem  14751  pccl  14762  pcdiv  14765  pcqcl  14769  pcdvds  14776  pcndvds  14778  pcndvds2  14780  pcelnn  14782  pcz  14793  pcmpt  14800  fldivp1  14805  pcfac  14807  infpnlem1  14817  prmunb  14821  prmreclem1  14823  1arith  14834  ram0  14943  prmdvdsprmo  14963  prmdvdsprmorOLD  14978  prmgaplem4  14987  prmgaplem6  14989  prmgaplem7  14990  cshwshashlem2  15030  mulgnn  16715  ghmmulg  16846  dfod2  17153  gexdvds  17171  gexnnod  17175  gexex  17426  mulgass2  17764  qsssubdrg  18962  prmirredlem  18995  znidomb  19063  znrrg  19067  chfacfisf  19809  chfacfisfcpmat  19810  chfacfscmul0  19813  chfacfpmmul0  19817  cayhamlem1  19821  cpmadugsumlemF  19831  lmmo  20327  1stckgenlem  20499  imasdsf1olem  21319  clmmulg  22017  cmetcaulem  22151  ovolunlem1a  22327  ovolicc2lem4  22351  mbfi1fseqlem6  22555  dvexp3  22807  dgreq0  23087  elqaalem2  23141  aaliou3lem1  23163  aaliou3lem2  23164  aaliou3lem3  23165  aaliou3lem9  23171  pserdvlem2  23248  logtayl2  23472  root1eq1  23560  root1cj  23561  atantayl2  23729  birthdaylem2  23743  birthdaylem3  23744  emcllem5  23790  basellem2  23871  basellem3  23872  basellem5  23874  sgmss  23896  issqf  23926  sgmnncl  23937  prmorcht  23968  mumullem1  23969  mumullem2  23970  sqff1o  23972  dvdsdivcl  23973  dvdsflsumcom  23980  muinv  23985  vmalelog  23996  chtublem  24002  vmasum  24007  logfac2  24008  logfaclbnd  24013  bclbnd  24071  bposlem5  24079  lgsval4a  24109  lgssq  24126  lgssq2  24127  lgsdchr  24139  lgsquadlem1  24145  lgsquadlem2  24146  lgsquad3  24152  rplogsumlem1  24185  rplogsumlem2  24186  dchrisumlem2  24191  dchrmusumlema  24194  dchrmusum2  24195  dchrvmasumiflem1  24202  dchrvmaeq0  24205  dchrisum0flblem2  24210  dchrisum0re  24214  dchrisum0lema  24215  dchrisum0lem1b  24216  dchrisum0lem2a  24218  logdivbnd  24257  pntrsumbnd2  24268  ostth2lem1  24319  ostth2lem3  24336  ostth3  24339  axlowdimlem13  24830  clwwlkel  25366  clwwlkf  25367  clwwlkvbij  25374  wwlksubclwwlk  25377  clwwisshclwwlem  25379  clwwisshclww  25380  numclwlk2lem2f  25676  gxpval  25832  gxcom  25842  gxinv  25843  gxid  25846  gxmodid  25852  gxdi  25869  bcm1n  28207  pnfinf  28338  isarchiofld  28419  rearchi  28444  submat1n  28470  lmatfvlem  28480  esumcvg  28746  oddpwdc  29013  fibp1  29060  erdszelem7  29708  climuzcnv  30103  elfzm12  30107  bcprod  30161  nn0prpwlem  30763  poimirlem13  31656  poimirlem14  31657  mblfinlem2  31681  fzmul  31772  incsequz  31780  geomcau  31791  heibor1lem  31844  bfplem2  31858  fzsplit1nn0  35304  irrapxlem1  35375  pellexlem5  35386  rmynn  35511  jm2.24nn  35514  jm2.17c  35517  congrep  35528  congabseq  35529  acongrep  35535  acongeq  35538  jm2.18  35548  jm2.23  35556  jm2.20nn  35557  jm2.26lem3  35561  jm2.26  35562  jm2.15nn0  35563  jm2.16nn0  35564  jm2.27dlem2  35570  rmydioph  35574  jm3.1  35580  expdiophlem1  35581  expdioph  35583  idomodle  35768  hashgcdlem  35772  hashgcdeq  35773  phisum  35774  proot1ex  35776  nznngen  36301  sumnnodd  37281  stoweidlem7  37435  stoweidlem17  37445  wallispilem4  37498  stirlinglem2  37505  stirlinglem3  37506  stirlinglem4  37507  stirlinglem12  37515  stirlinglem13  37516  stirlinglem14  37517  stirlinglem15  37518  stirlingr  37520  dirkertrigeqlem1  37528  fouriersw  37662  iccpartres  38121  iccpartipre  38124  iccpartltu  38128  iccelpart  38136  gcdzeq  38182  nneoALTV  38190  divgcdoddALTV  38200  gboge7  38253  gbege6  38255  subsubelfzo0  38410  2ffzoeq  38412  altgsumbc  38892  altgsumbcALT  38893  pw2m1lepw2m1  39078  nnpw2even  39096  nnlog2ge0lt1  39137  logbpw2m1  39138  blenpw2m1  39150  nnpw2blenfzo  39152  nnpw2pmod  39154  nnpw2p  39157  blengt1fldiv2p1  39164  dignn0fr  39172  dignn0flhalflem1  39186  dignn0flhalflem2  39187  nn0sumshdiglemA  39190  nn0sumshdiglemB  39191
  Copyright terms: Public domain W3C validator