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

Theorem nn0zd 10992
Description: A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
nn0zd.1
Assertion
Ref Expression
nn0zd

Proof of Theorem nn0zd
StepHypRef Expression
1 nn0ssz 10910 . 2
2 nn0zd.1 . 2
31, 2sseldi 3501 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cn0 10820   cz 10889
This theorem is referenced by:  nnzd  10993  elfz0addOLD  11805  difelfznle  11818  zmodfz  12017  expnegz  12200  expaddzlem  12209  expaddz  12210  expmulz  12212  faclbnd  12368  bcpasc  12399  hashf1  12506  fz1isolem  12510  hashge2el2dif  12521  hashtpg  12523  wrdlenge1n0  12576  ccatcl  12593  ccatval1  12595  ccatval3  12597  ccatsymb  12600  ccatass  12605  ccatrn  12606  lswccatn0lsw  12607  ccats1val2  12631  ccat2s1fvw  12642  swrdtrcfv0  12669  swrdspsleq  12673  swrdtrcfvl  12675  swrdccat1  12682  swrdccat2  12683  swrdccatin2  12712  swrdccatin12  12716  splfv2a  12732  splval2  12733  revcl  12735  revccat  12740  revrev  12741  cshwmodn  12766  cshwsublen  12767  cshwn  12768  cshwidxmod  12774  2cshwid  12782  3cshw  12786  cshweqdif2  12787  revco  12800  ccatco  12801  ccat2s1fvwALT  12893  zabscl  13146  absrdbnd  13174  iseraltlem3  13506  fsum0diaglem  13591  modfsummods  13607  binomlem  13641  binom1p  13643  incexc2  13650  climcndslem1  13661  geoser  13678  geolim2  13680  mertenslem1  13693  mertenslem2  13694  mertens  13695  ruclem10  13972  divalglem9  14059  divalgmod  14064  bitsfzolem  14084  bitsfzo  14085  bitsmod  14086  bitsfi  14087  bitsinv1lem  14091  sadcaddlem  14107  sadadd3  14111  sadaddlem  14116  sadadd  14117  sadasslem  14120  sadass  14121  sadeq  14122  bitsres  14123  bitsuz  14124  bitsshft  14125  smuval2  14132  smupvallem  14133  smupval  14138  smueqlem  14140  smumullem  14142  smumul  14143  gcdcllem1  14149  gcd0id  14161  gcdneg  14164  modgcd  14174  bezoutlem4  14179  dvdsgcdb  14182  gcdass  14183  mulgcd  14184  gcdeq  14190  dvdsmulgcd  14192  nn0seqcvgd  14199  algfx  14209  eucalginv  14213  eucalg  14216  sqnprm  14239  mulgcddvds  14245  rpmulgcd2  14246  qredeu  14248  divnumden  14281  powm2modprm  14328  coprimeprodsq  14333  iserodd  14359  pclem  14362  pcpre1  14366  pcpremul  14367  pcqcl  14380  pcdvdsb  14392  pcidlem  14395  pc2dvds  14402  pcprmpw2  14405  pcadd  14408  pcfac  14418  pcbc  14419  pockthlem  14423  prmreclem2  14435  prmreclem3  14436  mul4sqlem  14471  4sqlem11  14473  4sqlem12  14474  4sqlem14  14476  vdwapun  14492  lagsubg  16263  psgnuni  16524  psgnran  16540  odmodnn0  16564  mndodconglem  16565  mndodcong  16566  odmulg2  16577  odmulg  16578  odmulgeq  16579  odbezout  16580  odinv  16583  odf1  16584  gexod  16606  gexdvds3  16610  sylow1lem1  16618  sylow1lem3  16620  pgpfi  16625  pgpssslw  16634  sylow2alem2  16638  sylow2blem3  16642  fislw  16645  sylow3lem4  16650  sylow3lem6  16652  efginvrel2  16745  efgredlemf  16759  efgredlemd  16762  efgredlemc  16763  efgredlem  16765  efgcpbllemb  16773  odadd1  16854  odadd2  16855  gexexlem  16858  gexex  16859  torsubg  16860  lt6abl  16897  gsummulg  16965  ablfacrplem  17116  ablfacrp  17117  ablfacrp2  17118  ablfac1b  17121  ablfac1c  17122  ablfac1eulem  17123  ablfac1eu  17124  pgpfac1lem2  17126  pgpfaclem1  17132  ablfaclem3  17138  srgbinomlem3  17193  srgbinomlem4  17194  psrbaglefi  18023  psrbaglefiOLD  18024  chrid  18564  znunit  18602  psgnghm  18616  chfacfscmulfsupp  19360  chfacfpmmulfsupp  19364  cpmadugsumlemF  19377  dyadss  22003  dyaddisjlem  22004  ply1divex  22537  ply1termlem  22600  plyeq0lem  22607  plyaddlem1  22610  plymullem1  22611  coeeulem  22621  coeidlem  22634  coeeq2  22639  coemulhi  22651  dvply1  22680  dvply2g  22681  plydivex  22693  elqaalem2  22716  aareccl  22722  aannenlem1  22724  aalioulem1  22728  taylplem1  22758  taylplem2  22759  taylpfval  22760  dvtaylp  22765  taylthlem2  22769  dvradcnv  22816  abelthlem7  22833  cxpeq  23131  birthdaylem2  23282  ftalem1  23346  basellem3  23356  isppw2  23389  isnsqf  23409  mule1  23422  ppinncl  23448  musum  23467  chtublem  23486  pclogsum  23490  vmasum  23491  dchrabs  23535  bcmax  23553  bposlem1  23559  bposlem6  23564  lgsval2lem  23581  lgsmod  23596  lgsdirprm  23604  lgsne0  23608  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem3  23626  lgseisenlem4  23627  lgsquadlem1  23629  m1lgs  23637  2sqlem8  23647  chebbnd1lem1  23654  dchrisumlem1  23674  dchrisum0flblem1  23693  selberg2lem  23735  ostth2lem2  23819  ostth2lem3  23820  wwlknredwwlkn0  24727  wwlkextproplem2  24742  clwwlkndivn  24837  nbhashuvtx1  24915  eupath2lem3  24979  eupath2  24980  numclwwlkovf2ex  25086  numclwwlk5  25112  numclwwlk6  25113  ex-ind-dvds  25170  gxnn0mul  25279  nndiffz1  27596  2sqcoprm  27635  2sqmod  27636  archirng  27732  archirngz  27733  archiabllem1a  27735  qqhval2lem  27962  oddpwdc  28293  eulerpartlems  28299  eulerpartlemb  28307  sseqfv1  28328  sseqfn  28329  sseqmw  28330  sseqf  28331  sseqfv2  28333  sseqp1  28334  eluzmn  28491  ccatmulgnn0dir  28496  ofccat  28497  signsplypnf  28507  signsply0  28508  signslema  28519  signstfvn  28526  signstfvp  28528  signstfvc  28531  subfacval3  28633  binomfallfaclem2  29162  binomrisefac  29164  fallfacval4  29165  bpolydiflem  29816  geomcau  30252  eldioph2lem1  30693  pellexlem5  30769  congrep  30911  bezoutr  30923  bezoutr1  30924  jm2.18  30930  jm2.19lem1  30931  jm2.19lem2  30932  jm2.19  30935  jm2.22  30937  jm2.23  30938  jm2.20nn  30939  jm2.25  30941  jm2.26a  30942  jm2.26lem3  30943  jm2.26  30944  jm2.27a  30947  jm2.27b  30948  jm2.27c  30949  jm3.1  30962  expdiophlem1  30963  hbtlem5  31077  radcnvrat  31195  gcddvdslcm  31208  lcmneg  31209  lcmgcdlem  31212  lcmdvds  31214  lcmgcdeq  31216  lcmdvdsb  31217  lcmass  31218  nzin  31223  bccbc  31250  binomcxplemnn0  31254  binomcxplemnotnn0  31261  fprodexp  31600  mccllem  31605  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnxpaek  31739  dvnmul  31740  dvnprodlem1  31743  dvnprodlem2  31744  wallispilem1  31847  wallispilem5  31851  stirlinglem3  31858  stirlinglem5  31860  stirlinglem7  31862  stirlinglem8  31863  fourierdlem102  31991  fourierdlem114  32003  sqwvfoura  32011  elaa2lem  32016  etransclem10  32027  etransclem20  32037  etransclem21  32038  etransclem22  32039  etransclem23  32040  etransclem24  32041  etransclem27  32044  etransclem28  32045  etransclem35  32052  etransclem38  32055  etransclem44  32061  etransclem45  32062  etransclem46  32063  fsummmodsnunz  32348  ssnn0ssfz  32938  altgsumbcALT  32942  aacllem  33216
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-n0 10821  df-z 10890
  Copyright terms: Public domain W3C validator