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

Theorem nnne0d 10681
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 10669 . 2  |-  ( A  e.  NN  ->  A  =/=  0 )
31, 2syl 17 1  |-  ( ph  ->  A  =/=  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1897    =/= wne 2632   0cc0 9564   NNcn 10636
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
This theorem is referenced by:  facne0  12502  bcn1  12529  bcm1k  12531  bcp1n  12532  bcp1nk  12533  bcval5  12534  bcpasc  12537  hashf1  12652  trireciplem  13968  trirecip  13969  geo2sum  13977  geo2lim  13979  mertenslem1  13988  fallfacval4  14144  bcfallfac  14145  bpolycl  14153  bpolysum  14154  bpolydiflem  14155  fsumkthpow  14157  efcllem  14180  ege2le3  14192  efcj  14194  efaddlem  14195  eftlub  14211  eirrlem  14304  ruclem7  14336  sqr2irrlem  14348  bitsp1  14452  bitscmp  14460  sadcp1  14477  sadaddlem  14488  bitsres  14495  bitsuz  14496  bitsshft  14497  smupp1  14502  gcdnncl  14529  gcdeq0  14533  mulgcd  14562  sqgcd  14574  lcmeq0  14613  lcmgcdlem  14619  lcmfeq0b  14651  lcmfunsnlem2lem1  14659  lcmfunsnlem2lem2  14660  prmind2  14683  isprm5  14699  divgcdodd  14701  qmuldeneqnum  14744  divnumden  14745  numdensq  14751  hashdvds  14771  phiprmpw  14772  pythagtriplem4  14817  pythagtriplem19  14831  pcprendvds2  14839  pcpremul  14841  pceulem  14843  pcdiv  14850  pcqmul  14851  pc2dvds  14876  pcaddlem  14881  pcadd  14882  pcmpt2  14886  pcmptdvds  14887  pcbc  14893  expnprm  14895  prmpwdvds  14896  pockthlem  14897  prmreclem1  14908  prmreclem3  14910  prmreclem4  14911  4sqlem5  14934  4sqlem8  14937  4sqlem9  14938  4sqlem10  14939  mul4sqlem  14945  4sqlem12  14948  4sqlem14OLD  14950  4sqlem15OLD  14951  4sqlem16OLD  14952  4sqlem17OLD  14953  4sqlem14  14956  4sqlem15  14957  4sqlem16  14958  4sqlem17  14959  prmone0  15041  oddvds  17244  sylow1lem1  17298  sylow1lem4  17301  sylow1lem5  17302  sylow2blem3  17322  sylow3lem3  17329  sylow3lem4  17330  gexexlem  17538  ablfacrplem  17746  ablfacrp2  17748  ablfac1lem  17749  ablfac1b  17751  ablfac1eu  17754  pgpfac1lem3a  17757  pgpfac1lem3  17758  prmirredlem  19112  znrrg  19184  fvmptnn04ifa  19922  chfacfscmulgsum  19932  chfacfpmmulgsum  19936  lebnumlem3  22039  lebnumlem3OLD  22042  lebnumii  22045  ovollb2lem  22489  uniioombllem4  22592  dyadovol  22599  dyaddisjlem  22601  opnmbllem  22607  mbfi1fseqlem3  22723  mbfi1fseqlem4  22724  mbfi1fseqlem5  22725  mbfi1fseqlem6  22726  tdeglem4  23057  dgrcolem1  23275  dgrcolem2  23276  dvply1  23285  vieta1lem1  23311  vieta1lem2  23312  elqaalem2  23321  elqaalem3  23322  elqaalem2OLD  23324  elqaalem3OLD  23325  aalioulem1  23336  aalioulem2  23337  aaliou3lem9  23354  taylfvallem1  23360  tayl0  23365  taylply2  23371  taylply  23372  dvtaylp  23373  taylthlem2  23377  pserdvlem2  23431  advlogexp  23648  cxpmul2  23682  cxpeq  23745  atantayl3  23913  leibpi  23916  log2cnv  23918  log2tlbnd  23919  birthdaylem2  23926  birthdaylem3  23927  amgmlem  23963  amgm  23964  emcllem2  23970  emcllem5  23973  fsumharmonic  23985  zetacvg  23988  dmgmdivn0  24001  lgamgulmlem2  24003  lgamgulmlem3  24004  lgamgulmlem4  24005  lgamgulmlem5  24006  lgamgulmlem6  24007  lgamgulm2  24009  lgamcvg2  24028  gamcvg  24029  gamcvg2lem  24032  ftalem2  24046  ftalem4  24048  ftalem5  24049  ftalem4OLD  24050  ftalem5OLD  24051  basellem1  24055  basellem2  24056  basellem4  24058  basellem5  24059  basellem8  24062  sgmval2  24118  efchtdvds  24134  ppieq0  24151  dvdsdivcl  24158  fsumdvdsdiaglem  24160  dvdsflf1o  24164  muinv  24170  dvdsmulf1o  24171  chpchtsum  24195  logfaclbnd  24198  logexprlim  24201  mersenne  24203  perfectlem2  24206  perfect  24207  dchrabs  24236  bcmono  24253  bclbnd  24256  bposlem1  24260  bposlem2  24261  bposlem3  24262  bposlem6  24265  lgsval2lem  24282  lgseisenlem4  24328  lgsquadlem1  24330  lgsquadlem2  24331  lgsquad2lem1  24334  2sqlem3  24342  2sqlem8  24348  chebbnd1  24358  rplogsumlem2  24371  rpvmasumlem  24373  dchrisumlem1  24375  dchrmusum2  24380  dchrvmasumlem1  24381  dchrvmasum2lem  24382  dchrvmasum2if  24383  dchrvmasumlem3  24385  dchrvmasumiflem1  24387  dchrisum0flblem2  24395  mulogsumlem  24417  mulogsum  24418  mulog2sumlem2  24421  vmalogdivsum2  24424  vmalogdivsum  24425  logsqvma  24428  selberglem3  24433  selberg  24434  logdivbnd  24442  selberg3lem1  24443  selberg4lem1  24446  pntrsumo1  24451  selberg3r  24455  selberg4r  24456  selberg34r  24457  pntsval2  24462  pntrlog2bndlem2  24464  pntrlog2bndlem3  24465  pntrlog2bndlem5  24467  pntrlog2bndlem6  24469  pntpbnd1a  24471  pntpbnd1  24472  pntpbnd2  24473  padicabvf  24517  padicabvcxp  24518  ostth2  24523  ostth3  24524  bcm1n  28419  numdenneg  28428  2sqmod  28457  qqhf  28838  qqhghm  28840  qqhrhm  28841  qqhre  28872  oddpwdc  29235  signshnz  29528  subfacval2  29958  subfaclim  29959  cvmliftlem7  30062  cvmliftlem10  30065  cvmliftlem11  30066  cvmliftlem13  30067  bcprod  30422  iprodgam  30426  faclimlem1  30427  faclim2  30432  nn0prpwlem  31026  poimirlem17  32001  poimirlem20  32004  poimirlem23  32007  opnmbllem0  32020  irrapxlem4  35713  irrapxlem5  35714  pellexlem2  35718  pellexlem6  35722  jm2.27c  35906  itgpowd  36143  hashnzfzclim  36714  bcccl  36731  bccp1k  36733  bccm1k  36734  binomcxplemwb  36740  binomcxplemrat  36742  binomcxplemfrat  36743  mccllem  37714  clim1fr1  37716  dvnxpaek  37854  dvnprodlem2  37859  itgsinexp  37868  stoweidlem1  37898  stoweidlem11  37908  stoweidlem25  37922  stoweidlem26  37923  stoweidlem37  37935  stoweidlem38  37936  stoweidlem42  37940  stoweidlem51  37949  wallispilem4  37967  wallispilem5  37968  wallispi2lem1  37970  wallispi2lem2  37971  wallispi2  37972  stirlinglem4  37976  stirlinglem5  37977  stirlinglem12  37984  stirlinglem13  37985  sqwvfourb  38130  etransclem15  38151  etransclem20  38156  etransclem21  38157  etransclem22  38158  etransclem23  38159  etransclem24  38160  etransclem25  38161  etransclem31  38167  etransclem32  38168  etransclem33  38169  etransclem34  38170  etransclem35  38171  etransclem38  38174  etransclem41  38177  etransclem44  38180  etransclem45  38181  etransclem47  38183  etransclem48OLD  38184  etransclem48  38185  divgcdoddALTV  38848  perfectALTVlem2  38881  perfectALTV  38882  eluz2n0  40578  expnegico01  40587  fllogbd  40643  digexp  40690
  Copyright terms: Public domain W3C validator