Theorem nnne0 9099

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 9098	. . 3 |- -. 0 e. NN
2		eleq1 2270	. . 3 |- ( A = 0 -> ( A e. NN <-> 0 e. NN ) )
3	1, 2	mtbiri 677	. 2 |- ( A = 0 -> -. A e. NN )
4	3	necon2ai 2432	1 |- ( A e. NN -> A =/= 0 )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2178   =/= wne 2378   0cc0 7960   NNcn 9071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-un 4498  ax-setind 4603  ax-cnex 8051  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057  ax-0lt1 8066  ax-0id 8068  ax-rnegex 8069  ax-pre-ltirr 8072  ax-pre-lttrn 8074  ax-pre-ltadd 8076

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-nel 2474  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-br 4060  df-opab 4122  df-xp 4699  df-cnv 4701  df-iota 5251  df-fv 5298  df-ov 5970  df-pnf 8144  df-mnf 8145  df-xr 8146  df-ltxr 8147  df-le 8148  df-inn 9072

This theorem is referenced by:  nnne0d  9116  divfnzn  9777  qreccl  9798  fzo1fzo0n0  10344  expnnval  10724  expnegap0  10729  hashnncl  10977  ef0lem  12086  dvdsval3  12217  nndivdvds  12222  modmulconst  12249  dvdsdivcl  12276  divalg2  12352  ndvdssub  12356  nndvdslegcd  12401  divgcdz  12407  divgcdnn  12411  gcdzeq  12458  eucalgf  12492  eucalginv  12493  lcmgcdlem  12514  qredeu  12534  cncongr1  12540  cncongr2  12541  divnumden  12633  divdenle  12634  phimullem  12662  hashgcdlem  12675  phisum  12678  prm23lt5  12701  pythagtriplem8  12710  pythagtriplem9  12711  pceu  12733  pccl  12737  pcdiv  12740  pcqcl  12744  pcdvds  12753  pcndvds  12755  pcndvds2  12757  pceq0  12760  pcz  12770  pcmpt  12781  fldivp1  12786  pcfac  12788  ennnfonelemjn  12888  mulgnn  13577  mulgnegnn  13583  znf1o  14528  znfi  14532  znhash  14533  znidomb  14535  znrrg  14537  dvexp2  15299  lgsval4a  15614  lgsabs1  15631  lgssq2  15633