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

Theorem nnne0d 11679
Description: A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnge1d.1 (𝜑𝐴 ∈ ℕ)
Assertion
Ref Expression
nnne0d (𝜑𝐴 ≠ 0)

Proof of Theorem nnne0d
StepHypRef Expression
1 nnge1d.1 . 2 (𝜑𝐴 ∈ ℕ)
2 nnne0 11663 . 2 (𝐴 ∈ ℕ → 𝐴 ≠ 0)
31, 2syl 17 1 (𝜑𝐴 ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  wne 2990  0cc0 10530  cn 11629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-nn 11630
This theorem is referenced by:  eluz2n0  12280  facne0  13646  bcn1  13673  bcm1k  13675  bcp1n  13676  bcp1nk  13677  bcval5  13678  bcpasc  13681  hashf1  13815  trireciplem  15212  trirecip  15213  geo2sum  15224  geo2lim  15226  mertenslem1  15235  fallfacval4  15392  bcfallfac  15393  bpolycl  15401  bpolysum  15402  bpolydiflem  15403  fsumkthpow  15405  efcllem  15426  ege2le3  15438  efcj  15440  efaddlem  15441  eftlub  15457  eirrlem  15552  ruclem7  15584  sqrt2irrlem  15596  bitsp1  15773  bitscmp  15780  sadcp1  15797  sadaddlem  15808  bitsres  15815  bitsuz  15816  bitsshft  15817  smupp1  15822  gcdnncl  15849  gcdeq0  15858  dvdsgcdidd  15878  mulgcd  15889  sqgcd  15902  lcmeq0  15937  lcmgcdlem  15943  lcmfeq0b  15967  lcmfunsnlem2lem1  15975  lcmfunsnlem2lem2  15976  divgcdcoprm0  16002  prmind2  16022  isprm5  16044  divgcdodd  16047  qmuldeneqnum  16080  divnumden  16081  numdensq  16087  hashdvds  16105  phiprmpw  16106  pythagtriplem4  16149  pythagtriplem19  16163  pcprendvds2  16171  pcpremul  16173  pceulem  16175  pcdiv  16182  pcqmul  16183  pc2dvds  16208  dvdsprmpweqle  16215  pcaddlem  16217  pcadd  16218  pcmpt2  16222  pcmptdvds  16223  pcbc  16229  expnprm  16231  prmpwdvds  16233  pockthlem  16234  prmreclem1  16245  prmreclem3  16247  prmreclem4  16248  4sqlem5  16271  4sqlem8  16274  4sqlem9  16275  4sqlem10  16276  mul4sqlem  16282  4sqlem12  16285  4sqlem14  16287  4sqlem15  16288  4sqlem16  16289  4sqlem17  16290  prmone0  16364  oddvds  18670  sylow1lem1  18718  sylow1lem4  18721  sylow1lem5  18722  sylow2blem3  18742  sylow3lem3  18749  sylow3lem4  18750  gexexlem  18968  ablfacrplem  19183  ablfacrp2  19185  ablfac1lem  19186  ablfac1b  19188  ablfac1eu  19191  pgpfac1lem3a  19194  pgpfac1lem3  19195  fincygsubgodd  19230  fincygsubgodexd  19231  prmirredlem  20189  znrrg  20260  fvmptnn04ifa  21458  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  lebnumlem3  23571  lebnumii  23574  ovollb2lem  24095  uniioombllem4  24193  dyadovol  24200  dyaddisjlem  24202  opnmbllem  24208  mbfi1fseqlem3  24324  mbfi1fseqlem4  24325  mbfi1fseqlem5  24326  mbfi1fseqlem6  24327  itgpowd  24656  tdeglem4  24664  dgrcolem1  24873  dgrcolem2  24874  dvply1  24883  vieta1lem1  24909  vieta1lem2  24910  elqaalem2  24919  elqaalem3  24920  aalioulem1  24931  aalioulem2  24932  aaliou3lem9  24949  taylfvallem1  24955  tayl0  24960  taylply2  24966  taylply  24967  dvtaylp  24968  taylthlem2  24972  pserdvlem2  25026  advlogexp  25249  cxpmul2  25283  cxpeq  25349  atantayl3  25528  leibpi  25531  log2cnv  25533  log2tlbnd  25534  birthdaylem2  25541  birthdaylem3  25542  amgmlem  25578  amgm  25579  emcllem2  25585  emcllem5  25588  fsumharmonic  25600  zetacvg  25603  dmgmdivn0  25616  lgamgulmlem2  25618  lgamgulmlem3  25619  lgamgulmlem4  25620  lgamgulmlem5  25621  lgamgulmlem6  25622  lgamgulm2  25624  lgamcvg2  25643  gamcvg  25644  gamcvg2lem  25647  ftalem2  25662  ftalem4  25664  ftalem5  25665  basellem1  25669  basellem2  25670  basellem4  25672  basellem5  25673  basellem8  25676  sgmval2  25731  efchtdvds  25747  ppieq0  25764  fsumdvdsdiaglem  25771  dvdsflf1o  25775  muinv  25781  dvdsmulf1o  25782  chpchtsum  25806  logfaclbnd  25809  logexprlim  25812  mersenne  25814  perfectlem2  25817  perfect  25818  dchrabs  25847  bcmono  25864  bclbnd  25867  bposlem1  25871  bposlem2  25872  bposlem3  25873  bposlem6  25876  lgsval2lem  25894  lgsqr  25938  lgseisenlem4  25965  lgsquadlem1  25967  lgsquadlem2  25968  lgsquad2lem1  25971  2sqlem3  26007  2sqlem8  26013  2sqmod  26023  chebbnd1  26059  rplogsumlem2  26072  rpvmasumlem  26074  dchrisumlem1  26076  dchrmusum2  26081  dchrvmasumlem1  26082  dchrvmasum2lem  26083  dchrvmasum2if  26084  dchrvmasumlem3  26086  dchrvmasumiflem1  26088  dchrisum0flblem2  26096  mulogsumlem  26118  mulogsum  26119  mulog2sumlem2  26122  vmalogdivsum2  26125  vmalogdivsum  26126  logsqvma  26129  selberglem3  26134  selberg  26135  logdivbnd  26143  selberg3lem1  26144  selberg4lem1  26147  pntrsumo1  26152  selberg3r  26156  selberg4r  26157  selberg34r  26158  pntsval2  26163  pntrlog2bndlem2  26165  pntrlog2bndlem3  26166  pntrlog2bndlem5  26168  pntrlog2bndlem6  26170  pntpbnd1a  26172  pntpbnd1  26173  pntpbnd2  26174  padicabvf  26218  padicabvcxp  26219  ostth2  26224  ostth3  26225  clwwlknonex2  27897  numclwwlk1lem2foa  28142  numclwwlk1lem2fo  28146  bcm1n  30547  numdenneg  30562  qqhf  31335  qqhghm  31337  qqhrhm  31338  qqhre  31369  oddpwdc  31720  signshnz  31969  hgt750lemb  32035  subfacval2  32542  subfaclim  32543  cvmliftlem7  32646  cvmliftlem10  32649  cvmliftlem11  32650  cvmliftlem13  32651  bcprod  33078  iprodgam  33082  faclimlem1  33083  faclim2  33088  nn0prpwlem  33778  knoppndvlem16  33974  poimirlem17  35067  poimirlem20  35070  poimirlem23  35073  opnmbllem0  35086  nnproddivdvdsd  39282  lcmineqlem6  39315  lcmineqlem10  39319  lcmineqlem11  39320  lcmineqlem12  39321  lcmineqlem15  39324  lcmineqlem16  39325  lcmineqlem18  39327  lcmineqlem23  39332  2np3bcnp1  39339  fsuppind  39443  expgcd  39478  numdenexp  39481  zrtelqelz  39487  fltne  39603  fltnlta  39606  irrapxlem4  39753  irrapxlem5  39754  pellexlem2  39758  pellexlem6  39762  jm2.27c  39935  hashnzfzclim  41013  bcccl  41030  bccp1k  41032  bccm1k  41033  binomcxplemwb  41039  binomcxplemrat  41041  binomcxplemfrat  41042  mccllem  42226  clim1fr1  42230  dvnxpaek  42571  dvnprodlem2  42576  itgsinexp  42584  stoweidlem1  42630  stoweidlem11  42640  stoweidlem25  42654  stoweidlem26  42655  stoweidlem37  42666  stoweidlem38  42667  stoweidlem42  42671  stoweidlem51  42680  wallispilem4  42697  wallispilem5  42698  wallispi2lem1  42700  wallispi2lem2  42701  wallispi2  42702  stirlinglem4  42706  stirlinglem5  42707  stirlinglem12  42714  stirlinglem13  42715  sqwvfourb  42858  etransclem15  42878  etransclem20  42883  etransclem21  42884  etransclem22  42885  etransclem23  42886  etransclem24  42887  etransclem25  42888  etransclem31  42894  etransclem32  42895  etransclem33  42896  etransclem34  42897  etransclem35  42898  etransclem38  42901  etransclem41  42904  etransclem44  42907  etransclem45  42908  etransclem47  42910  etransclem48  42911  ovolval5lem1  43278  ovolval5lem2  43279  lighneallem4b  44114  divgcdoddALTV  44187  perfectALTVlem2  44227  perfectALTV  44228  expnegico01  44914  fllogbd  44961  digexp  45008  amgmlemALT  45318
  Copyright terms: Public domain W3C validator