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

Theorem nnz 10911
Description: A positive integer is an integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nnz

Proof of Theorem nnz
StepHypRef Expression
1 nnssz 10909 . 2
21sseli 3499 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cn 10561   cz 10889
This theorem is referenced by:  elnnz1  10915  znegcl  10924  nnleltp1  10943  nnltp1le  10944  nnlem1lt  10954  nnltlem1  10955  nnm1ge0  10956  prime  10968  nneo  10971  zeo  10973  uzindOLD  10982  btwnz  10991  eluz2b2  11183  qaddcl  11227  qreccl  11231  elfz1end  11744  fznatpl1  11763  fznn  11776  elfz1b  11777  elfzo0  11863  fzo1fzo0n0  11864  elfzo0z  11865  elfzo1  11871  ubmelm1fzo  11908  quoremz  11982  intfracq  11986  fznnfl  11989  zmodcl  12015  zmodfz  12017  zmodfzo  12018  modidmul0  12022  zmodid2  12024  zmodidfzo  12025  expnnval  12169  mulexpz  12206  nnesq  12290  expnlbnd  12296  expnlbnd2  12297  digit2  12299  faclbnd  12368  bc0k  12389  bcval5  12396  fz1isolem  12510  seqcoll  12512  cshwidxmod  12774  cshwidxn  12779  absexpz  13138  climuni  13375  isercoll  13490  climcnds  13663  arisum  13671  trireciplem  13673  expcnv  13675  geo2sum  13682  geo2lim  13684  0.999...  13690  geoihalfsum  13691  rpnnen2lem6  13953  rpnnen2lem9  13956  rpnnen2lem10  13957  dvdsval3  13990  nndivdvds  13992  dvdsle  14031  dvdseq  14033  fzm1ndvds  14038  dvdsfac  14041  oexpneg  14049  divalg2  14063  divalgmod  14064  ndvdsadd  14066  modgcd  14174  gcddiv  14187  gcdmultiple  14188  gcdmultiplez  14189  gcdeq  14190  rpmulgcd  14193  rplpwr  14194  rppwr  14195  sqgcd  14196  dvdssqlem  14197  dvdssq  14198  eucalginv  14213  1idssfct  14223  isprm3  14226  prmind2  14228  qredeq  14247  qredeu  14248  isprm6  14250  divgcdodd  14260  divnumden  14281  divdenle  14282  nn0gcdsq  14285  phicl2  14298  phiprmpw  14306  eulerthlem2  14312  pythagtriplem3  14342  pythagtriplem4  14343  pythagtriplem6  14345  pythagtriplem7  14346  pythagtriplem8  14347  pythagtriplem9  14348  pythagtriplem11  14349  pythagtriplem13  14351  pythagtriplem15  14353  pythagtriplem19  14357  pythagtrip  14358  iserodd  14359  pclem  14362  pccl  14373  pcdiv  14376  pcqcl  14380  pcdvds  14387  pcndvds  14389  pcndvds2  14391  pcelnn  14393  pcz  14404  pcmpt  14411  fldivp1  14416  pcfac  14418  infpnlem1  14428  prmunb  14432  prmreclem1  14434  1arith  14445  ram0  14540  cshwshashlem2  14581  mulgnn  16148  ghmmulg  16279  dfod2  16586  gexdvds  16604  gexnnod  16608  gexex  16859  mulgass2  17247  qsssubdrg  18477  prmirredlem  18523  prmirredlemOLD  18526  znidomb  18600  znrrg  18604  chfacfisf  19355  chfacfisfcpmat  19356  chfacfscmul0  19359  chfacfpmmul0  19363  cayhamlem1  19367  cpmadugsumlemF  19377  lmmo  19881  1stckgenlem  20054  imasdsf1olem  20876  clmmulg  21593  cmetcaulem  21727  ovolunlem1a  21907  ovolicc2lem4  21931  mbfi1fseqlem6  22127  dvexp3  22379  dgreq0  22662  elqaalem2  22716  aaliou3lem1  22738  aaliou3lem2  22739  aaliou3lem3  22740  aaliou3lem9  22746  pserdvlem2  22823  logtayl2  23043  root1eq1  23129  root1cj  23130  atantayl2  23269  birthdaylem2  23282  birthdaylem3  23283  emcllem5  23329  basellem2  23355  basellem3  23356  basellem5  23358  sgmss  23380  issqf  23410  sgmnncl  23421  prmorcht  23452  mumullem1  23453  mumullem2  23454  sqff1o  23456  dvdsdivcl  23457  dvdsflsumcom  23464  muinv  23469  vmalelog  23480  chtublem  23486  vmasum  23491  logfac2  23492  logfaclbnd  23497  bclbnd  23555  bposlem5  23563  lgsval4a  23593  lgssq  23610  lgssq2  23611  lgsdchr  23623  lgsquadlem1  23629  lgsquadlem2  23630  lgsquad3  23636  rplogsumlem1  23669  rplogsumlem2  23670  dchrisumlem2  23675  dchrmusumlema  23678  dchrmusum2  23679  dchrvmasumiflem1  23686  dchrvmaeq0  23689  dchrisum0flblem2  23694  dchrisum0re  23698  dchrisum0lema  23699  dchrisum0lem1b  23700  dchrisum0lem2a  23702  logdivbnd  23741  pntrsumbnd2  23752  ostth2lem1  23803  ostth2lem3  23820  ostth3  23823  axlowdimlem13  24257  clwwlkel  24793  clwwlkf  24794  clwwlkvbij  24801  wwlksubclwwlk  24804  clwwisshclwwlem  24806  clwwisshclww  24807  numclwlk2lem2f  25103  gxpval  25261  gxcom  25271  gxinv  25272  gxid  25275  gxmodid  25281  gxdi  25298  bcm1n  27600  pnfinf  27727  isarchiofld  27807  rearchi  27832  esumcvg  28092  oddpwdc  28293  fibp1  28340  erdszelem7  28641  climuzcnv  29037  elfzm12  29041  mblfinlem2  30052  nn0prpwlem  30140  fzmul  30233  incsequz  30241  geomcau  30252  heibor1lem  30305  bfplem2  30319  fzsplit1nn0  30687  irrapxlem1  30758  pellexlem5  30769  rmynn  30894  jm2.24nn  30897  jm2.17c  30900  congrep  30911  congabseq  30912  acongrep  30918  acongeq  30921  jm2.18  30930  jm2.23  30938  jm2.20nn  30939  jm2.26lem3  30943  jm2.26  30944  jm2.15nn0  30945  jm2.16nn0  30946  jm2.27dlem2  30952  rmydioph  30956  jm3.1  30962  expdiophlem1  30963  expdioph  30965  idomodle  31153  hashgcdlem  31157  hashgcdeq  31158  phisum  31159  proot1ex  31161  lcmgcdlem  31212  lcmass  31218  nznngen  31221  sumnnodd  31636  stoweidlem7  31789  stoweidlem17  31799  wallispilem4  31850  stirlinglem2  31857  stirlinglem3  31858  stirlinglem4  31859  stirlinglem12  31867  stirlinglem13  31868  stirlinglem14  31869  stirlinglem15  31870  stirlingr  31872  dirkertrigeqlem1  31880  fouriersw  32014  subsubelfzo0  32338  2ffzoeq  32341  altgsumbc  32941  altgsumbcALT  32942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-recs 7061  df-rdg 7095  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-nn 10562  df-z 10890
  Copyright terms: Public domain W3C validator