Theorem nnne0 10642

Description: A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.)

Assertion

Ref	Expression
nnne0	|- ( A e. NN -> A =/= 0 )

Proof of Theorem nnne0

Step	Hyp	Ref	Expression
1		0nnn 10641	. . 3 |- -. 0 e. NN
2		eleq1 2501	. . 3 |- ( A = 0 -> ( A e. NN <-> 0 e. NN ) )
3	1, 2	mtbiri 304	. 2 |- ( A = 0 -> -. A e. NN )
4	3	necon2ai 2666	1 |- ( A e. NN -> A =/= 0 )

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1870   =/= wne 2625   0cc0 9538   NNcn 10609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-nn 10610

This theorem is referenced by:  nndivre  10645  nndiv  10650  nndivtr  10651  nnne0d  10654  zdiv  11006  zdivadd  11007  zdivmul  11008  elq  11266  qmulz  11267  qre  11269  qaddcl  11280  qnegcl  11281  qmulcl  11282  qreccl  11284  rpnnen1lem5  11294  fzo1fzo0n0  11955  quoremz  12079  quoremnn0ALT  12081  intfracq  12083  fldiv  12084  fldiv2  12085  modmulnn  12111  modidmul0OLD  12120  expnnval  12272  expneg  12277  digit2  12402  facdiv  12469  facndiv  12470  bcm1k  12497  bcp1n  12498  bcval5  12500  hashnncl  12544  cshwidxmod  12890  relexpsucnnr  13067  divcnv  13889  harmonic  13895  expcnv  13900  ef0lem  14111  ruclem6  14265  sqrt2irr  14279  dvdsval3  14287  nndivdvds  14289  dvdseq  14330  divalg2  14361  divalgmod  14362  ndvdssub  14363  nndvdslegcd  14453  modgcd  14474  gcddiv  14488  gcdeq  14491  sqgcd  14497  eucalgf  14513  eucalginv  14514  lcmgcdlem  14542  lcmftp  14580  divgcdodd  14624  qredeq  14634  qredeu  14635  isprm6  14637  divnumden  14668  divdenle  14669  phimullem  14696  pythagtriplem10  14733  pythagtriplem8  14736  pythagtriplem9  14737  pythagtriplem19  14746  pccl  14762  pcdiv  14765  pcqcl  14769  pcdvds  14776  pcndvds  14778  pcndvds2  14780  pceq0  14783  pcneg  14786  pcz  14793  pcmpt  14800  fldivp1  14805  pcfac  14807  infpnlem2  14818  cshwshashlem1  15029  mulgnn  16715  mulgnegnn  16719  oddvdsnn0  17135  odmulgeq  17146  gexnnod  17175  cply1coe0  18828  cply1coe0bi  18829  qsssubdrg  18962  prmirredlem  18995  znf1o  19053  znhash  19060  znidomb  19063  znunithash  19066  znrrg  19067  m2cpm  19696  m2cpminvid2lem  19709  fvmptnn04ifc  19807  vitali  22448  mbfi1fseqlem3  22552  dvexp2  22785  plyeq0lem  23032  abelthlem9  23260  logtayllem  23469  logtayl  23470  logtaylsum  23471  logtayl2  23472  cxpexp  23478  cxproot  23500  root1id  23559  root1eq1  23560  cxpeq  23562  atantayl  23728  atantayl2  23729  leibpilem2  23732  leibpi  23733  birthdaylem2  23743  birthdaylem3  23744  dfef2  23761  emcllem2  23787  emcllem3  23788  zetacvg  23805  lgam1  23854  basellem4  23873  basellem5  23874  basellem8  23877  basellem9  23878  mumullem2  23970  dvdsflip  23974  fsumdvdscom  23977  chtublem  24002  dchrelbas4  24034  bclbnd  24071  lgsval4a  24109  lgsabs1  24125  lgssq  24126  lgssq2  24127  dchrmusumlema  24194  dchrmusum2  24195  dchrvmasumiflem1  24202  dchrvmaeq0  24205  dchrisum0flblem1  24209  dchrisum0flblem2  24210  dchrisum0re  24214  ostthlem1  24328  ostth1  24334  cyclnspth  25204  clwwisshclwwlem  25379  gxpval  25832  gxmodid  25852  ipasslem4  26320  ipasslem5  26321  divnumden2  28219  qqhval2  28625  qqhnm  28633  signstfveq0  29254  subfacp1lem6  29696  circum  30106  fz0n  30151  divcnvlin  30154  iprodgam  30165  faclim  30169  nndivsub  30902  poimirlem29  31673  poimirlem31  31675  poimirlem32  31676  heiborlem4  31850  heiborlem6  31852  pellexlem1  35383  congrep  35529  jm2.20nn  35558  hashgcdlem  35773  phisum  35775  proot1ex  35777  hashnzfzclim  36308  binomcxplemnotnn0  36342  nnne1ge2  37114  mccllem  37249  clim1fr1  37251  dvnxpaek  37386  dvnprodlem2  37391  wallispilem5  37500  wallispi2lem1  37502  stirlinglem1  37505  stirlinglem3  37507  stirlinglem4  37508  stirlinglem5  37509  stirlinglem7  37511  stirlinglem10  37514  stirlinglem12  37516  stirlinglem14  37518  stirlinglem15  37519  fouriersw  37663  iccpartiltu  38126  gcdzeq  38183  divgcdoddALTV  38201  nnsgrpnmnd  38576  eluz2cnn0n1  39067  mod0mul  39083  modn0mul  39084  blennn  39147  nnpw2blen  39152  digvalnn0  39171  nn0digval  39172  dignn0fr  39173  dignn0ldlem  39174  dig0  39178