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

Theorem nnz 10910
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 10908 . 2  |-  NN  C_  ZZ
21sseli 3403 1  |-  ( N  e.  NN  ->  N  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   NNcn 10560   ZZcz 10888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567
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 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-er 7318  df-en 7525  df-dom 7526  df-sdom 7527  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-nn 10561  df-z 10889
This theorem is referenced by:  elnnz1  10914  znegcl  10923  nnleltp1  10942  nnltp1le  10943  nnlem1lt  10953  nnltlem1  10954  nnm1ge0  10955  prime  10967  nneo  10970  zeo  10972  btwnz  10988  eluz2b2  11182  qaddcl  11231  qreccl  11235  elfz1end  11780  fznatpl1  11801  fznn  11814  elfz1b  11815  elfzo0  11907  fzo1fzo0n0  11908  elfzo0z  11909  elfzo1  11915  ubmelm1fzo  11957  quoremz  12032  intfracq  12036  fznnfl  12039  zmodcl  12066  zmodfz  12068  zmodfzo  12069  modidmul0OLD  12073  zmodid2  12075  zmodidfzo  12076  expnnval  12225  mulexpz  12262  nnesq  12346  expnlbnd  12352  expnlbnd2  12353  digit2  12355  faclbnd  12425  bc0k  12446  bcval5  12453  fz1isolem  12572  seqcoll  12575  lswccatn0lsw  12682  cshwidxmod  12851  cshwidxn  12856  absexpz  13312  climuni  13559  isercoll  13674  climcnds  13852  arisum  13861  trireciplem  13863  expcnv  13865  geo2sum  13872  geo2lim  13874  0.999...  13880  geoihalfsum  13881  rpnnen2lem6  14215  rpnnen2lem9  14218  rpnnen2lem10  14219  dvdsval3  14252  nndivdvds  14254  dvdsle  14293  dvdseq  14295  fzm1ndvds  14300  dvdsfac  14303  oexpneg  14311  divalg2  14329  divalgmod  14330  ndvdsadd  14332  nndvdslegcd  14422  modgcd  14443  gcddiv  14460  gcdmultiple  14461  gcdmultiplez  14462  gcdeq  14463  rpmulgcd  14466  rplpwr  14467  rppwr  14468  sqgcd  14469  dvdssqlem  14470  dvdssq  14471  eucalginv  14486  lcmgcdlem  14514  lcmgcdnn  14519  lcmass  14522  lcmftp  14552  lcmfunsnlem2lem1  14554  1idssfct  14573  isprm3  14576  prmind2  14578  divgcdodd  14596  coprmgcdb  14597  qredeq  14606  qredeu  14607  isprm6  14609  ncoprmlnprm  14620  coprmprod  14621  coprmproddvdslem  14622  coprmproddvds  14623  divnumden  14640  divdenle  14641  nn0gcdsq  14644  phicl2  14659  phiprmpw  14667  eulerthlem2  14673  pythagtriplem3  14711  pythagtriplem4  14712  pythagtriplem6  14714  pythagtriplem7  14715  pythagtriplem8  14716  pythagtriplem9  14717  pythagtriplem11  14718  pythagtriplem13  14720  pythagtriplem15  14722  pythagtriplem19  14726  pythagtrip  14727  iserodd  14728  pclem  14731  pccl  14742  pcdiv  14745  pcqcl  14749  pcdvds  14756  pcndvds  14758  pcndvds2  14760  pcelnn  14762  pcz  14773  pcmpt  14780  fldivp1  14785  pcfac  14787  infpnlem1  14797  prmunb  14801  prmreclem1  14803  1arith  14814  ram0  14923  prmdvdsprmo  14943  prmdvdsprmorOLD  14958  prmgaplem4  14967  prmgaplem6  14969  prmgaplem7  14970  cshwshashlem2  15010  mulgnn  16707  ghmmulg  16838  dfod2  17158  gexdvds  17178  gexnnod  17183  gexex  17434  mulgass2  17772  qsssubdrg  18970  prmirredlem  19006  znidomb  19074  znrrg  19078  chfacfisf  19820  chfacfisfcpmat  19821  chfacfscmul0  19824  chfacfpmmul0  19828  cayhamlem1  19832  cpmadugsumlemF  19842  lmmo  20338  1stckgenlem  20510  imasdsf1olem  21330  clmmulg  22066  cmetcaulem  22200  ovolunlem1a  22391  ovolicc2lem4OLD  22415  ovolicc2lem4  22416  mbfi1fseqlem6  22620  dvexp3  22872  dgreq0  23161  elqaalem2  23215  elqaalem2OLD  23218  aaliou3lem1  23240  aaliou3lem2  23241  aaliou3lem3  23242  aaliou3lem9  23248  pserdvlem2  23325  logtayl2  23549  root1eq1  23637  root1cj  23638  atantayl2  23806  birthdaylem2  23820  birthdaylem3  23821  emcllem5  23867  basellem2  23950  basellem3  23951  basellem5  23953  sgmss  23975  issqf  24005  sgmnncl  24016  prmorcht  24047  mumullem1  24048  mumullem2  24049  sqff1o  24051  dvdsdivcl  24052  dvdsflsumcom  24059  muinv  24064  vmalelog  24075  chtublem  24081  vmasum  24086  logfac2  24087  logfaclbnd  24092  bclbnd  24150  bposlem5  24158  lgsval4a  24188  lgssq  24205  lgssq2  24206  lgsdchr  24218  lgsquadlem1  24224  lgsquadlem2  24225  lgsquad3  24231  rplogsumlem1  24264  rplogsumlem2  24265  dchrisumlem2  24270  dchrmusumlema  24273  dchrmusum2  24274  dchrvmasumiflem1  24281  dchrvmaeq0  24284  dchrisum0flblem2  24289  dchrisum0re  24293  dchrisum0lema  24294  dchrisum0lem1b  24295  dchrisum0lem2a  24297  logdivbnd  24336  pntrsumbnd2  24347  ostth2lem1  24398  ostth2lem3  24415  ostth3  24418  axlowdimlem13  24926  clwwlkel  25463  clwwlkf  25464  clwwlkvbij  25471  wwlksubclwwlk  25474  clwwisshclwwlem  25476  clwwisshclww  25477  numclwlk2lem2f  25773  gxpval  25929  gxcom  25939  gxinv  25940  gxid  25943  gxmodid  25949  gxdi  25966  bcm1n  28321  pnfinf  28451  isarchiofld  28532  rearchi  28557  submat1n  28583  lmatfvlem  28593  esumcvg  28859  oddpwdc  29139  fibp1  29186  erdszelem7  29872  climuzcnv  30267  elfzm12  30271  bcprod  30325  nn0prpwlem  30927  poimirlem13  31860  poimirlem14  31861  mblfinlem2  31885  fzmul  31976  incsequz  31984  geomcau  31995  heibor1lem  32048  bfplem2  32062  fzsplit1nn0  35508  irrapxlem1  35579  pellexlem5  35590  rmynn  35719  jm2.24nn  35722  jm2.17c  35725  congrep  35736  congabseq  35737  acongrep  35743  acongeq  35746  jm2.18  35756  jm2.23  35764  jm2.20nn  35765  jm2.26lem3  35769  jm2.26  35770  jm2.15nn0  35771  jm2.16nn0  35772  jm2.27dlem2  35778  rmydioph  35782  jm3.1  35788  expdiophlem1  35789  expdioph  35791  idomodle  35983  hashgcdlem  35987  hashgcdeq  35988  phisum  35989  proot1ex  35991  nznngen  36578  sumnnodd  37593  stoweidlem7  37750  stoweidlem17  37760  wallispilem4  37813  stirlinglem2  37820  stirlinglem3  37821  stirlinglem4  37822  stirlinglem12  37830  stirlinglem13  37831  stirlinglem14  37832  stirlinglem15  37833  stirlingr  37835  dirkertrigeqlem1  37843  fouriersw  37978  ovnsubaddlem1  38239  iccpartres  38545  iccpartipre  38548  iccpartltu  38552  iccelpart  38560  gcdzeq  38606  nneoALTV  38614  divgcdoddALTV  38624  gboge7  38677  gbege6  38679  subsubelfzo0  38860  2ffzoeq  38862  altgsumbc  39736  altgsumbcALT  39737  pw2m1lepw2m1  39921  nnpw2even  39939  nnlog2ge0lt1  39980  logbpw2m1  39981  blenpw2m1  39993  nnpw2blenfzo  39995  nnpw2pmod  39997  nnpw2p  40000  blengt1fldiv2p1  40007  dignn0fr  40015  dignn0flhalflem1  40029  dignn0flhalflem2  40030  nn0sumshdiglemA  40033  nn0sumshdiglemB  40034
  Copyright terms: Public domain W3C validator