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

Theorem nnz 10987
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 10985 . 2  |-  NN  C_  ZZ
21sseli 3439 1  |-  ( N  e.  NN  ->  N  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1897   NNcn 10636   ZZcz 10965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-nn 10637  df-z 10966
This theorem is referenced by:  elnnz1  10991  znegcl  11000  nnleltp1  11019  nnltp1le  11020  nnlem1lt  11030  nnltlem1  11031  nnm1ge0  11032  prime  11044  nneo  11047  zeo  11049  btwnz  11065  eluz2b2  11259  qaddcl  11308  qreccl  11312  elfz1end  11857  fznatpl1  11878  fznn  11891  elfz1b  11892  elfzo0  11986  fzo1fzo0n0  11987  elfzo0z  11988  elfzo1  11995  ubmelm1fzo  12037  quoremz  12113  intfracq  12117  fznnfl  12120  zmodcl  12147  zmodfz  12149  zmodfzo  12150  modidmul0OLD  12154  zmodid2  12156  zmodidfzo  12157  expnnval  12306  mulexpz  12343  nnesq  12427  expnlbnd  12433  expnlbnd2  12434  digit2  12436  faclbnd  12506  bc0k  12527  bcval5  12534  fz1isolem  12656  seqcoll  12659  lswccatn0lsw  12769  cshwidxmod  12941  cshwidxn  12946  absexpz  13416  climuni  13664  isercoll  13779  climcnds  13957  arisum  13966  trireciplem  13968  expcnv  13970  geo2sum  13977  geo2lim  13979  0.999...  13985  geoihalfsum  13986  rpnnen2lem6  14320  rpnnen2lem9  14323  rpnnen2lem10  14324  dvdsval3  14357  nndivdvds  14359  dvdsle  14398  dvdseq  14400  fzm1ndvds  14405  dvdsfac  14408  oexpneg  14416  divalg2  14434  divalgmod  14435  ndvdsadd  14437  nndvdslegcd  14527  modgcd  14548  gcddiv  14565  gcdmultiple  14566  gcdmultiplez  14567  gcdeq  14568  rpmulgcd  14571  rplpwr  14572  rppwr  14573  sqgcd  14574  dvdssqlem  14575  dvdssq  14576  eucalginv  14591  lcmgcdlem  14619  lcmgcdnn  14624  lcmass  14627  lcmftp  14657  lcmfunsnlem2lem1  14659  1idssfct  14678  isprm3  14681  prmind2  14683  divgcdodd  14701  coprmgcdb  14702  qredeq  14711  qredeu  14712  isprm6  14714  ncoprmlnprm  14725  coprmprod  14726  coprmproddvdslem  14727  coprmproddvds  14728  divnumden  14745  divdenle  14746  nn0gcdsq  14749  phicl2  14764  phiprmpw  14772  eulerthlem2  14778  pythagtriplem3  14816  pythagtriplem4  14817  pythagtriplem6  14819  pythagtriplem7  14820  pythagtriplem8  14821  pythagtriplem9  14822  pythagtriplem11  14823  pythagtriplem13  14825  pythagtriplem15  14827  pythagtriplem19  14831  pythagtrip  14832  iserodd  14833  pclem  14836  pccl  14847  pcdiv  14850  pcqcl  14854  pcdvds  14861  pcndvds  14863  pcndvds2  14865  pcelnn  14867  pcz  14878  pcmpt  14885  fldivp1  14890  pcfac  14892  infpnlem1  14902  prmunb  14906  prmreclem1  14908  1arith  14919  ram0  15028  prmdvdsprmo  15048  prmdvdsprmorOLD  15063  prmgaplem4  15072  prmgaplem6  15074  prmgaplem7  15075  cshwshashlem2  15115  mulgnn  16812  ghmmulg  16943  dfod2  17263  gexdvds  17283  gexnnod  17288  gexex  17539  mulgass2  17877  qsssubdrg  19075  prmirredlem  19112  znidomb  19180  znrrg  19184  chfacfisf  19926  chfacfisfcpmat  19927  chfacfscmul0  19930  chfacfpmmul0  19934  cayhamlem1  19938  cpmadugsumlemF  19948  lmmo  20444  1stckgenlem  20616  imasdsf1olem  21436  clmmulg  22172  cmetcaulem  22306  ovolunlem1a  22497  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  mbfi1fseqlem6  22726  dvexp3  22978  dgreq0  23267  elqaalem2  23321  elqaalem2OLD  23324  aaliou3lem1  23346  aaliou3lem2  23347  aaliou3lem3  23348  aaliou3lem9  23354  pserdvlem2  23431  logtayl2  23655  root1eq1  23743  root1cj  23744  atantayl2  23912  birthdaylem2  23926  birthdaylem3  23927  emcllem5  23973  basellem2  24056  basellem3  24057  basellem5  24059  sgmss  24081  issqf  24111  sgmnncl  24122  prmorcht  24153  mumullem1  24154  mumullem2  24155  sqff1o  24157  dvdsdivcl  24158  dvdsflsumcom  24165  muinv  24170  vmalelog  24181  chtublem  24187  vmasum  24192  logfac2  24193  logfaclbnd  24198  bclbnd  24256  bposlem5  24264  lgsval4a  24294  lgssq  24311  lgssq2  24312  lgsdchr  24324  lgsquadlem1  24330  lgsquadlem2  24331  lgsquad3  24337  rplogsumlem1  24370  rplogsumlem2  24371  dchrisumlem2  24376  dchrmusumlema  24379  dchrmusum2  24380  dchrvmasumiflem1  24387  dchrvmaeq0  24390  dchrisum0flblem2  24395  dchrisum0re  24399  dchrisum0lema  24400  dchrisum0lem1b  24401  dchrisum0lem2a  24403  logdivbnd  24442  pntrsumbnd2  24453  ostth2lem1  24504  ostth2lem3  24521  ostth3  24524  axlowdimlem13  25032  clwwlkel  25569  clwwlkf  25570  clwwlkvbij  25577  wwlksubclwwlk  25580  clwwisshclwwlem  25582  clwwisshclww  25583  numclwlk2lem2f  25879  gxpval  26035  gxcom  26045  gxinv  26046  gxid  26049  gxmodid  26055  gxdi  26072  bcm1n  28419  pnfinf  28548  isarchiofld  28628  rearchi  28653  submat1n  28679  lmatfvlem  28689  esumcvg  28955  oddpwdc  29235  fibp1  29282  erdszelem7  29968  climuzcnv  30363  elfzm12  30367  bcprod  30422  nn0prpwlem  31026  poimirlem13  31997  poimirlem14  31998  mblfinlem2  32022  fzmul  32113  incsequz  32121  geomcau  32132  heibor1lem  32185  bfplem2  32199  fzsplit1nn0  35640  irrapxlem1  35710  pellexlem5  35721  rmynn  35850  jm2.24nn  35853  jm2.17c  35856  congrep  35867  congabseq  35868  acongrep  35874  acongeq  35877  jm2.18  35887  jm2.23  35895  jm2.20nn  35896  jm2.26lem3  35900  jm2.26  35901  jm2.15nn0  35902  jm2.16nn0  35903  jm2.27dlem2  35909  rmydioph  35913  jm3.1  35919  expdiophlem1  35920  expdioph  35922  idomodle  36114  hashgcdlem  36118  hashgcdeq  36119  phisum  36120  proot1ex  36122  nznngen  36708  sumnnodd  37747  stoweidlem7  37904  stoweidlem17  37914  wallispilem4  37967  stirlinglem2  37974  stirlinglem3  37975  stirlinglem4  37976  stirlinglem12  37984  stirlinglem13  37985  stirlinglem14  37986  stirlinglem15  37987  stirlingr  37989  dirkertrigeqlem1  37997  fouriersw  38132  ovnsubaddlem1  38429  iccpartres  38769  iccpartipre  38772  iccpartltu  38776  iccelpart  38784  gcdzeq  38830  nneoALTV  38838  divgcdoddALTV  38848  gboge7  38901  gbege6  38903  subsubelfzo0  39103  2ffzoeq  39105  altgsumbc  40405  altgsumbcALT  40406  pw2m1lepw2m1  40590  nnpw2even  40608  nnlog2ge0lt1  40649  logbpw2m1  40650  blenpw2m1  40662  nnpw2blenfzo  40664  nnpw2pmod  40666  nnpw2p  40669  blengt1fldiv2p1  40676  dignn0fr  40684  dignn0flhalflem1  40698  dignn0flhalflem2  40699  nn0sumshdiglemA  40702  nn0sumshdiglemB  40703
  Copyright terms: Public domain W3C validator