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

Theorem nnne0d 10623
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 10611 . 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 1844    =/= wne 2600   0cc0 9524   NNcn 10578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-resscn 9581  ax-1cn 9582  ax-icn 9583  ax-addcl 9584  ax-addrcl 9585  ax-mulcl 9586  ax-mulrcl 9587  ax-mulcom 9588  ax-addass 9589  ax-mulass 9590  ax-distr 9591  ax-i2m1 9592  ax-1ne0 9593  ax-1rid 9594  ax-rnegex 9595  ax-rrecex 9596  ax-cnre 9597  ax-pre-lttri 9598  ax-pre-lttrn 9599  ax-pre-ltadd 9600  ax-pre-mulgt0 9601
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-nel 2603  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-iun 4275  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-riota 6242  df-ov 6283  df-oprab 6284  df-mpt2 6285  df-om 6686  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-er 7350  df-en 7557  df-dom 7558  df-sdom 7559  df-pnf 9662  df-mnf 9663  df-xr 9664  df-ltxr 9665  df-le 9666  df-sub 9845  df-neg 9846  df-nn 10579
This theorem is referenced by:  facne0  12410  bcn1  12437  bcm1k  12439  bcp1n  12440  bcp1nk  12441  bcval5  12442  bcpasc  12445  hashf1  12557  trireciplem  13827  trirecip  13828  geo2sum  13836  geo2lim  13838  mertenslem1  13847  fallfacval4  13990  bcfallfac  13991  bpolycl  13999  bpolysum  14000  bpolydiflem  14001  fsumkthpow  14003  efcllem  14024  ege2le3  14036  efcj  14038  efaddlem  14039  eftlub  14055  eirrlem  14148  ruclem7  14180  sqr2irrlem  14192  bitsp1  14292  bitscmp  14299  sadcp1  14316  sadaddlem  14327  bitsres  14334  bitsuz  14335  bitsshft  14336  smupp1  14341  gcdeq0  14370  mulgcd  14395  sqgcd  14407  prmind2  14439  isprm5  14464  divgcdodd  14471  qmuldeneqnum  14491  divnumden  14492  numdensq  14498  hashdvds  14516  phiprmpw  14517  pythagtriplem4  14554  pythagtriplem19  14568  pcprendvds2  14576  pcpremul  14578  pceulem  14580  pcdiv  14587  pcqmul  14588  pc2dvds  14613  pcaddlem  14618  pcadd  14619  pcmpt2  14623  pcmptdvds  14624  pcbc  14630  expnprm  14632  prmpwdvds  14633  pockthlem  14634  prmreclem1  14645  prmreclem3  14647  prmreclem4  14648  4sqlem5  14671  4sqlem8  14674  4sqlem9  14675  4sqlem10  14676  mul4sqlem  14682  4sqlem12  14685  4sqlem14  14687  4sqlem15  14688  4sqlem16  14689  4sqlem17  14690  oddvds  16897  sylow1lem1  16944  sylow1lem4  16947  sylow1lem5  16948  sylow2blem3  16968  sylow3lem3  16975  sylow3lem4  16976  gexexlem  17184  ablfacrplem  17438  ablfacrp2  17440  ablfac1lem  17441  ablfac1b  17443  ablfac1eu  17446  pgpfac1lem3a  17449  pgpfac1lem3  17450  prmirredlem  18832  znrrg  18904  fvmptnn04ifa  19645  chfacfscmulgsum  19655  chfacfpmmulgsum  19659  lebnumlem3  21757  lebnumii  21760  ovollb2lem  22193  uniioombllem4  22289  dyadovol  22296  dyaddisjlem  22298  opnmbllem  22304  mbfi1fseqlem3  22418  mbfi1fseqlem4  22419  mbfi1fseqlem5  22420  mbfi1fseqlem6  22421  tdeglem4  22752  dgrcolem1  22964  dgrcolem2  22965  dvply1  22974  vieta1lem1  23000  vieta1lem2  23001  elqaalem2  23010  elqaalem3  23011  aalioulem1  23022  aalioulem2  23023  aaliou3lem9  23040  taylfvallem1  23046  tayl0  23051  taylply2  23057  taylply  23058  dvtaylp  23059  taylthlem2  23063  pserdvlem2  23117  advlogexp  23332  cxpmul2  23366  cxpeq  23429  atantayl3  23597  leibpi  23600  log2cnv  23602  log2tlbnd  23603  birthdaylem2  23610  birthdaylem3  23611  amgmlem  23647  amgm  23648  emcllem2  23654  emcllem5  23657  fsumharmonic  23669  zetacvg  23672  dmgmdivn0  23685  lgamgulmlem2  23687  lgamgulmlem3  23688  lgamgulmlem4  23689  lgamgulmlem5  23690  lgamgulmlem6  23691  lgamgulm2  23693  lgamcvg2  23712  gamcvg  23713  gamcvg2lem  23716  ftalem2  23730  ftalem4  23732  ftalem5  23733  basellem1  23737  basellem2  23738  basellem4  23740  basellem5  23741  basellem8  23744  sgmval2  23800  efchtdvds  23816  ppieq0  23833  dvdsdivcl  23840  fsumdvdsdiaglem  23842  dvdsflf1o  23846  muinv  23852  dvdsmulf1o  23853  chpchtsum  23877  logfaclbnd  23880  logexprlim  23883  mersenne  23885  perfectlem2  23888  perfect  23889  dchrabs  23918  bcmono  23935  bclbnd  23938  bposlem1  23942  bposlem2  23943  bposlem3  23944  bposlem6  23947  lgsval2lem  23964  lgseisenlem4  24010  lgsquadlem1  24012  lgsquadlem2  24013  lgsquad2lem1  24016  2sqlem3  24024  2sqlem8  24030  chebbnd1  24040  rplogsumlem2  24053  rpvmasumlem  24055  dchrisumlem1  24057  dchrmusum2  24062  dchrvmasumlem1  24063  dchrvmasum2lem  24064  dchrvmasum2if  24065  dchrvmasumlem3  24067  dchrvmasumiflem1  24069  dchrisum0flblem2  24077  mulogsumlem  24099  mulogsum  24100  mulog2sumlem2  24103  vmalogdivsum2  24106  vmalogdivsum  24107  logsqvma  24110  selberglem3  24115  selberg  24116  logdivbnd  24124  selberg3lem1  24125  selberg4lem1  24128  pntrsumo1  24133  selberg3r  24137  selberg4r  24138  selberg34r  24139  pntsval2  24144  pntrlog2bndlem2  24146  pntrlog2bndlem3  24147  pntrlog2bndlem5  24149  pntrlog2bndlem6  24151  pntpbnd1a  24153  pntpbnd1  24154  pntpbnd2  24155  padicabvf  24199  padicabvcxp  24200  ostth2  24205  ostth3  24206  bcm1n  28061  gcdnncl  28071  numdenneg  28072  2sqmod  28101  qqhf  28432  qqhghm  28434  qqhrhm  28435  qqhre  28463  oddpwdc  28812  signshnz  29067  subfacval2  29497  subfaclim  29498  cvmliftlem7  29601  cvmliftlem10  29604  cvmliftlem11  29605  cvmliftlem13  29606  bcprod  29960  iprodgam  29964  faclimlem1  29965  faclim2  29970  nn0prpwlem  30563  opnmbllem0  31435  irrapxlem4  35135  irrapxlem5  35136  pellexlem2  35140  pellexlem6  35144  jm2.27c  35324  itgpowd  35559  lcmeq0  36067  lcmgcdlem  36073  hashnzfzclim  36088  bcccl  36105  bccp1k  36107  bccm1k  36108  binomcxplemwb  36114  binomcxplemrat  36116  binomcxplemfrat  36117  mccllem  36986  clim1fr1  36988  dvnxpaek  37120  dvnprodlem2  37125  itgsinexp  37134  stoweidlem1  37164  stoweidlem11  37174  stoweidlem25  37188  stoweidlem26  37189  stoweidlem37  37200  stoweidlem38  37201  stoweidlem42  37205  stoweidlem51  37214  wallispilem4  37231  wallispilem5  37232  wallispi2lem1  37234  wallispi2lem2  37235  wallispi2  37236  stirlinglem4  37240  stirlinglem5  37241  stirlinglem12  37248  stirlinglem13  37249  sqwvfourb  37393  etransclem15  37413  etransclem20  37418  etransclem21  37419  etransclem22  37420  etransclem23  37421  etransclem24  37422  etransclem25  37423  etransclem31  37429  etransclem32  37430  etransclem33  37431  etransclem34  37432  etransclem35  37433  etransclem38  37436  etransclem41  37439  etransclem44  37442  etransclem45  37443  etransclem47  37445  etransclem48  37446  divgcdoddALTV  37777  perfectALTVlem2  37810  perfectALTV  37811  eluz2n0  38638  expnegico01  38647  fllogbd  38704  digexp  38751
  Copyright terms: Public domain W3C validator