Theorem nnne0 10503

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 10502	. . 3 |- -. 0 e. NN
2		eleq1 2464	. . 3 |- ( A = 0 -> ( A e. NN <-> 0 e. NN ) )
3	1, 2	mtbiri 301	. 2 |- ( A = 0 -> -. A e. NN )
4	3	necon2ai 2627	1 |- ( A e. NN -> A =/= 0 )

Syntax hints:   -> wi 4   = wceq 1399   e. wcel 1836   =/= wne 2587   0cc0 9421   NNcn 10470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-iun 4258  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-om 6618  df-recs 6978  df-rdg 7012  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-nn 10471

This theorem is referenced by:  nndivre  10506  nndiv  10511  nndivtr  10512  nnne0d  10515  zdiv  10868  zdivadd  10869  zdivmul  10870  elq  11121  qmulz  11122  qre  11124  qaddcl  11135  qnegcl  11136  qmulcl  11137  qreccl  11139  rpnnen1lem5  11149  fzo1fzo0n0  11777  quoremz  11901  quoremnn0ALT  11903  intfracq  11905  fldiv  11906  fldiv2  11907  modmulnn  11933  modidmul0OLD  11942  expnnval  12091  expneg  12096  digit2  12220  facdiv  12286  facndiv  12287  bcm1k  12314  bcp1n  12315  bcval5  12317  hashnncl  12358  cshwidxmod  12704  relexpsucnnr  12881  divcnv  13686  harmonic  13691  expcnv  13696  ef0lem  13835  ruclem6  13989  sqrt2irr  14003  dvdsval3  14011  nndivdvds  14013  dvdseq  14054  divalg2  14084  divalgmod  14085  ndvdssub  14086  modgcd  14195  gcddiv  14208  gcdeq  14211  sqgcd  14217  eucalgf  14233  eucalginv  14234  qredeq  14268  qredeu  14269  isprm6  14271  divgcdodd  14281  divnumden  14302  divdenle  14303  phimullem  14330  pythagtriplem10  14365  pythagtriplem8  14368  pythagtriplem9  14369  pythagtriplem19  14378  pccl  14394  pcdiv  14397  pcqcl  14401  pcdvds  14408  pcndvds  14410  pcndvds2  14412  pceq0  14415  pcneg  14418  pcz  14425  pcmpt  14432  fldivp1  14437  pcfac  14439  infpnlem2  14450  cshwshashlem1  14601  mulgnn  16284  mulgnegnn  16288  oddvdsnn0  16704  odmulgeq  16715  gexnnod  16744  cply1coe0  18473  cply1coe0bi  18474  qsssubdrg  18609  prmirredlem  18642  znf1o  18700  znhash  18707  znidomb  18710  znunithash  18713  znrrg  18714  m2cpm  19346  m2cpminvid2lem  19359  fvmptnn04ifc  19457  vitali  22126  mbfi1fseqlem3  22228  dvexp2  22461  plyeq0lem  22711  abelthlem9  22939  logtayllem  23146  logtayl  23147  logtaylsum  23148  logtayl2  23149  cxpexp  23155  cxproot  23177  root1id  23234  root1eq1  23235  cxpeq  23237  atantayl  23403  atantayl2  23404  leibpilem2  23407  leibpi  23408  birthdaylem2  23418  birthdaylem3  23419  dfef2  23436  emcllem2  23462  emcllem3  23463  basellem4  23493  basellem5  23494  basellem8  23497  basellem9  23498  mumullem2  23590  dvdsflip  23594  fsumdvdscom  23597  chtublem  23622  dchrelbas4  23654  bclbnd  23691  lgsval4a  23729  lgsabs1  23745  lgssq  23746  lgssq2  23747  dchrmusumlema  23814  dchrmusum2  23815  dchrvmasumiflem1  23822  dchrvmaeq0  23825  dchrisum0flblem1  23829  dchrisum0flblem2  23830  dchrisum0re  23834  ostthlem1  23948  ostth1  23954  cyclnspth  24773  clwwisshclwwlem  24948  gxpval  25399  gxmodid  25419  ipasslem4  25887  ipasslem5  25888  divnumden2  27792  qqhval2  28147  qqhnm  28155  signstfveq0  28753  zetacvg  28782  lgam1  28831  subfacp1lem6  28854  circum  29265  fz0n  29312  divcnvlin  29320  iprodgam  29327  faclim  29373  nndivsub  30111  heiborlem4  30512  heiborlem6  30514  pellexlem1  30966  congrep  31112  jm2.20nn  31141  hashgcdlem  31361  phisum  31363  proot1ex  31365  lcmgcdlem  31416  hashnzfzclim  31431  binomcxplemnotnn0  31465  nnne1ge2  31683  mccllem  31806  clim1fr1  31808  dvnxpaek  31940  dvnprodlem2  31945  wallispilem5  32052  wallispi2lem1  32054  stirlinglem1  32057  stirlinglem3  32059  stirlinglem4  32060  stirlinglem5  32061  stirlinglem7  32063  stirlinglem10  32066  stirlinglem12  32068  stirlinglem14  32070  stirlinglem15  32071  fouriersw  32215  gcdzeq  32541  divgcdoddALTV  32559  nnsgrpnmnd  32859  eluz2cnn0n1  33350  mod0mul  33367  modn0mul  33368  blennn  33431  nnpw2blen  33436  digvalnn0  33455  nn0digval  33456  dignn0fr  33457  dignn0ldlem  33458  dig0  33462