Theorem nnne0 10675

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 10674	. . 3 |- -. 0 e. NN
2		eleq1 2528	. . 3 |- ( A = 0 -> ( A e. NN <-> 0 e. NN ) )
3	1, 2	mtbiri 309	. 2 |- ( A = 0 -> -. A e. NN )
4	3	necon2ai 2665	1 |- ( A e. NN -> A =/= 0 )

Syntax hints:   -> wi 4   = wceq 1455   e. wcel 1898   =/= wne 2633   0cc0 9570   NNcn 10642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643

This theorem is referenced by:  nndivre  10678  nndiv  10683  nndivtr  10684  nnne0d  10687  zdiv  11040  zdivadd  11041  zdivmul  11042  elq  11300  qmulz  11301  qre  11303  qaddcl  11314  qnegcl  11315  qmulcl  11316  qreccl  11318  rpnnen1lem5  11328  fzo1fzo0n0  11994  quoremz  12120  quoremnn0ALT  12122  intfracq  12124  fldiv  12125  fldiv2  12126  modmulnn  12152  modidmul0OLD  12161  expnnval  12313  expneg  12318  digit2  12443  facdiv  12510  facndiv  12511  bcm1k  12538  bcp1n  12539  bcval5  12541  hashnncl  12585  cshwidxmod  12948  relexpsucnnr  13143  divcnv  13966  harmonic  13972  expcnv  13977  ef0lem  14188  ruclem6  14342  sqrt2irr  14356  dvdsval3  14364  nndivdvds  14366  dvdseq  14407  divalg2  14441  divalgmod  14442  ndvdssub  14443  nndvdslegcd  14534  modgcd  14555  gcddiv  14572  gcdeq  14575  sqgcd  14581  eucalgf  14597  eucalginv  14598  lcmgcdlem  14626  lcmftp  14664  divgcdodd  14708  qredeq  14718  qredeu  14719  isprm6  14721  divnumden  14752  divdenle  14753  phimullem  14782  pythagtriplem10  14825  pythagtriplem8  14828  pythagtriplem9  14829  pythagtriplem19  14838  pccl  14854  pcdiv  14857  pcqcl  14861  pcdvds  14868  pcndvds  14870  pcndvds2  14872  pceq0  14875  pcneg  14878  pcz  14885  pcmpt  14892  fldivp1  14897  pcfac  14899  infpnlem2  14910  cshwshashlem1  15121  mulgnn  16819  mulgnegnn  16823  oddvdsnn0  17248  odmulgeq  17263  gexnnod  17295  cply1coe0  18948  cply1coe0bi  18949  qsssubdrg  19082  prmirredlem  19119  znf1o  19177  znhash  19184  znidomb  19187  znunithash  19190  znrrg  19191  m2cpm  19820  m2cpminvid2lem  19833  fvmptnn04ifc  19931  vitali  22627  mbfi1fseqlem3  22731  dvexp2  22964  plyeq0lem  23220  abelthlem9  23451  logtayllem  23660  logtayl  23661  logtaylsum  23662  logtayl2  23663  cxpexp  23669  cxproot  23691  root1id  23750  root1eq1  23751  cxpeq  23753  atantayl  23919  atantayl2  23920  leibpilem2  23923  leibpi  23924  birthdaylem2  23934  birthdaylem3  23935  dfef2  23952  emcllem2  23978  emcllem3  23979  zetacvg  23996  lgam1  24045  basellem4  24066  basellem5  24067  basellem8  24070  basellem9  24071  mumullem2  24163  dvdsflip  24167  fsumdvdscom  24170  chtublem  24195  dchrelbas4  24227  bclbnd  24264  lgsval4a  24302  lgsabs1  24318  lgssq  24319  lgssq2  24320  dchrmusumlema  24387  dchrmusum2  24388  dchrvmasumiflem1  24395  dchrvmaeq0  24398  dchrisum0flblem1  24402  dchrisum0flblem2  24403  dchrisum0re  24407  ostthlem1  24521  ostth1  24527  cyclnspth  25415  clwwisshclwwlem  25590  gxpval  26043  gxmodid  26063  ipasslem4  26531  ipasslem5  26532  divnumden2  28433  qqhval2  28837  qqhnm  28845  signstfveq0  29516  subfacp1lem6  29958  circum  30368  fz0n  30414  divcnvlin  30417  iprodgam  30428  faclim  30432  nndivsub  31167  poimirlem29  32015  poimirlem31  32017  poimirlem32  32018  heiborlem4  32192  heiborlem6  32194  pellexlem1  35719  congrep  35869  jm2.20nn  35898  hashgcdlem  36120  phisum  36122  proot1ex  36124  hashnzfzclim  36716  binomcxplemnotnn0  36750  nnne1ge2  37580  mccllem  37763  clim1fr1  37765  dvnxpaek  37903  dvnprodlem2  37908  wallispilem5  38032  wallispi2lem1  38034  stirlinglem1  38037  stirlinglem3  38039  stirlinglem4  38040  stirlinglem5  38041  stirlinglem7  38043  stirlinglem10  38046  stirlinglem12  38048  stirlinglem14  38050  stirlinglem15  38051  fouriersw  38196  iccpartiltu  38871  gcdzeq  38928  divgcdoddALTV  38946  pthdlem2lem  39889  nnsgrpnmnd  40187  eluz2cnn0n1  40676  mod0mul  40691  modn0mul  40692  blennn  40755  nnpw2blen  40760  digvalnn0  40779  nn0digval  40780  dignn0fr  40781  dignn0ldlem  40782  dig0  40786