Theorem nnne0 11053

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

Assertion

Ref	Expression
nnne0	⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Proof of Theorem nnne0

Step	Hyp	Ref	Expression
1		0nnn 11052	. . 3 ⊢ ¬ 0 ∈ ℕ
2		eleq1 2689	. . 3 ⊢ (𝐴 = 0 → (𝐴 ∈ ℕ ↔ 0 ∈ ℕ))
3	1, 2	mtbiri 317	. 2 ⊢ (𝐴 = 0 → ¬ 𝐴 ∈ ℕ)
4	3	necon2ai 2823	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  0cc0 9936  ℕcn 11020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021

This theorem is referenced by:  nndivre  11056  nndiv  11061  nndivtr  11062  nnne0d  11065  zdiv  11447  zdivadd  11448  zdivmul  11449  elq  11790  qmulz  11791  qre  11793  qaddcl  11804  qnegcl  11805  qmulcl  11806  qreccl  11808  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  nn0ledivnn  11941  fzo1fzo0n0  12518  quoremz  12654  quoremnn0ALT  12656  intfracq  12658  fldiv  12659  fldiv2  12660  modmulnn  12688  modsumfzodifsn  12743  expnnval  12863  expneg  12868  digit2  12997  facdiv  13074  facndiv  13075  bcm1k  13102  bcp1n  13103  bcval5  13105  hashnncl  13157  cshwidxmod  13549  relexpsucnnr  13765  divcnv  14585  harmonic  14591  expcnv  14596  ef0lem  14809  ruclem6  14964  sqrt2irr  14979  dvdsval3  14987  nndivdvds  14989  modmulconst  15013  dvdsdivcl  15038  dvdsflip  15039  divalg2  15128  divalgmod  15129  divalgmodOLD  15130  ndvdssub  15133  nndvdslegcd  15227  divgcdz  15233  divgcdnn  15236  modgcd  15253  gcddiv  15268  gcdzeq  15271  eucalgf  15296  eucalginv  15297  lcmgcdlem  15319  lcmftp  15349  qredeq  15371  qredeu  15372  cncongr1  15381  cncongr2  15382  isprm6  15426  divnumden  15456  divdenle  15457  phimullem  15484  hashgcdlem  15493  phisum  15495  prm23lt5  15519  pythagtriplem10  15525  pythagtriplem8  15528  pythagtriplem9  15529  pythagtriplem19  15538  pccl  15554  pcdiv  15557  pcqcl  15561  pcdvds  15568  pcndvds  15570  pcndvds2  15572  pceq0  15575  pcneg  15578  pcz  15585  pcmpt  15596  fldivp1  15601  pcfac  15603  oddprmdvds  15607  infpnlem2  15615  cshwshashlem1  15802  mulgnn  17547  mulgnegnn  17551  mulgmodid  17581  oddvdsnn0  17963  odmulgeq  17974  gexnnod  18003  cply1coe0  19669  cply1coe0bi  19670  qsssubdrg  19805  prmirredlem  19841  znf1o  19900  znhash  19907  znidomb  19910  znunithash  19913  znrrg  19914  m2cpm  20546  m2cpminvid2lem  20559  fvmptnn04ifc  20657  vitali  23382  mbfi1fseqlem3  23484  dvexp2  23717  plyeq0lem  23966  abelthlem9  24194  logtayllem  24405  logtayl  24406  logtaylsum  24407  logtayl2  24408  cxpexp  24414  cxproot  24436  root1id  24495  root1eq1  24496  cxpeq  24498  atantayl  24664  atantayl2  24665  leibpilem2  24668  leibpi  24669  birthdaylem2  24679  birthdaylem3  24680  dfef2  24697  emcllem2  24723  emcllem3  24724  zetacvg  24741  lgam1  24790  basellem4  24810  basellem5  24811  basellem8  24814  basellem9  24815  mumullem2  24906  fsumdvdscom  24911  chtublem  24936  dchrelbas4  24968  bclbnd  25005  lgsval4a  25044  lgsabs1  25061  lgssq2  25063  dchrmusumlema  25182  dchrmusum2  25183  dchrvmasumiflem1  25190  dchrvmaeq0  25193  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0re  25202  ostthlem1  25316  ostth1  25322  pthdlem2lem  26663  wspthsnonn0vne  26813  clwwisshclwwslem  26927  numclwwlkffin0  27215  ipasslem4  27689  ipasslem5  27690  divnumden2  29564  qqhval2  30026  qqhnm  30034  signstfveq0  30654  subfacp1lem6  31167  circum  31568  fz0n  31616  divcnvlin  31618  iprodgam  31628  faclim  31632  nndivsub  32456  poimirlem29  33438  poimirlem31  33440  poimirlem32  33441  heiborlem4  33613  heiborlem6  33615  pellexlem1  37393  congrep  37540  jm2.20nn  37564  proot1ex  37779  hashnzfzclim  38521  binomcxplemnotnn0  38555  nnne1ge2  39504  mccllem  39829  clim1fr1  39833  dvnxpaek  40157  dvnprodlem2  40162  wallispilem5  40286  wallispi2lem1  40288  stirlinglem1  40291  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem7  40297  stirlinglem10  40300  stirlinglem12  40302  stirlinglem14  40304  stirlinglem15  40305  fouriersw  40448  vonioolem2  40895  vonicclem2  40898  iccpartiltu  41358  divgcdoddALTV  41593  nnsgrpnmnd  41818  eluz2cnn0n1  42301  mod0mul  42314  modn0mul  42315  blennn  42369  nnpw2blen  42374  digvalnn0  42393  nn0digval  42394  dignn0fr  42395  dignn0ldlem  42396  dig0  42400