Theorem nnne0 12170

Description: A positive integer is nonzero. See nnne0ALT 12174 for a shorter proof using ax-pre-mulgt0 11094. This proof avoids 0lt1 11650, and thus ax-pre-mulgt0 11094, by splitting ax-1ne0 11086 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11094. (Revised by Steven Nguyen, 30-Jan-2023.)

Assertion

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

Proof of Theorem nnne0

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1ne0 11086	. . 3 ⊢ 1 ≠ 0
2		1re 11123	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11125	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11238	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 230	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5098	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5098	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5098	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5098	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 22	. . . . . 6 ⊢ (1 < 0 → 1 < 0)
15		simp1 1136	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 12151	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11124	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11152	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11138	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11126	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11739	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11075	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11312	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5130	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11285	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1119	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (1 < 0 → (𝑦 < 0 → (𝑦 + 1) < 0)))
30	29	a2d 29	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((1 < 0 → 𝑦 < 0) → (1 < 0 → (𝑦 + 1) < 0)))
31	7, 9, 11, 13, 14, 30	nnind 12154	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11693	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5099	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5099	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5099	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5099	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
41	40	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
42		id 22	. . . . . 6 ⊢ (0 < 1 → 0 < 1)
43		simp1 1136	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
44	43	nnred 12151	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11124	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
46		simp3 1138	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
47		simp2 1137	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
48	44, 45, 46, 47	addgt0d 11703	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
49	48	3exp 1119	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (0 < 1 → (0 < 𝑦 → 0 < (𝑦 + 1))))
50	49	a2d 29	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((0 < 1 → 0 < 𝑦) → (0 < 1 → 0 < (𝑦 + 1))))
51	35, 37, 39, 41, 42, 50	nnind 12154	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11692	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 959	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 691	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ≠ wne 2929   class class class wbr 5095  (class class class)co 7355  ℝcr 11016  0cc0 11017  1c1 11018   + caddc 11020   < clt 11157  ℕcn 12136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-nn 12137

This theorem is referenced by:  nnneneg  12171  0nnn  12172  nndivre  12177  nndiv  12182  nndivtr  12183  nnne0d  12186  zdiv  12553  zdivadd  12554  zdivmul  12555  elq  12854  qmulz  12855  qre  12857  qaddcl  12869  qnegcl  12870  qmulcl  12871  qreccl  12873  rpnnen1lem5  12885  nn0ledivnn  13011  fzo1fzo0n0  13622  quoremz  13766  quoremnn0ALT  13768  intfracq  13770  fldiv  13771  fldiv2  13772  modmulnn  13800  modsumfzodifsn  13858  expnnval  13978  expneg  13983  digit2  14150  facdiv  14201  facndiv  14202  bcm1k  14229  bcp1n  14230  bcval5  14232  hashnncl  14280  cshwidxmod  14717  relexpsucnnr  14939  divcnv  15767  harmonic  15773  expcnv  15778  ef0lem  15992  ruclem6  16151  sqrt2irr  16165  dvdsval3  16174  nndivdvds  16179  modmulconst  16206  dvdsdivcl  16234  dvdsflip  16235  divalg2  16323  divalgmod  16324  ndvdssub  16327  nndvdslegcd  16423  divgcdz  16429  divgcdnn  16433  modgcd  16450  gcddiv  16469  gcdzeq  16470  eucalgf  16501  eucalginv  16502  lcmgcdlem  16524  lcmftp  16554  qredeq  16575  qredeu  16576  cncongr1  16585  cncongr2  16586  isprm6  16632  divnumden  16666  divdenle  16667  phimullem  16697  hashgcdlem  16706  phisum  16709  prm23lt5  16733  pythagtriplem10  16739  pythagtriplem8  16742  pythagtriplem9  16743  pccl  16768  pcdiv  16771  pcqcl  16775  pcdvds  16783  pcndvds  16785  pcndvds2  16787  pceq0  16790  pcneg  16793  pcz  16800  pcmpt  16811  fldivp1  16816  pcfac  16818  oddprmdvds  16822  infpnlem2  16830  cshwshashlem1  17014  smndex1n0mnd  18828  mulgnn  18996  mulgnegnn  19005  mulgmodid  19034  oddvdsnn0  19464  odmulgeq  19477  gexnnod  19508  qsssubdrg  21372  prmirredlem  21418  znf1o  21497  znhash  21504  znidomb  21507  znunithash  21510  znrrg  21511  cply1coe0  22236  cply1coe0bi  22237  m2cpm  22676  m2cpminvid2lem  22689  fvmptnn04ifc  22787  vitali  25561  mbfi1fseqlem3  25665  dvexp2  25905  plyeq0lem  26162  abelthlem9  26397  logtayllem  26615  logtayl  26616  logtaylsum  26617  logtayl2  26618  cxpexp  26624  cxproot  26646  root1id  26711  root1eq1  26712  cxpeq  26714  logbgcd1irr  26751  atantayl  26894  atantayl2  26895  leibpilem2  26898  leibpi  26899  birthdaylem2  26909  birthdaylem3  26910  dfef2  26928  emcllem2  26954  emcllem3  26955  zetacvg  26972  lgam1  27021  basellem4  27041  basellem8  27045  basellem9  27046  mumullem2  27137  fsumdvdscom  27142  chtublem  27169  dchrelbas4  27201  bclbnd  27238  lgsval4a  27277  lgsabs1  27294  lgssq2  27296  dchrmusumlema  27451  dchrmusum2  27452  dchrvmasumiflem1  27459  dchrvmaeq0  27462  dchrisum0flblem1  27466  dchrisum0flblem2  27467  dchrisum0re  27471  ostthlem1  27585  ostth1  27591  pthdlem2lem  29766  wspthsnonn0vne  29916  clwwisshclwwslem  30015  ipasslem4  30835  ipasslem5  30836  divnumden2  32824  1fldgenq  33332  qqhval2  34067  qqhnm  34075  signstfveq0  34662  subfacp1lem6  35301  circum  35790  fz0n  35847  divcnvlin  35849  iprodgam  35858  faclim  35862  nndivsub  36573  poimirlem29  37762  poimirlem31  37764  poimirlem32  37765  heiborlem4  37927  heiborlem6  37929  nnproddivdvdsd  42166  pellexlem1  42986  congrep  43130  jm2.20nn  43154  proot1ex  43353  hashnzfzclim  44479  binomcxplemnotnn0  44513  nnne1ge2  45455  mccllem  45759  clim1fr1  45763  dvnxpaek  46102  dvnprodlem2  46107  wallispilem5  46229  wallispi2lem1  46231  stirlinglem1  46234  stirlinglem3  46236  stirlinglem4  46237  stirlinglem5  46238  stirlinglem7  46240  stirlinglem10  46243  stirlinglem12  46245  stirlinglem14  46247  stirlinglem15  46248  fouriersw  46391  vonioolem2  46841  vonicclem2  46844  mod0mul  47518  modn0mul  47519  modlt0b  47525  iccpartiltu  47584  divgcdoddALTV  47844  fpprwppr  47901  isubgr3stgrlem7  48134  gpg3kgrtriexlem5  48249  nnsgrpnmnd  48340  eluz2cnn0n1  48673  blennn  48737  nnpw2blen  48742  digvalnn0  48761  nn0digval  48762  dignn0fr  48763  dignn0ldlem  48764  dig0  48768