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

Theorem nnne0d 10587
Description: A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnge1d.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nnne0d  |-  ( ph  ->  A  =/=  0 )

Proof of Theorem nnne0d
StepHypRef Expression
1 nnge1d.1 . 2  |-  ( ph  ->  A  e.  NN )
2 nnne0 10575 . 2  |-  ( A  e.  NN  ->  A  =/=  0 )
31, 2syl 16 1  |-  ( ph  ->  A  =/=  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804    =/= wne 2638   0cc0 9495   NNcn 10543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-recs 7044  df-rdg 7078  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10544
This theorem is referenced by:  facne0  12346  bcn1  12373  bcm1k  12375  bcp1n  12376  bcp1nk  12377  bcval5  12378  bcpasc  12381  hashf1  12488  trireciplem  13655  trirecip  13656  geo2sum  13664  geo2lim  13666  mertenslem1  13675  efcllem  13795  ege2le3  13807  efcj  13809  efaddlem  13810  eftlub  13826  eirrlem  13919  ruclem7  13951  sqr2irrlem  13963  bitsp1  14063  bitscmp  14070  sadcp1  14087  sadaddlem  14098  bitsres  14105  bitsuz  14106  bitsshft  14107  smupp1  14112  gcdeq0  14141  mulgcd  14166  sqgcd  14178  prmind2  14210  isprm5  14235  divgcdodd  14242  qmuldeneqnum  14262  divnumden  14263  numdensq  14269  hashdvds  14287  phiprmpw  14288  pythagtriplem4  14325  pythagtriplem19  14339  pcprendvds2  14347  pcpremul  14349  pceulem  14351  pcdiv  14358  pcqmul  14359  pc2dvds  14384  pcaddlem  14389  pcadd  14390  pcmpt2  14394  pcmptdvds  14395  pcbc  14401  expnprm  14403  prmpwdvds  14404  pockthlem  14405  prmreclem1  14416  prmreclem3  14418  prmreclem4  14419  4sqlem5  14442  4sqlem8  14445  4sqlem9  14446  4sqlem10  14447  mul4sqlem  14453  4sqlem12  14456  4sqlem14  14458  4sqlem15  14459  4sqlem16  14460  4sqlem17  14461  oddvds  16550  sylow1lem1  16597  sylow1lem4  16600  sylow1lem5  16601  sylow2blem3  16621  sylow3lem3  16628  sylow3lem4  16629  gexexlem  16837  ablfacrplem  17095  ablfacrp2  17097  ablfac1lem  17098  ablfac1b  17100  ablfac1eu  17103  pgpfac1lem3a  17106  pgpfac1lem3  17107  prmirredlem  18501  prmirredlemOLD  18504  znrrg  18582  fvmptnn04ifa  19329  chfacfscmulgsum  19339  chfacfpmmulgsum  19343  lebnumlem3  21441  lebnumii  21444  ovollb2lem  21877  uniioombllem4  21973  dyadovol  21980  dyaddisjlem  21982  opnmbllem  21988  mbfi1fseqlem3  22102  mbfi1fseqlem4  22103  mbfi1fseqlem5  22104  mbfi1fseqlem6  22105  tdeglem4  22436  dgrcolem1  22648  dgrcolem2  22649  dvply1  22658  vieta1lem1  22684  vieta1lem2  22685  elqaalem2  22694  elqaalem3  22695  aalioulem1  22706  aalioulem2  22707  aaliou3lem9  22724  taylfvallem1  22730  tayl0  22735  taylply2  22741  taylply  22742  dvtaylp  22743  taylthlem2  22747  pserdvlem2  22801  advlogexp  23014  cxpmul2  23048  cxpeq  23109  atantayl3  23248  leibpi  23251  log2cnv  23253  log2tlbnd  23254  birthdaylem2  23260  birthdaylem3  23261  amgmlem  23297  amgm  23298  emcllem2  23304  emcllem5  23307  fsumharmonic  23319  ftalem2  23325  ftalem4  23327  ftalem5  23328  basellem1  23332  basellem2  23333  basellem4  23335  basellem5  23336  basellem8  23339  sgmval2  23395  efchtdvds  23411  ppieq0  23428  dvdsdivcl  23435  fsumdvdsdiaglem  23437  dvdsflf1o  23441  muinv  23447  dvdsmulf1o  23448  chpchtsum  23472  logfaclbnd  23475  logexprlim  23478  mersenne  23480  perfectlem2  23483  perfect  23484  dchrabs  23513  bcmono  23530  bclbnd  23533  bposlem1  23537  bposlem2  23538  bposlem3  23539  bposlem6  23542  lgsval2lem  23559  lgseisenlem4  23605  lgsquadlem1  23607  lgsquadlem2  23608  lgsquad2lem1  23611  2sqlem3  23619  2sqlem8  23625  chebbnd1  23635  rplogsumlem2  23648  rpvmasumlem  23650  dchrisumlem1  23652  dchrmusum2  23657  dchrvmasumlem1  23658  dchrvmasum2lem  23659  dchrvmasum2if  23660  dchrvmasumlem3  23662  dchrvmasumiflem1  23664  dchrisum0flblem2  23672  mulogsumlem  23694  mulogsum  23695  mulog2sumlem2  23698  vmalogdivsum2  23701  vmalogdivsum  23702  logsqvma  23705  selberglem3  23710  selberg  23711  logdivbnd  23719  selberg3lem1  23720  selberg4lem1  23723  pntrsumo1  23728  selberg3r  23732  selberg4r  23733  selberg34r  23734  pntsval2  23739  pntrlog2bndlem2  23741  pntrlog2bndlem3  23742  pntrlog2bndlem5  23744  pntrlog2bndlem6  23746  pntpbnd1a  23748  pntpbnd1  23749  pntpbnd2  23750  padicabvf  23794  padicabvcxp  23795  ostth2  23800  ostth3  23801  bcm1n  27578  gcdnncl  27585  numdenneg  27586  2sqmod  27614  qqhf  27945  qqhghm  27947  qqhrhm  27948  qqhre  27976  oddpwdc  28271  signshnz  28526  zetacvg  28535  dmgmdivn0  28548  lgamgulmlem2  28550  lgamgulmlem3  28551  lgamgulmlem4  28552  lgamgulmlem5  28553  lgamgulmlem6  28554  lgamgulm2  28556  lgamcvg2  28575  gamcvg  28576  gamcvg2lem  28579  subfacval2  28609  subfaclim  28610  cvmliftlem7  28714  cvmliftlem10  28717  cvmliftlem11  28718  cvmliftlem13  28719  iprodgam  29101  fallfacval4  29141  bcfallfac  29142  faclimlem1  29144  faclim2  29149  bpolycl  29790  bpolysum  29791  bpolydiflem  29792  fsumkthpow  29794  opnmbllem0  30026  nn0prpwlem  30116  irrapxlem4  30737  irrapxlem5  30738  pellexlem2  30742  pellexlem6  30746  jm2.27c  30925  itgpowd  31158  lcmeq0  31182  lcmgcdlem  31188  hashnzfzclim  31203  mccllem  31559  clim1fr1  31561  dvnxpaek  31693  dvnprodlem2  31698  itgsinexp  31707  stoweidlem1  31737  stoweidlem11  31747  stoweidlem25  31761  stoweidlem26  31762  stoweidlem37  31773  stoweidlem38  31774  stoweidlem42  31778  stoweidlem51  31787  wallispilem4  31804  wallispilem5  31805  wallispi2lem1  31807  wallispi2lem2  31808  wallispi2  31809  stirlinglem4  31813  stirlinglem5  31814  stirlinglem12  31821  stirlinglem13  31822  sqwvfourb  31966  etransclem15  31986  etransclem20  31991  etransclem21  31992  etransclem22  31993  etransclem23  31994  etransclem24  31995  etransclem25  31996  etransclem31  32002  etransclem32  32003  etransclem33  32004  etransclem34  32005  etransclem35  32006  etransclem38  32009  etransclem41  32012  etransclem44  32015  etransclem45  32016  etransclem47  32018  etransclem48  32019
  Copyright terms: Public domain W3C validator