Theorem nnne0d 12398

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

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nnne0 12382	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝐴 ≠ 0)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2958  0cc0 11210  ℕcn 12345

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-i2m1 11278  ax-1ne0 11279  ax-1rid 11280  ax-rnegex 11281  ax-rrecex 11282  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285  ax-pre-ltadd 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6310  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-ov 7430  df-om 7885  df-2nd 8009  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-rdg 8429  df-er 8728  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359  df-nn 12346

This theorem is used by:  eluz2n0  13030  facne0  14440  bcn1  14467  bcm1k  14469  bcp1n  14470  bcp1nk  14471  bcval5  14472  bcpasc  14475  hashf1  14612  trireciplem  16043  trirecip  16044  geo2sum  16054  geo2lim  16056  mertenslem1  16065  fallfacval4  16221  bcfallfac  16222  bpolycl  16230  bpolysum  16231  bpolydiflem  16232  fsumkthpow  16234  efcllem  16255  ege2le3  16268  efcj  16270  efaddlem  16271  eftlub  16289  eirrlem  16384  ruclem7  16416  sqrt2irrlem  16428  bitsp1  16613  bitscmp  16620  sadcp1  16637  sadaddlem  16648  bitsres  16655  bitsuz  16656  bitsshft  16657  smupp1  16662  gcdnncl  16689  gcdeq0  16701  dvdsgcdidd  16722  mulgcd  16733  sqgcd  16748  expgcd  16749  lcmeq0  16787  lcmgcdlem  16793  lcmfeq0b  16817  lcmfunsnlem2lem1  16825  lcmfunsnlem2lem2  16826  divgcdcoprm0  16852  prmind2  16872  isprm5  16895  divgcdodd  16898  qmuldeneqnum  16935  divnumden  16936  numdensq  16942  numdenexp  16949  hashdvds  16964  phiprmpw  16965  pythagtriplem4  17009  pythagtriplem19  17023  pcprendvds2  17031  pcpremul  17033  pceulem  17035  pcdiv  17042  pcqmul  17043  pc2dvds  17069  dvdsprmpweqle  17076  pcaddlem  17078  pcadd  17079  pcmpt2  17083  pcmptdvds  17084  pcbc  17090  expnprm  17092  prmpwdvds  17094  pockthlem  17095  prmreclem1  17106  prmreclem3  17108  prmreclem4  17109  4sqlem5  17132  4sqlem8  17135  4sqlem9  17136  4sqlem10  17137  mul4sqlem  17143  4sqlem12  17146  4sqlem14  17148  4sqlem15  17149  4sqlem16  17150  4sqlem17  17151  prmone0  17225  oddvds  19773  sylow1lem1  19824  sylow1lem4  19827  sylow1lem5  19828  sylow2blem3  19848  sylow3lem3  19855  sylow3lem4  19856  gexexlem  20078  ablfacrplem  20293  ablfacrp2  20295  ablfac1lem  20296  ablfac1b  20298  ablfac1eu  20301  pgpfac1lem3a  20304  pgpfac1lem3  20305  fincygsubgodd  20340  fincygsubgodexd  20341  prmirredlem  21790  znrrg  21883  psdmul  22499  fvmptnn04ifa  23180  chfacfscmulgsum  23190  chfacfpmmulgsum  23194  lebnumlem3  25296  lebnumii  25299  ovollb2lem  25821  uniioombllem4  25919  dyadovol  25926  dyaddisjlem  25928  opnmbllem  25934  mbfi1fseqlem3  26050  mbfi1fseqlem4  26051  mbfi1fseqlem5  26052  mbfi1fseqlem6  26053  itgpowd  26382  tdeglem4  26390  dgrcolem1  26604  dgrcolem2  26605  dvply1  26617  vieta1lem1  26645  vieta1lem2  26646  elqaalem2  26655  elqaalem3  26656  aalioulem1  26671  aalioulem2  26672  aaliou3lem9  26689  taylfvallem1  26696  tayl0  26701  taylply2  26707  taylply  26708  dvtaylp  26709  taylthlem2  26713  pserdvlem2  26767  advlogexp  26995  cxpmul2  27029  cxpeq  27097  atantayl3  27279  leibpi  27282  log2cnv  27284  log2tlbnd  27285  birthdaylem2  27292  birthdaylem3  27293  amgmlem  27329  amgm  27330  emcllem2  27336  emcllem5  27339  fsumharmonic  27351  zetacvg  27354  dmgmdivn0  27367  lgamgulmlem2  27369  lgamgulmlem3  27370  lgamgulmlem4  27371  lgamgulmlem5  27372  lgamgulmlem6  27373  lgamgulm2  27375  lgamcvg2  27394  gamcvg  27395  gamcvg2lem  27398  ftalem2  27413  ftalem4  27415  ftalem5  27416  basellem1  27420  basellem2  27421  basellem4  27423  basellem5  27424  basellem8  27427  sgmval2  27482  efchtdvds  27498  ppieq0  27515  fsumdvdsdiaglem  27522  dvdsflf1o  27526  muinv  27532  mpodvdsmulf1o  27533  dvdsmulf1o  27535  chpchtsum  27558  logfaclbnd  27561  logexprlim  27564  mersenne  27566  perfectlem2  27569  perfect  27570  dchrabs  27599  bcmono  27616  bclbnd  27619  bposlem1  27623  bposlem2  27624  bposlem3  27625  bposlem6  27628  lgsval2lem  27646  lgsqr  27690  lgseisenlem4  27717  lgsquadlem1  27719  lgsquadlem2  27720  lgsquad2lem1  27723  2sqlem3  27759  2sqlem8  27765  2sqmod  27775  chebbnd1  27811  rplogsumlem2  27824  rpvmasumlem  27826  dchrisumlem1  27828  dchrmusum2  27833  dchrvmasumlem1  27834  dchrvmasum2lem  27835  dchrvmasum2if  27836  dchrvmasumlem3  27838  dchrvmasumiflem1  27840  dchrisum0flblem2  27848  mulogsumlem  27870  mulogsum  27871  mulog2sumlem2  27874  vmalogdivsum2  27877  vmalogdivsum  27878  logsqvma  27881  selberglem3  27886  selberg  27887  logdivbnd  27895  selberg3lem1  27896  selberg4lem1  27899  pntrsumo1  27904  selberg3r  27908  selberg4r  27909  selberg34r  27910  pntsval2  27915  pntrlog2bndlem2  27917  pntrlog2bndlem3  27918  pntrlog2bndlem5  27920  pntrlog2bndlem6  27922  pntpbnd1a  27924  pntpbnd1  27925  pntpbnd2  27926  padicabvf  27970  padicabvcxp  27971  ostth2  27976  ostth3  27977  fltabcoprmex  27983  fltne  27987  flt4lem6  28000  nna4b4nsq  28002  clwwlknonex2  30712  numclwwlk1lem2foa  30967  numclwwlk1lem2fo  30971  nrt2irr  31086  bcm1n  33440  elq2  33456  numdenneg  33459  2exple2exp  33478  zringfrac  34139  cos9thpiminplylem2  34468  qqhf  34671  qqhghm  34673  qqhrhm  34674  qqhre  34705  oddpwdc  35039  signshnz  35273  hgt750lemb  35338  subfacval2  36073  subfaclim  36074  cvmliftlem7  36177  cvmliftlem10  36180  cvmliftlem11  36181  cvmliftlem13  36182  bcprod  36630  iprodgam  36634  faclimlem1  36635  faclim2  36640  nn0prpwlem  37237  knoppndvlem16  37520  poimirlem17  38695  poimirlem20  38698  poimirlem23  38701  opnmbllem0  38714  nnproddivdvdsd  43190  lcmineqlem6  43224  lcmineqlem10  43228  lcmineqlem11  43229  lcmineqlem12  43230  lcmineqlem15  43233  lcmineqlem16  43234  lcmineqlem18  43236  lcmineqlem23  43241  aks4d1p5  43270  aks4d1p7d1  43272  aks4d1p8  43277  aks6d1c1p3  43300  aks6d1c1  43306  aks6d1c2p2  43309  aks6d1c3  43313  aks6d1c4  43314  aks6d1c2lem4  43317  2np3bcnp1  43334  sticksstones10  43345  aks6d1c6lem3  43362  aks6d1c6lem4  43363  bcled  43368  bcle2d  43369  aks6d1c7lem1  43370  aks6d1c7  43374  unitscyglem2  43386  unitscyglem4  43388  fsuppind  43758  fltnlta  43814  irrapxlem4  43972  irrapxlem5  43973  pellexlem2  43977  pellexlem6  43981  jm2.27c  44154  hashnzfzclim  45446  bcccl  45463  bccp1k  45465  bccm1k  45466  binomcxplemwb  45472  binomcxplemrat  45474  binomcxplemfrat  45475  mccllem  46748  clim1fr1  46752  dvnxpaek  47091  dvnprodlem2  47096  itgsinexp  47104  stoweidlem1  47150  stoweidlem11  47160  stoweidlem25  47174  stoweidlem26  47175  stoweidlem37  47186  stoweidlem38  47187  stoweidlem42  47191  stoweidlem51  47200  wallispilem4  47217  wallispilem5  47218  wallispi2lem1  47220  wallispi2lem2  47221  wallispi2  47222  stirlinglem4  47226  stirlinglem5  47227  stirlinglem12  47234  stirlinglem13  47235  sqwvfourb  47378  etransclem15  47398  etransclem20  47403  etransclem21  47404  etransclem22  47405  etransclem23  47406  etransclem24  47407  etransclem25  47408  etransclem31  47414  etransclem32  47415  etransclem33  47416  etransclem34  47417  etransclem35  47418  etransclem38  47421  etransclem41  47424  etransclem44  47427  etransclem45  47428  etransclem47  47430  etransclem48  47431  ovolval5lem1  47801  ovolval5lem2  47802  lighneallem4b  48833  ppivalnnnprmge6  48850  divgcdoddALTV  48919  perfectALTVlem2  48959  perfectALTV  48960  expnegico01  49769  fllogbd  49811  digexp  49858  amgmlemALT  51202