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

Theorem nnne0d 11676
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 11660 . 2 (𝐴 ∈ ℕ → 𝐴 ≠ 0)
31, 2syl 17 1 (𝜑𝐴 ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wne 3016  0cc0 10526  cn 11627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7148  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-nn 11628
This theorem is referenced by:  eluz2n0  12277  facne0  13636  bcn1  13663  bcm1k  13665  bcp1n  13666  bcp1nk  13667  bcval5  13668  bcpasc  13671  hashf1  13805  trireciplem  15207  trirecip  15208  geo2sum  15219  geo2lim  15221  mertenslem1  15230  fallfacval4  15387  bcfallfac  15388  bpolycl  15396  bpolysum  15397  bpolydiflem  15398  fsumkthpow  15400  efcllem  15421  ege2le3  15433  efcj  15435  efaddlem  15436  eftlub  15452  eirrlem  15547  ruclem7  15579  sqrt2irrlem  15591  bitsp1  15770  bitscmp  15777  sadcp1  15794  sadaddlem  15805  bitsres  15812  bitsuz  15813  bitsshft  15814  smupp1  15819  gcdnncl  15846  gcdeq0  15855  dvdsgcdidd  15875  mulgcd  15886  sqgcd  15899  lcmeq0  15934  lcmgcdlem  15940  lcmfeq0b  15964  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  divgcdcoprm0  15999  prmind2  16019  isprm5  16041  divgcdodd  16044  qmuldeneqnum  16077  divnumden  16078  numdensq  16084  hashdvds  16102  phiprmpw  16103  pythagtriplem4  16146  pythagtriplem19  16160  pcprendvds2  16168  pcpremul  16170  pceulem  16172  pcdiv  16179  pcqmul  16180  pc2dvds  16205  dvdsprmpweqle  16212  pcaddlem  16214  pcadd  16215  pcmpt2  16219  pcmptdvds  16220  pcbc  16226  expnprm  16228  prmpwdvds  16230  pockthlem  16231  prmreclem1  16242  prmreclem3  16244  prmreclem4  16245  4sqlem5  16268  4sqlem8  16271  4sqlem9  16272  4sqlem10  16273  mul4sqlem  16279  4sqlem12  16282  4sqlem14  16284  4sqlem15  16285  4sqlem16  16286  4sqlem17  16287  prmone0  16361  oddvds  18606  sylow1lem1  18654  sylow1lem4  18657  sylow1lem5  18658  sylow2blem3  18678  sylow3lem3  18685  sylow3lem4  18686  gexexlem  18903  ablfacrplem  19118  ablfacrp2  19120  ablfac1lem  19121  ablfac1b  19123  ablfac1eu  19126  pgpfac1lem3a  19129  pgpfac1lem3  19130  fincygsubgodd  19165  fincygsubgodexd  19166  prmirredlem  20570  znrrg  20642  fvmptnn04ifa  21388  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  lebnumlem3  23496  lebnumii  23499  ovollb2lem  24018  uniioombllem4  24116  dyadovol  24123  dyaddisjlem  24125  opnmbllem  24131  mbfi1fseqlem3  24247  mbfi1fseqlem4  24248  mbfi1fseqlem5  24249  mbfi1fseqlem6  24250  tdeglem4  24583  dgrcolem1  24792  dgrcolem2  24793  dvply1  24802  vieta1lem1  24828  vieta1lem2  24829  elqaalem2  24838  elqaalem3  24839  aalioulem1  24850  aalioulem2  24851  aaliou3lem9  24868  taylfvallem1  24874  tayl0  24879  taylply2  24885  taylply  24886  dvtaylp  24887  taylthlem2  24891  pserdvlem2  24945  advlogexp  25165  cxpmul2  25199  cxpeq  25265  atantayl3  25444  leibpi  25448  log2cnv  25450  log2tlbnd  25451  birthdaylem2  25458  birthdaylem3  25459  amgmlem  25495  amgm  25496  emcllem2  25502  emcllem5  25505  fsumharmonic  25517  zetacvg  25520  dmgmdivn0  25533  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamgulmlem4  25537  lgamgulmlem5  25538  lgamgulmlem6  25539  lgamgulm2  25541  lgamcvg2  25560  gamcvg  25561  gamcvg2lem  25564  ftalem2  25579  ftalem4  25581  ftalem5  25582  basellem1  25586  basellem2  25587  basellem4  25589  basellem5  25590  basellem8  25593  sgmval2  25648  efchtdvds  25664  ppieq0  25681  fsumdvdsdiaglem  25688  dvdsflf1o  25692  muinv  25698  dvdsmulf1o  25699  chpchtsum  25723  logfaclbnd  25726  logexprlim  25729  mersenne  25731  perfectlem2  25734  perfect  25735  dchrabs  25764  bcmono  25781  bclbnd  25784  bposlem1  25788  bposlem2  25789  bposlem3  25790  bposlem6  25793  lgsval2lem  25811  lgsqr  25855  lgseisenlem4  25882  lgsquadlem1  25884  lgsquadlem2  25885  lgsquad2lem1  25888  2sqlem3  25924  2sqlem8  25930  2sqmod  25940  chebbnd1  25976  rplogsumlem2  25989  rpvmasumlem  25991  dchrisumlem1  25993  dchrmusum2  25998  dchrvmasumlem1  25999  dchrvmasum2lem  26000  dchrvmasum2if  26001  dchrvmasumlem3  26003  dchrvmasumiflem1  26005  dchrisum0flblem2  26013  mulogsumlem  26035  mulogsum  26036  mulog2sumlem2  26039  vmalogdivsum2  26042  vmalogdivsum  26043  logsqvma  26046  selberglem3  26051  selberg  26052  logdivbnd  26060  selberg3lem1  26061  selberg4lem1  26064  pntrsumo1  26069  selberg3r  26073  selberg4r  26074  selberg34r  26075  pntsval2  26080  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntpbnd1a  26089  pntpbnd1  26090  pntpbnd2  26091  padicabvf  26135  padicabvcxp  26136  ostth2  26141  ostth3  26142  clwwlknonex2  27816  numclwwlk1lem2foa  28061  numclwwlk1lem2fo  28065  bcm1n  30445  numdenneg  30460  qqhf  31127  qqhghm  31129  qqhrhm  31130  qqhre  31161  oddpwdc  31512  signshnz  31761  hgt750lemb  31827  subfacval2  32332  subfaclim  32333  cvmliftlem7  32436  cvmliftlem10  32439  cvmliftlem11  32440  cvmliftlem13  32441  bcprod  32868  iprodgam  32872  faclimlem1  32873  faclim2  32878  nn0prpwlem  33568  knoppndvlem16  33764  poimirlem17  34791  poimirlem20  34794  poimirlem23  34797  opnmbllem0  34810  expgcd  39063  numdenexp  39066  zrtelqelz  39072  fltne  39152  fltnlta  39155  irrapxlem4  39302  irrapxlem5  39303  pellexlem2  39307  pellexlem6  39311  jm2.27c  39484  itgpowd  39701  hashnzfzclim  40534  bcccl  40551  bccp1k  40553  bccm1k  40554  binomcxplemwb  40560  binomcxplemrat  40562  binomcxplemfrat  40563  mccllem  41758  clim1fr1  41762  dvnxpaek  42107  dvnprodlem2  42112  itgsinexp  42120  stoweidlem1  42167  stoweidlem11  42177  stoweidlem25  42191  stoweidlem26  42192  stoweidlem37  42203  stoweidlem38  42204  stoweidlem42  42208  stoweidlem51  42217  wallispilem4  42234  wallispilem5  42235  wallispi2lem1  42237  wallispi2lem2  42238  wallispi2  42239  stirlinglem4  42243  stirlinglem5  42244  stirlinglem12  42251  stirlinglem13  42252  sqwvfourb  42395  etransclem15  42415  etransclem20  42420  etransclem21  42421  etransclem22  42422  etransclem23  42423  etransclem24  42424  etransclem25  42425  etransclem31  42431  etransclem32  42432  etransclem33  42433  etransclem34  42434  etransclem35  42435  etransclem38  42438  etransclem41  42441  etransclem44  42444  etransclem45  42445  etransclem47  42447  etransclem48  42448  ovolval5lem1  42815  ovolval5lem2  42816  lighneallem4b  43621  divgcdoddALTV  43694  perfectALTVlem2  43734  perfectALTV  43735  expnegico01  44471  fllogbd  44518  digexp  44565  amgmlemALT  44802
  Copyright terms: Public domain W3C validator