Theorem nnne0d 12313

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 12297	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝐴 ≠ 0)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2955  0cc0 11127  ℕcn 12260

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7417  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-nn 12261

This theorem is used by:  eluz2n0  12945  facne0  14353  bcn1  14380  bcm1k  14382  bcp1n  14383  bcp1nk  14384  bcval5  14385  bcpasc  14388  hashf1  14525  trireciplem  15954  trirecip  15955  geo2sum  15965  geo2lim  15967  mertenslem1  15976  fallfacval4  16132  bcfallfac  16133  bpolycl  16141  bpolysum  16142  bpolydiflem  16143  fsumkthpow  16145  efcllem  16166  ege2le3  16179  efcj  16181  efaddlem  16182  eftlub  16200  eirrlem  16295  ruclem7  16327  sqrt2irrlem  16339  bitsp1  16524  bitscmp  16531  sadcp1  16548  sadaddlem  16559  bitsres  16566  bitsuz  16567  bitsshft  16568  smupp1  16573  gcdnncl  16600  gcdeq0  16610  dvdsgcdidd  16630  mulgcd  16641  sqgcd  16655  expgcd  16656  lcmeq0  16693  lcmgcdlem  16699  lcmfeq0b  16723  lcmfunsnlem2lem1  16731  lcmfunsnlem2lem2  16732  divgcdcoprm0  16758  prmind2  16778  isprm5  16801  divgcdodd  16804  qmuldeneqnum  16841  divnumden  16842  numdensq  16848  numdenexp  16854  hashdvds  16869  phiprmpw  16870  pythagtriplem4  16914  pythagtriplem19  16928  pcprendvds2  16936  pcpremul  16938  pceulem  16940  pcdiv  16947  pcqmul  16948  pc2dvds  16974  dvdsprmpweqle  16981  pcaddlem  16983  pcadd  16984  pcmpt2  16988  pcmptdvds  16989  pcbc  16995  expnprm  16997  prmpwdvds  16999  pockthlem  17000  prmreclem1  17011  prmreclem3  17013  prmreclem4  17014  4sqlem5  17037  4sqlem8  17040  4sqlem9  17041  4sqlem10  17042  mul4sqlem  17048  4sqlem12  17051  4sqlem14  17053  4sqlem15  17054  4sqlem16  17055  4sqlem17  17056  prmone0  17130  oddvds  19677  sylow1lem1  19728  sylow1lem4  19731  sylow1lem5  19732  sylow2blem3  19752  sylow3lem3  19759  sylow3lem4  19760  gexexlem  19982  ablfacrplem  20197  ablfacrp2  20199  ablfac1lem  20200  ablfac1b  20202  ablfac1eu  20205  pgpfac1lem3a  20208  pgpfac1lem3  20209  fincygsubgodd  20244  fincygsubgodexd  20245  prmirredlem  21688  znrrg  21781  psdmul  22397  fvmptnn04ifa  23078  chfacfscmulgsum  23088  chfacfpmmulgsum  23092  lebnumlem3  25194  lebnumii  25197  ovollb2lem  25719  uniioombllem4  25817  dyadovol  25824  dyaddisjlem  25826  opnmbllem  25832  mbfi1fseqlem3  25948  mbfi1fseqlem4  25949  mbfi1fseqlem5  25950  mbfi1fseqlem6  25951  itgpowd  26280  tdeglem4  26288  dgrcolem1  26502  dgrcolem2  26503  dvply1  26517  vieta1lem1  26545  vieta1lem2  26546  elqaalem2  26555  elqaalem3  26556  aalioulem1  26571  aalioulem2  26572  aaliou3lem9  26589  taylfvallem1  26596  tayl0  26601  taylply2  26607  taylply  26608  dvtaylp  26609  taylthlem2  26613  pserdvlem2  26667  advlogexp  26895  cxpmul2  26929  cxpeq  26997  atantayl3  27179  leibpi  27182  log2cnv  27184  log2tlbnd  27185  birthdaylem2  27192  birthdaylem3  27193  amgmlem  27229  amgm  27230  emcllem2  27236  emcllem5  27239  fsumharmonic  27251  zetacvg  27254  dmgmdivn0  27267  lgamgulmlem2  27269  lgamgulmlem3  27270  lgamgulmlem4  27271  lgamgulmlem5  27272  lgamgulmlem6  27273  lgamgulm2  27275  lgamcvg2  27294  gamcvg  27295  gamcvg2lem  27298  ftalem2  27313  ftalem4  27315  ftalem5  27316  basellem1  27320  basellem2  27321  basellem4  27323  basellem5  27324  basellem8  27327  sgmval2  27382  efchtdvds  27398  ppieq0  27415  fsumdvdsdiaglem  27422  dvdsflf1o  27426  muinv  27432  mpodvdsmulf1o  27433  dvdsmulf1o  27435  chpchtsum  27458  logfaclbnd  27461  logexprlim  27464  mersenne  27466  perfectlem2  27469  perfect  27470  dchrabs  27499  bcmono  27516  bclbnd  27519  bposlem1  27523  bposlem2  27524  bposlem3  27525  bposlem6  27528  lgsval2lem  27546  lgsqr  27590  lgseisenlem4  27617  lgsquadlem1  27619  lgsquadlem2  27620  lgsquad2lem1  27623  2sqlem3  27659  2sqlem8  27665  2sqmod  27675  chebbnd1  27711  rplogsumlem2  27724  rpvmasumlem  27726  dchrisumlem1  27728  dchrmusum2  27733  dchrvmasumlem1  27734  dchrvmasum2lem  27735  dchrvmasum2if  27736  dchrvmasumlem3  27738  dchrvmasumiflem1  27740  dchrisum0flblem2  27748  mulogsumlem  27770  mulogsum  27771  mulog2sumlem2  27774  vmalogdivsum2  27777  vmalogdivsum  27778  logsqvma  27781  selberglem3  27786  selberg  27787  logdivbnd  27795  selberg3lem1  27796  selberg4lem1  27799  pntrsumo1  27804  selberg3r  27808  selberg4r  27809  selberg34r  27810  pntsval2  27815  pntrlog2bndlem2  27817  pntrlog2bndlem3  27818  pntrlog2bndlem5  27820  pntrlog2bndlem6  27822  pntpbnd1a  27824  pntpbnd1  27825  pntpbnd2  27826  padicabvf  27870  padicabvcxp  27871  ostth2  27876  ostth3  27877  clwwlknonex2  30582  numclwwlk1lem2foa  30837  numclwwlk1lem2fo  30841  nrt2irr  30956  bcm1n  33269  elq2  33285  numdenneg  33288  2exple2exp  33307  zringfrac  33967  cos9thpiminplylem2  34296  qqhf  34499  qqhghm  34501  qqhrhm  34502  qqhre  34533  oddpwdc  34868  signshnz  35102  hgt750lemb  35167  subfacval2  35769  subfaclim  35770  cvmliftlem7  35873  cvmliftlem10  35876  cvmliftlem11  35877  cvmliftlem13  35878  bcprod  36320  iprodgam  36324  faclimlem1  36325  faclim2  36330  nn0prpwlem  36944  knoppndvlem16  37227  poimirlem17  38389  poimirlem20  38392  poimirlem23  38395  opnmbllem0  38408  nnproddivdvdsd  42869  lcmineqlem6  42903  lcmineqlem10  42907  lcmineqlem11  42908  lcmineqlem12  42909  lcmineqlem15  42912  lcmineqlem16  42913  lcmineqlem18  42915  lcmineqlem23  42920  aks4d1p5  42949  aks4d1p7d1  42951  aks4d1p8  42956  aks6d1c1p3  42979  aks6d1c1  42985  aks6d1c2p2  42988  aks6d1c3  42992  aks6d1c4  42993  aks6d1c2lem4  42996  2np3bcnp1  43013  sticksstones10  43024  aks6d1c6lem3  43041  aks6d1c6lem4  43042  bcled  43047  bcle2d  43048  aks6d1c7lem1  43049  aks6d1c7  43053  unitscyglem2  43065  unitscyglem4  43067  fsuppind  43439  fltabcoprmex  43488  fltne  43493  flt4lem6  43507  nna4b4nsq  43509  fltnlta  43512  irrapxlem4  43669  irrapxlem5  43670  pellexlem2  43674  pellexlem6  43678  jm2.27c  43851  hashnzfzclim  45149  bcccl  45166  bccp1k  45168  bccm1k  45169  binomcxplemwb  45175  binomcxplemrat  45177  binomcxplemfrat  45178  mccllem  46430  clim1fr1  46434  dvnxpaek  46773  dvnprodlem2  46778  itgsinexp  46786  stoweidlem1  46832  stoweidlem11  46842  stoweidlem25  46856  stoweidlem26  46857  stoweidlem37  46868  stoweidlem38  46869  stoweidlem42  46873  stoweidlem51  46882  wallispilem4  46899  wallispilem5  46900  wallispi2lem1  46902  wallispi2lem2  46903  wallispi2  46904  stirlinglem4  46908  stirlinglem5  46909  stirlinglem12  46916  stirlinglem13  46917  sqwvfourb  47060  etransclem15  47080  etransclem20  47085  etransclem21  47086  etransclem22  47087  etransclem23  47088  etransclem24  47089  etransclem25  47090  etransclem31  47096  etransclem32  47097  etransclem33  47098  etransclem34  47099  etransclem35  47100  etransclem38  47103  etransclem41  47106  etransclem44  47109  etransclem45  47110  etransclem47  47112  etransclem48  47113  ovolval5lem1  47483  ovolval5lem2  47484  lighneallem4b  48515  ppivalnnnprmge6  48532  divgcdoddALTV  48601  perfectALTVlem2  48641  perfectALTV  48642  expnegico01  49451  fllogbd  49493  digexp  49540  amgmlemALT  50824