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

Theorem nnne0d 11103
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 11091 . 2 (𝐴 ∈ ℕ → 𝐴 ≠ 0)
31, 2syl 17 1 (𝜑𝐴 ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wne 2823  0cc0 9974  cn 11058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059
This theorem is referenced by:  eluz2n0  11766  facne0  13113  bcn1  13140  bcm1k  13142  bcp1n  13143  bcp1nk  13144  bcval5  13145  bcpasc  13148  hashf1  13279  trireciplem  14638  trirecip  14639  geo2sum  14648  geo2lim  14650  mertenslem1  14660  fallfacval4  14818  bcfallfac  14819  bpolycl  14827  bpolysum  14828  bpolydiflem  14829  fsumkthpow  14831  efcllem  14852  ege2le3  14864  efcj  14866  efaddlem  14867  eftlub  14883  eirrlem  14976  ruclem7  15009  sqrt2irrlem  15021  sqrt2irrlemOLD  15022  bitsp1  15200  bitscmp  15207  sadcp1  15224  sadaddlem  15235  bitsres  15242  bitsuz  15243  bitsshft  15244  smupp1  15249  gcdnncl  15276  gcdeq0  15285  mulgcd  15312  sqgcd  15325  lcmeq0  15360  lcmgcdlem  15366  lcmfeq0b  15390  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  divgcdcoprm0  15426  prmind2  15445  isprm5  15466  divgcdodd  15469  qmuldeneqnum  15502  divnumden  15503  numdensq  15509  hashdvds  15527  phiprmpw  15528  pythagtriplem4  15571  pythagtriplem19  15585  pcprendvds2  15593  pcpremul  15595  pceulem  15597  pcdiv  15604  pcqmul  15605  pc2dvds  15630  dvdsprmpweqle  15637  pcaddlem  15639  pcadd  15640  pcmpt2  15644  pcmptdvds  15645  pcbc  15651  expnprm  15653  prmpwdvds  15655  pockthlem  15656  prmreclem1  15667  prmreclem3  15669  prmreclem4  15670  4sqlem5  15693  4sqlem8  15696  4sqlem9  15697  4sqlem10  15698  mul4sqlem  15704  4sqlem12  15707  4sqlem14  15709  4sqlem15  15710  4sqlem16  15711  4sqlem17  15712  prmone0  15786  oddvds  18012  sylow1lem1  18059  sylow1lem4  18062  sylow1lem5  18063  sylow2blem3  18083  sylow3lem3  18090  sylow3lem4  18091  gexexlem  18301  ablfacrplem  18510  ablfacrp2  18512  ablfac1lem  18513  ablfac1b  18515  ablfac1eu  18518  pgpfac1lem3a  18521  pgpfac1lem3  18522  prmirredlem  19889  znrrg  19962  fvmptnn04ifa  20703  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  lebnumlem3  22809  lebnumii  22812  ovollb2lem  23302  uniioombllem4  23400  dyadovol  23407  dyaddisjlem  23409  opnmbllem  23415  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  tdeglem4  23865  dgrcolem1  24074  dgrcolem2  24075  dvply1  24084  vieta1lem1  24110  vieta1lem2  24111  elqaalem2  24120  elqaalem3  24121  aalioulem1  24132  aalioulem2  24133  aaliou3lem9  24150  taylfvallem1  24156  tayl0  24161  taylply2  24167  taylply  24168  dvtaylp  24169  taylthlem2  24173  pserdvlem2  24227  advlogexp  24446  cxpmul2  24480  cxpeq  24543  atantayl3  24711  leibpi  24714  log2cnv  24716  log2tlbnd  24717  birthdaylem2  24724  birthdaylem3  24725  amgmlem  24761  amgm  24762  emcllem2  24768  emcllem5  24771  fsumharmonic  24783  zetacvg  24786  dmgmdivn0  24799  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem4  24803  lgamgulmlem5  24804  lgamgulmlem6  24805  lgamgulm2  24807  lgamcvg2  24826  gamcvg  24827  gamcvg2lem  24830  ftalem2  24845  ftalem4  24847  ftalem5  24848  basellem1  24852  basellem2  24853  basellem4  24855  basellem5  24856  basellem8  24859  sgmval2  24914  efchtdvds  24930  ppieq0  24947  fsumdvdsdiaglem  24954  dvdsflf1o  24958  muinv  24964  dvdsmulf1o  24965  chpchtsum  24989  logfaclbnd  24992  logexprlim  24995  mersenne  24997  perfectlem2  25000  perfect  25001  dchrabs  25030  bcmono  25047  bclbnd  25050  bposlem1  25054  bposlem2  25055  bposlem3  25056  bposlem6  25059  lgsval2lem  25077  lgsqr  25121  lgseisenlem4  25148  lgsquadlem1  25150  lgsquadlem2  25151  lgsquad2lem1  25154  2sqlem3  25190  2sqlem8  25196  chebbnd1  25206  rplogsumlem2  25219  rpvmasumlem  25221  dchrisumlem1  25223  dchrmusum2  25228  dchrvmasumlem1  25229  dchrvmasum2lem  25230  dchrvmasum2if  25231  dchrvmasumlem3  25233  dchrvmasumiflem1  25235  dchrisum0flblem2  25243  mulogsumlem  25265  mulogsum  25266  mulog2sumlem2  25269  vmalogdivsum2  25272  vmalogdivsum  25273  logsqvma  25276  selberglem3  25281  selberg  25282  logdivbnd  25290  selberg3lem1  25291  selberg4lem1  25294  pntrsumo1  25299  selberg3r  25303  selberg4r  25304  selberg34r  25305  pntsval2  25310  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  padicabvf  25365  padicabvcxp  25366  ostth2  25371  ostth3  25372  clwwlknonex2  27084  numclwlk1lem2foa  27344  numclwlk1lem2fo  27348  bcm1n  29682  numdenneg  29691  2sqmod  29776  qqhf  30158  qqhghm  30160  qqhrhm  30161  qqhre  30192  oddpwdc  30544  signshnz  30796  hgt750lemb  30862  subfacval2  31295  subfaclim  31296  cvmliftlem7  31399  cvmliftlem10  31402  cvmliftlem11  31403  cvmliftlem13  31404  bcprod  31750  iprodgam  31754  faclimlem1  31755  faclim2  31760  nn0prpwlem  32442  knoppndvlem16  32643  poimirlem17  33556  poimirlem20  33559  poimirlem23  33562  opnmbllem0  33575  irrapxlem4  37706  irrapxlem5  37707  pellexlem2  37711  pellexlem6  37715  jm2.27c  37891  itgpowd  38117  hashnzfzclim  38838  bcccl  38855  bccp1k  38857  bccm1k  38858  binomcxplemwb  38864  binomcxplemrat  38866  binomcxplemfrat  38867  mccllem  40147  clim1fr1  40151  dvnxpaek  40475  dvnprodlem2  40480  itgsinexp  40488  stoweidlem1  40536  stoweidlem11  40546  stoweidlem25  40560  stoweidlem26  40561  stoweidlem37  40572  stoweidlem38  40573  stoweidlem42  40577  stoweidlem51  40586  wallispilem4  40603  wallispilem5  40604  wallispi2lem1  40606  wallispi2lem2  40607  wallispi2  40608  stirlinglem4  40612  stirlinglem5  40613  stirlinglem12  40620  stirlinglem13  40621  sqwvfourb  40764  etransclem15  40784  etransclem20  40789  etransclem21  40790  etransclem22  40791  etransclem23  40792  etransclem24  40793  etransclem25  40794  etransclem31  40800  etransclem32  40801  etransclem33  40802  etransclem34  40803  etransclem35  40804  etransclem38  40807  etransclem41  40810  etransclem44  40813  etransclem45  40814  etransclem47  40816  etransclem48  40817  ovolval5lem1  41187  ovolval5lem2  41188  lighneallem4b  41851  divgcdoddALTV  41918  perfectALTVlem2  41956  perfectALTV  41957  expnegico01  42633  fllogbd  42679  digexp  42726  amgmlemALT  42877
  Copyright terms: Public domain W3C validator