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

Theorem nnne0d 11277
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 11265 . 2 (𝐴 ∈ ℕ → 𝐴 ≠ 0)
31, 2syl 17 1 (𝜑𝐴 ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  wne 2932  0cc0 10148  cn 11232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-nn 11233
This theorem is referenced by:  eluz2n0  11941  facne0  13287  bcn1  13314  bcm1k  13316  bcp1n  13317  bcp1nk  13318  bcval5  13319  bcpasc  13322  hashf1  13453  trireciplem  14813  trirecip  14814  geo2sum  14823  geo2lim  14825  mertenslem1  14835  fallfacval4  14993  bcfallfac  14994  bpolycl  15002  bpolysum  15003  bpolydiflem  15004  fsumkthpow  15006  efcllem  15027  ege2le3  15039  efcj  15041  efaddlem  15042  eftlub  15058  eirrlem  15151  ruclem7  15184  sqrt2irrlem  15196  sqrt2irrlemOLD  15197  bitsp1  15375  bitscmp  15382  sadcp1  15399  sadaddlem  15410  bitsres  15417  bitsuz  15418  bitsshft  15419  smupp1  15424  gcdnncl  15451  gcdeq0  15460  mulgcd  15487  sqgcd  15500  lcmeq0  15535  lcmgcdlem  15541  lcmfeq0b  15565  lcmfunsnlem2lem1  15573  lcmfunsnlem2lem2  15574  divgcdcoprm0  15601  prmind2  15620  isprm5  15641  divgcdodd  15644  qmuldeneqnum  15677  divnumden  15678  numdensq  15684  hashdvds  15702  phiprmpw  15703  pythagtriplem4  15746  pythagtriplem19  15760  pcprendvds2  15768  pcpremul  15770  pceulem  15772  pcdiv  15779  pcqmul  15780  pc2dvds  15805  dvdsprmpweqle  15812  pcaddlem  15814  pcadd  15815  pcmpt2  15819  pcmptdvds  15820  pcbc  15826  expnprm  15828  prmpwdvds  15830  pockthlem  15831  prmreclem1  15842  prmreclem3  15844  prmreclem4  15845  4sqlem5  15868  4sqlem8  15871  4sqlem9  15872  4sqlem10  15873  mul4sqlem  15879  4sqlem12  15882  4sqlem14  15884  4sqlem15  15885  4sqlem16  15886  4sqlem17  15887  prmone0  15961  oddvds  18186  sylow1lem1  18233  sylow1lem4  18236  sylow1lem5  18237  sylow2blem3  18257  sylow3lem3  18264  sylow3lem4  18265  gexexlem  18475  ablfacrplem  18684  ablfacrp2  18686  ablfac1lem  18687  ablfac1b  18689  ablfac1eu  18692  pgpfac1lem3a  18695  pgpfac1lem3  18696  prmirredlem  20063  znrrg  20136  fvmptnn04ifa  20877  chfacfscmulgsum  20887  chfacfpmmulgsum  20891  lebnumlem3  22983  lebnumii  22986  ovollb2lem  23476  uniioombllem4  23574  dyadovol  23581  dyaddisjlem  23583  opnmbllem  23589  mbfi1fseqlem3  23703  mbfi1fseqlem4  23704  mbfi1fseqlem5  23705  mbfi1fseqlem6  23706  tdeglem4  24039  dgrcolem1  24248  dgrcolem2  24249  dvply1  24258  vieta1lem1  24284  vieta1lem2  24285  elqaalem2  24294  elqaalem3  24295  aalioulem1  24306  aalioulem2  24307  aaliou3lem9  24324  taylfvallem1  24330  tayl0  24335  taylply2  24341  taylply  24342  dvtaylp  24343  taylthlem2  24347  pserdvlem2  24401  advlogexp  24621  cxpmul2  24655  cxpeq  24718  atantayl3  24886  leibpi  24889  log2cnv  24891  log2tlbnd  24892  birthdaylem2  24899  birthdaylem3  24900  amgmlem  24936  amgm  24937  emcllem2  24943  emcllem5  24946  fsumharmonic  24958  zetacvg  24961  dmgmdivn0  24974  lgamgulmlem2  24976  lgamgulmlem3  24977  lgamgulmlem4  24978  lgamgulmlem5  24979  lgamgulmlem6  24980  lgamgulm2  24982  lgamcvg2  25001  gamcvg  25002  gamcvg2lem  25005  ftalem2  25020  ftalem4  25022  ftalem5  25023  basellem1  25027  basellem2  25028  basellem4  25030  basellem5  25031  basellem8  25034  sgmval2  25089  efchtdvds  25105  ppieq0  25122  fsumdvdsdiaglem  25129  dvdsflf1o  25133  muinv  25139  dvdsmulf1o  25140  chpchtsum  25164  logfaclbnd  25167  logexprlim  25170  mersenne  25172  perfectlem2  25175  perfect  25176  dchrabs  25205  bcmono  25222  bclbnd  25225  bposlem1  25229  bposlem2  25230  bposlem3  25231  bposlem6  25234  lgsval2lem  25252  lgsqr  25296  lgseisenlem4  25323  lgsquadlem1  25325  lgsquadlem2  25326  lgsquad2lem1  25329  2sqlem3  25365  2sqlem8  25371  chebbnd1  25381  rplogsumlem2  25394  rpvmasumlem  25396  dchrisumlem1  25398  dchrmusum2  25403  dchrvmasumlem1  25404  dchrvmasum2lem  25405  dchrvmasum2if  25406  dchrvmasumlem3  25408  dchrvmasumiflem1  25410  dchrisum0flblem2  25418  mulogsumlem  25440  mulogsum  25441  mulog2sumlem2  25444  vmalogdivsum2  25447  vmalogdivsum  25448  logsqvma  25451  selberglem3  25456  selberg  25457  logdivbnd  25465  selberg3lem1  25466  selberg4lem1  25469  pntrsumo1  25474  selberg3r  25478  selberg4r  25479  selberg34r  25480  pntsval2  25485  pntrlog2bndlem2  25487  pntrlog2bndlem3  25488  pntrlog2bndlem5  25490  pntrlog2bndlem6  25492  pntpbnd1a  25494  pntpbnd1  25495  pntpbnd2  25496  padicabvf  25540  padicabvcxp  25541  ostth2  25546  ostth3  25547  clwwlknonex2  27279  numclwlk1lem2foa  27534  numclwlk1lem2fo  27538  bcm1n  29884  numdenneg  29893  2sqmod  29978  qqhf  30360  qqhghm  30362  qqhrhm  30363  qqhre  30394  oddpwdc  30746  signshnz  30998  hgt750lemb  31064  subfacval2  31497  subfaclim  31498  cvmliftlem7  31601  cvmliftlem10  31604  cvmliftlem11  31605  cvmliftlem13  31606  bcprod  31952  iprodgam  31956  faclimlem1  31957  faclim2  31962  nn0prpwlem  32644  knoppndvlem16  32845  poimirlem17  33757  poimirlem20  33760  poimirlem23  33763  opnmbllem0  33776  irrapxlem4  37909  irrapxlem5  37910  pellexlem2  37914  pellexlem6  37918  jm2.27c  38094  itgpowd  38320  hashnzfzclim  39041  bcccl  39058  bccp1k  39060  bccm1k  39061  binomcxplemwb  39067  binomcxplemrat  39069  binomcxplemfrat  39070  mccllem  40350  clim1fr1  40354  dvnxpaek  40678  dvnprodlem2  40683  itgsinexp  40691  stoweidlem1  40739  stoweidlem11  40749  stoweidlem25  40763  stoweidlem26  40764  stoweidlem37  40775  stoweidlem38  40776  stoweidlem42  40780  stoweidlem51  40789  wallispilem4  40806  wallispilem5  40807  wallispi2lem1  40809  wallispi2lem2  40810  wallispi2  40811  stirlinglem4  40815  stirlinglem5  40816  stirlinglem12  40823  stirlinglem13  40824  sqwvfourb  40967  etransclem15  40987  etransclem20  40992  etransclem21  40993  etransclem22  40994  etransclem23  40995  etransclem24  40996  etransclem25  40997  etransclem31  41003  etransclem32  41004  etransclem33  41005  etransclem34  41006  etransclem35  41007  etransclem38  41010  etransclem41  41013  etransclem44  41016  etransclem45  41017  etransclem47  41019  etransclem48  41020  ovolval5lem1  41390  ovolval5lem2  41391  lighneallem4b  42054  divgcdoddALTV  42121  perfectALTVlem2  42159  perfectALTV  42160  expnegico01  42836  fllogbd  42882  digexp  42929  amgmlemALT  43080
  Copyright terms: Public domain W3C validator