Theorem nnne0d 12303

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2960  0cc0 11117  ℕcn 12250

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-nn 12251

This theorem is used by:  eluz2n0  12935  facne0  14342  bcn1  14369  bcm1k  14371  bcp1n  14372  bcp1nk  14373  bcval5  14374  bcpasc  14377  hashf1  14514  trireciplem  15941  trirecip  15942  geo2sum  15952  geo2lim  15954  mertenslem1  15963  fallfacval4  16121  bcfallfac  16122  bpolycl  16130  bpolysum  16131  bpolydiflem  16132  fsumkthpow  16134  efcllem  16155  ege2le3  16168  efcj  16170  efaddlem  16171  eftlub  16189  eirrlem  16284  ruclem7  16316  sqrt2irrlem  16328  bitsp1  16513  bitscmp  16520  sadcp1  16537  sadaddlem  16548  bitsres  16555  bitsuz  16556  bitsshft  16557  smupp1  16562  gcdnncl  16589  gcdeq0  16599  dvdsgcdidd  16619  mulgcd  16630  sqgcd  16644  expgcd  16645  lcmeq0  16682  lcmgcdlem  16688  lcmfeq0b  16712  lcmfunsnlem2lem1  16720  lcmfunsnlem2lem2  16721  divgcdcoprm0  16747  prmind2  16767  isprm5  16790  divgcdodd  16793  qmuldeneqnum  16830  divnumden  16831  numdensq  16837  numdenexp  16843  hashdvds  16858  phiprmpw  16859  pythagtriplem4  16903  pythagtriplem19  16917  pcprendvds2  16925  pcpremul  16927  pceulem  16929  pcdiv  16936  pcqmul  16937  pc2dvds  16963  dvdsprmpweqle  16970  pcaddlem  16972  pcadd  16973  pcmpt2  16977  pcmptdvds  16978  pcbc  16984  expnprm  16986  prmpwdvds  16988  pockthlem  16989  prmreclem1  17000  prmreclem3  17002  prmreclem4  17003  4sqlem5  17026  4sqlem8  17029  4sqlem9  17030  4sqlem10  17031  mul4sqlem  17037  4sqlem12  17040  4sqlem14  17042  4sqlem15  17043  4sqlem16  17044  4sqlem17  17045  prmone0  17119  oddvds  19663  sylow1lem1  19714  sylow1lem4  19717  sylow1lem5  19718  sylow2blem3  19738  sylow3lem3  19745  sylow3lem4  19746  gexexlem  19968  ablfacrplem  20183  ablfacrp2  20185  ablfac1lem  20186  ablfac1b  20188  ablfac1eu  20191  pgpfac1lem3a  20194  pgpfac1lem3  20195  fincygsubgodd  20230  fincygsubgodexd  20231  prmirredlem  21674  znrrg  21767  psdmul  22381  fvmptnn04ifa  23059  chfacfscmulgsum  23069  chfacfpmmulgsum  23073  lebnumlem3  25175  lebnumii  25178  ovollb2lem  25700  uniioombllem4  25798  dyadovol  25805  dyaddisjlem  25807  opnmbllem  25813  mbfi1fseqlem3  25929  mbfi1fseqlem4  25930  mbfi1fseqlem5  25931  mbfi1fseqlem6  25932  itgpowd  26262  tdeglem4  26270  dgrcolem1  26483  dgrcolem2  26484  dvply1  26498  vieta1lem1  26524  vieta1lem2  26525  elqaalem2  26534  elqaalem3  26535  aalioulem1  26548  aalioulem2  26549  aaliou3lem9  26566  taylfvallem1  26573  tayl0  26578  taylply2  26584  taylply  26585  dvtaylp  26586  taylthlem2  26590  pserdvlem2  26644  advlogexp  26873  cxpmul2  26907  cxpeq  26975  atantayl3  27157  leibpi  27160  log2cnv  27162  log2tlbnd  27163  birthdaylem2  27170  birthdaylem3  27171  amgmlem  27207  amgm  27208  emcllem2  27214  emcllem5  27217  fsumharmonic  27229  zetacvg  27232  dmgmdivn0  27245  lgamgulmlem2  27247  lgamgulmlem3  27248  lgamgulmlem4  27249  lgamgulmlem5  27250  lgamgulmlem6  27251  lgamgulm2  27253  lgamcvg2  27272  gamcvg  27273  gamcvg2lem  27276  ftalem2  27291  ftalem4  27293  ftalem5  27294  basellem1  27298  basellem2  27299  basellem4  27301  basellem5  27302  basellem8  27305  sgmval2  27360  efchtdvds  27376  ppieq0  27393  fsumdvdsdiaglem  27400  dvdsflf1o  27404  muinv  27410  mpodvdsmulf1o  27411  dvdsmulf1o  27413  chpchtsum  27436  logfaclbnd  27439  logexprlim  27442  mersenne  27444  perfectlem2  27447  perfect  27448  dchrabs  27477  bcmono  27494  bclbnd  27497  bposlem1  27501  bposlem2  27502  bposlem3  27503  bposlem6  27506  lgsval2lem  27524  lgsqr  27568  lgseisenlem4  27595  lgsquadlem1  27597  lgsquadlem2  27598  lgsquad2lem1  27601  2sqlem3  27637  2sqlem8  27643  2sqmod  27653  chebbnd1  27689  rplogsumlem2  27702  rpvmasumlem  27704  dchrisumlem1  27706  dchrmusum2  27711  dchrvmasumlem1  27712  dchrvmasum2lem  27713  dchrvmasum2if  27714  dchrvmasumlem3  27716  dchrvmasumiflem1  27718  dchrisum0flblem2  27726  mulogsumlem  27748  mulogsum  27749  mulog2sumlem2  27752  vmalogdivsum2  27755  vmalogdivsum  27756  logsqvma  27759  selberglem3  27764  selberg  27765  logdivbnd  27773  selberg3lem1  27774  selberg4lem1  27777  pntrsumo1  27782  selberg3r  27786  selberg4r  27787  selberg34r  27788  pntsval2  27793  pntrlog2bndlem2  27795  pntrlog2bndlem3  27796  pntrlog2bndlem5  27798  pntrlog2bndlem6  27800  pntpbnd1a  27802  pntpbnd1  27803  pntpbnd2  27804  padicabvf  27848  padicabvcxp  27849  ostth2  27854  ostth3  27855  clwwlknonex2  30529  numclwwlk1lem2foa  30778  numclwwlk1lem2fo  30782  nrt2irr  30897  bcm1n  33212  elq2  33228  numdenneg  33231  2exple2exp  33250  zringfrac  33910  cos9thpiminplylem2  34239  qqhf  34442  qqhghm  34444  qqhrhm  34445  qqhre  34476  oddpwdc  34811  signshnz  35045  hgt750lemb  35110  subfacval2  35718  subfaclim  35719  cvmliftlem7  35822  cvmliftlem10  35825  cvmliftlem11  35826  cvmliftlem13  35827  bcprod  36269  iprodgam  36273  faclimlem1  36274  faclim2  36279  nn0prpwlem  36892  knoppndvlem16  37175  poimirlem17  38347  poimirlem20  38350  poimirlem23  38353  opnmbllem0  38366  nnproddivdvdsd  42827  lcmineqlem6  42861  lcmineqlem10  42865  lcmineqlem11  42866  lcmineqlem12  42867  lcmineqlem15  42870  lcmineqlem16  42871  lcmineqlem18  42873  lcmineqlem23  42878  aks4d1p5  42907  aks4d1p7d1  42909  aks4d1p8  42914  aks6d1c1p3  42937  aks6d1c1  42943  aks6d1c2p2  42946  aks6d1c3  42950  aks6d1c4  42951  aks6d1c2lem4  42954  2np3bcnp1  42971  sticksstones10  42982  aks6d1c6lem3  42999  aks6d1c6lem4  43000  bcled  43005  bcle2d  43006  aks6d1c7lem1  43007  aks6d1c7  43011  unitscyglem2  43023  unitscyglem4  43025  fsuppind  43382  fltabcoprmex  43431  fltne  43436  flt4lem6  43450  nna4b4nsq  43452  fltnlta  43455  irrapxlem4  43612  irrapxlem5  43613  pellexlem2  43617  pellexlem6  43621  jm2.27c  43794  hashnzfzclim  45092  bcccl  45109  bccp1k  45111  bccm1k  45112  binomcxplemwb  45118  binomcxplemrat  45120  binomcxplemfrat  45121  mccllem  46373  clim1fr1  46377  dvnxpaek  46716  dvnprodlem2  46721  itgsinexp  46729  stoweidlem1  46775  stoweidlem11  46785  stoweidlem25  46799  stoweidlem26  46800  stoweidlem37  46811  stoweidlem38  46812  stoweidlem42  46816  stoweidlem51  46825  wallispilem4  46842  wallispilem5  46843  wallispi2lem1  46845  wallispi2lem2  46846  wallispi2  46847  stirlinglem4  46851  stirlinglem5  46852  stirlinglem12  46859  stirlinglem13  46860  sqwvfourb  47003  etransclem15  47023  etransclem20  47028  etransclem21  47029  etransclem22  47030  etransclem23  47031  etransclem24  47032  etransclem25  47033  etransclem31  47039  etransclem32  47040  etransclem33  47041  etransclem34  47042  etransclem35  47043  etransclem38  47046  etransclem41  47049  etransclem44  47052  etransclem45  47053  etransclem47  47055  etransclem48  47056  ovolval5lem1  47426  ovolval5lem2  47427  lighneallem4b  48421  ppivalnnnprmge6  48438  divgcdoddALTV  48507  perfectALTVlem2  48547  perfectALTV  48548  expnegico01  49357  fllogbd  49399  digexp  49446  amgmlemALT  50710