Theorem nnne0d 12264

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

Syntax hints:   → wi 4   ∈ wcel 2143   ≠ wne 2958  0cc0 11074  ℕcn 12211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7719  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6289  df-ord 6350  df-on 6351  df-lim 6352  df-suc 6353  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-ov 7400  df-om 7848  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8382  df-er 8679  df-en 8929  df-dom 8930  df-sdom 8931  df-pnf 11219  df-mnf 11220  df-xr 11221  df-ltxr 11222  df-le 11223  df-nn 12212

This theorem is referenced by:  eluz2n0  12895  facne0  14300  bcn1  14327  bcm1k  14329  bcp1n  14330  bcp1nk  14331  bcval5  14332  bcpasc  14335  hashf1  14471  trireciplem  15893  trirecip  15894  geo2sum  15904  geo2lim  15906  mertenslem1  15915  fallfacval4  16074  bcfallfac  16075  bpolycl  16083  bpolysum  16084  bpolydiflem  16085  fsumkthpow  16087  efcllem  16108  ege2le3  16121  efcj  16123  efaddlem  16124  eftlub  16142  eirrlem  16237  ruclem7  16269  sqrt2irrlem  16281  bitsp1  16466  bitscmp  16473  sadcp1  16490  sadaddlem  16501  bitsres  16508  bitsuz  16509  bitsshft  16510  smupp1  16515  gcdnncl  16542  gcdeq0  16552  dvdsgcdidd  16572  mulgcd  16583  sqgcd  16597  expgcd  16598  lcmeq0  16635  lcmgcdlem  16641  lcmfeq0b  16665  lcmfunsnlem2lem1  16673  lcmfunsnlem2lem2  16674  divgcdcoprm0  16700  prmind2  16720  isprm5  16743  divgcdodd  16746  qmuldeneqnum  16783  divnumden  16784  numdensq  16790  numdenexp  16796  hashdvds  16811  phiprmpw  16812  pythagtriplem4  16856  pythagtriplem19  16870  pcprendvds2  16878  pcpremul  16880  pceulem  16882  pcdiv  16889  pcqmul  16890  pc2dvds  16916  dvdsprmpweqle  16923  pcaddlem  16925  pcadd  16926  pcmpt2  16930  pcmptdvds  16931  pcbc  16937  expnprm  16939  prmpwdvds  16941  pockthlem  16942  prmreclem1  16953  prmreclem3  16955  prmreclem4  16956  4sqlem5  16979  4sqlem8  16982  4sqlem9  16983  4sqlem10  16984  mul4sqlem  16990  4sqlem12  16993  4sqlem14  16995  4sqlem15  16996  4sqlem16  16997  4sqlem17  16998  prmone0  17072  oddvds  19588  sylow1lem1  19639  sylow1lem4  19642  sylow1lem5  19643  sylow2blem3  19663  sylow3lem3  19670  sylow3lem4  19671  gexexlem  19893  ablfacrplem  20108  ablfacrp2  20110  ablfac1lem  20111  ablfac1b  20113  ablfac1eu  20116  pgpfac1lem3a  20119  pgpfac1lem3  20120  fincygsubgodd  20155  fincygsubgodexd  20156  prmirredlem  21525  znrrg  21618  psdmul  22232  fvmptnn04ifa  22911  chfacfscmulgsum  22921  chfacfpmmulgsum  22925  lebnumlem3  25026  lebnumii  25029  ovollb2lem  25551  uniioombllem4  25649  dyadovol  25656  dyaddisjlem  25658  opnmbllem  25664  mbfi1fseqlem3  25780  mbfi1fseqlem4  25781  mbfi1fseqlem5  25782  mbfi1fseqlem6  25783  itgpowd  26113  tdeglem4  26121  dgrcolem1  26334  dgrcolem2  26335  dvply1  26349  vieta1lem1  26375  vieta1lem2  26376  elqaalem2  26385  elqaalem3  26386  aalioulem1  26397  aalioulem2  26398  aaliou3lem9  26415  taylfvallem1  26421  tayl0  26426  taylply2  26432  taylply  26433  dvtaylp  26434  taylthlem2  26438  pserdvlem2  26492  advlogexp  26721  cxpmul2  26755  cxpeq  26823  atantayl3  27005  leibpi  27008  log2cnv  27010  log2tlbnd  27011  birthdaylem2  27018  birthdaylem3  27019  amgmlem  27055  amgm  27056  emcllem2  27062  emcllem5  27065  fsumharmonic  27077  zetacvg  27080  dmgmdivn0  27093  lgamgulmlem2  27095  lgamgulmlem3  27096  lgamgulmlem4  27097  lgamgulmlem5  27098  lgamgulmlem6  27099  lgamgulm2  27101  lgamcvg2  27120  gamcvg  27121  gamcvg2lem  27124  ftalem2  27139  ftalem4  27141  ftalem5  27142  basellem1  27146  basellem2  27147  basellem4  27149  basellem5  27150  basellem8  27153  sgmval2  27208  efchtdvds  27224  ppieq0  27241  fsumdvdsdiaglem  27248  dvdsflf1o  27252  muinv  27258  mpodvdsmulf1o  27259  dvdsmulf1o  27261  chpchtsum  27284  logfaclbnd  27287  logexprlim  27290  mersenne  27292  perfectlem2  27295  perfect  27296  dchrabs  27325  bcmono  27342  bclbnd  27345  bposlem1  27349  bposlem2  27350  bposlem3  27351  bposlem6  27354  lgsval2lem  27372  lgsqr  27416  lgseisenlem4  27443  lgsquadlem1  27445  lgsquadlem2  27446  lgsquad2lem1  27449  2sqlem3  27485  2sqlem8  27491  2sqmod  27501  chebbnd1  27537  rplogsumlem2  27550  rpvmasumlem  27552  dchrisumlem1  27554  dchrmusum2  27559  dchrvmasumlem1  27560  dchrvmasum2lem  27561  dchrvmasum2if  27562  dchrvmasumlem3  27564  dchrvmasumiflem1  27566  dchrisum0flblem2  27574  mulogsumlem  27596  mulogsum  27597  mulog2sumlem2  27600  vmalogdivsum2  27603  vmalogdivsum  27604  logsqvma  27607  selberglem3  27612  selberg  27613  logdivbnd  27621  selberg3lem1  27622  selberg4lem1  27625  pntrsumo1  27630  selberg3r  27634  selberg4r  27635  selberg34r  27636  pntsval2  27641  pntrlog2bndlem2  27643  pntrlog2bndlem3  27644  pntrlog2bndlem5  27646  pntrlog2bndlem6  27648  pntpbnd1a  27650  pntpbnd1  27651  pntpbnd2  27652  padicabvf  27696  padicabvcxp  27697  ostth2  27702  ostth3  27703  clwwlknonex2  30312  numclwwlk1lem2foa  30557  numclwwlk1lem2fo  30561  nrt2irr  30676  bcm1n  32998  elq2  33015  numdenneg  33018  2exple2exp  33037  zringfrac  33751  cos9thpiminplylem2  34081  qqhf  34284  qqhghm  34286  qqhrhm  34287  qqhre  34318  oddpwdc  34652  signshnz  34886  hgt750lemb  34951  subfacval2  35538  subfaclim  35539  cvmliftlem7  35642  cvmliftlem10  35645  cvmliftlem11  35646  cvmliftlem13  35647  bcprod  36089  iprodgam  36093  faclimlem1  36094  faclim2  36099  nn0prpwlem  36683  knoppndvlem16  36966  poimirlem17  38137  poimirlem20  38140  poimirlem23  38143  opnmbllem0  38156  nnproddivdvdsd  42618  lcmineqlem6  42652  lcmineqlem10  42656  lcmineqlem11  42657  lcmineqlem12  42658  lcmineqlem15  42661  lcmineqlem16  42662  lcmineqlem18  42664  lcmineqlem23  42669  aks4d1p5  42698  aks4d1p7d1  42700  aks4d1p8  42705  aks6d1c1p3  42728  aks6d1c1  42734  aks6d1c2p2  42737  aks6d1c3  42741  aks6d1c4  42742  aks6d1c2lem4  42745  2np3bcnp1  42762  sticksstones10  42773  aks6d1c6lem3  42790  aks6d1c6lem4  42791  bcled  42796  bcle2d  42797  aks6d1c7lem1  42798  aks6d1c7  42802  unitscyglem2  42814  unitscyglem4  42816  fsuppind  43173  fltabcoprmex  43222  fltne  43227  flt4lem6  43241  nna4b4nsq  43243  fltnlta  43246  irrapxlem4  43403  irrapxlem5  43404  pellexlem2  43408  pellexlem6  43412  jm2.27c  43585  hashnzfzclim  44899  bcccl  44916  bccp1k  44918  bccm1k  44919  binomcxplemwb  44925  binomcxplemrat  44927  binomcxplemfrat  44928  mccllem  46174  clim1fr1  46178  dvnxpaek  46517  dvnprodlem2  46522  itgsinexp  46530  stoweidlem1  46576  stoweidlem11  46586  stoweidlem25  46600  stoweidlem26  46601  stoweidlem37  46612  stoweidlem38  46613  stoweidlem42  46617  stoweidlem51  46626  wallispilem4  46643  wallispilem5  46644  wallispi2lem1  46646  wallispi2lem2  46647  wallispi2  46648  stirlinglem4  46652  stirlinglem5  46653  stirlinglem12  46660  stirlinglem13  46661  sqwvfourb  46804  etransclem15  46824  etransclem20  46829  etransclem21  46830  etransclem22  46831  etransclem23  46832  etransclem24  46833  etransclem25  46834  etransclem31  46840  etransclem32  46841  etransclem33  46842  etransclem34  46843  etransclem35  46844  etransclem38  46847  etransclem41  46850  etransclem44  46853  etransclem45  46854  etransclem47  46856  etransclem48  46857  ovolval5lem1  47227  ovolval5lem2  47228  lighneallem4b  48219  ppivalnnnprmge6  48236  divgcdoddALTV  48305  perfectALTVlem2  48345  perfectALTV  48346  expnegico01  49141  fllogbd  49183  digexp  49230  amgmlemALT  50425