Theorem nnne0 10650

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 10649	. . 3 |- -. 0 e. NN
2		eleq1 2495	. . 3 |- ( A = 0 -> ( A e. NN <-> 0 e. NN ) )
3	1, 2	mtbiri 304	. 2 |- ( A = 0 -> -. A e. NN )
4	3	necon2ai 2655	1 |- ( A e. NN -> A =/= 0 )

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1872   =/= wne 2614   0cc0 9547   NNcn 10617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624

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 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  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 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-er 7375  df-en 7582  df-dom 7583  df-sdom 7584  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-nn 10618

This theorem is referenced by:  nndivre  10653  nndiv  10658  nndivtr  10659  nnne0d  10662  zdiv  11014  zdivadd  11015  zdivmul  11016  elq  11274  qmulz  11275  qre  11277  qaddcl  11288  qnegcl  11289  qmulcl  11290  qreccl  11292  rpnnen1lem5  11302  fzo1fzo0n0  11965  quoremz  12089  quoremnn0ALT  12091  intfracq  12093  fldiv  12094  fldiv2  12095  modmulnn  12121  modidmul0OLD  12130  expnnval  12282  expneg  12287  digit2  12412  facdiv  12479  facndiv  12480  bcm1k  12507  bcp1n  12508  bcval5  12510  hashnncl  12554  cshwidxmod  12908  relexpsucnnr  13089  divcnv  13911  harmonic  13917  expcnv  13922  ef0lem  14133  ruclem6  14287  sqrt2irr  14301  dvdsval3  14309  nndivdvds  14311  dvdseq  14352  divalg2  14386  divalgmod  14387  ndvdssub  14388  nndvdslegcd  14479  modgcd  14500  gcddiv  14517  gcdeq  14520  sqgcd  14526  eucalgf  14542  eucalginv  14543  lcmgcdlem  14571  lcmftp  14609  divgcdodd  14653  qredeq  14663  qredeu  14664  isprm6  14666  divnumden  14697  divdenle  14698  phimullem  14727  pythagtriplem10  14770  pythagtriplem8  14773  pythagtriplem9  14774  pythagtriplem19  14783  pccl  14799  pcdiv  14802  pcqcl  14806  pcdvds  14813  pcndvds  14815  pcndvds2  14817  pceq0  14820  pcneg  14823  pcz  14830  pcmpt  14837  fldivp1  14842  pcfac  14844  infpnlem2  14855  cshwshashlem1  15066  mulgnn  16764  mulgnegnn  16768  oddvdsnn0  17193  odmulgeq  17208  gexnnod  17240  cply1coe0  18893  cply1coe0bi  18894  qsssubdrg  19027  prmirredlem  19063  znf1o  19121  znhash  19128  znidomb  19131  znunithash  19134  znrrg  19135  m2cpm  19764  m2cpminvid2lem  19777  fvmptnn04ifc  19875  vitali  22570  mbfi1fseqlem3  22674  dvexp2  22907  plyeq0lem  23163  abelthlem9  23394  logtayllem  23603  logtayl  23604  logtaylsum  23605  logtayl2  23606  cxpexp  23612  cxproot  23634  root1id  23693  root1eq1  23694  cxpeq  23696  atantayl  23862  atantayl2  23863  leibpilem2  23866  leibpi  23867  birthdaylem2  23877  birthdaylem3  23878  dfef2  23895  emcllem2  23921  emcllem3  23922  zetacvg  23939  lgam1  23988  basellem4  24009  basellem5  24010  basellem8  24013  basellem9  24014  mumullem2  24106  dvdsflip  24110  fsumdvdscom  24113  chtublem  24138  dchrelbas4  24170  bclbnd  24207  lgsval4a  24245  lgsabs1  24261  lgssq  24262  lgssq2  24263  dchrmusumlema  24330  dchrmusum2  24331  dchrvmasumiflem1  24338  dchrvmaeq0  24341  dchrisum0flblem1  24345  dchrisum0flblem2  24346  dchrisum0re  24350  ostthlem1  24464  ostth1  24470  cyclnspth  25358  clwwisshclwwlem  25533  gxpval  25986  gxmodid  26006  ipasslem4  26474  ipasslem5  26475  divnumden2  28389  qqhval2  28795  qqhnm  28803  signstfveq0  29475  subfacp1lem6  29917  circum  30327  fz0n  30372  divcnvlin  30375  iprodgam  30386  faclim  30390  nndivsub  31123  poimirlem29  31934  poimirlem31  31936  poimirlem32  31937  heiborlem4  32111  heiborlem6  32113  pellexlem1  35644  congrep  35794  jm2.20nn  35823  hashgcdlem  36045  phisum  36047  proot1ex  36049  hashnzfzclim  36642  binomcxplemnotnn0  36676  nnne1ge2  37460  mccllem  37618  clim1fr1  37620  dvnxpaek  37758  dvnprodlem2  37763  wallispilem5  37872  wallispi2lem1  37874  stirlinglem1  37877  stirlinglem3  37879  stirlinglem4  37880  stirlinglem5  37881  stirlinglem7  37883  stirlinglem10  37886  stirlinglem12  37888  stirlinglem14  37890  stirlinglem15  37891  fouriersw  38036  iccpartiltu  38607  gcdzeq  38664  divgcdoddALTV  38682  nnsgrpnmnd  39467  eluz2cnn0n1  39958  mod0mul  39973  modn0mul  39974  blennn  40037  nnpw2blen  40042  digvalnn0  40061  nn0digval  40062  dignn0fr  40063  dignn0ldlem  40064  dig0  40068