Theorem nnne0 12162

Description: A positive integer is nonzero. See nnne0ALT 12166 for a shorter proof using ax-pre-mulgt0 11086. This proof avoids 0lt1 11642, and thus ax-pre-mulgt0 11086, by splitting ax-1ne0 11078 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11086. (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 11078	. . 3 ⊢ 1 ≠ 0
2		1re 11115	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11117	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11230	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 230	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5095	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5095	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5095	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5095	. . . . . . 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 12143	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11116	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11144	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11130	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11118	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11731	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11067	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11304	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5127	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11277	. . . . . . . 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 12146	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11685	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5096	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5096	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5096	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5096	. . . . . . 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 12143	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11116	. . . . . . . . 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 11695	. . . . . . . 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 12146	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11684	. . 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 1540   ∈ wcel 2109   ≠ wne 2925   class class class wbr 5092  (class class class)co 7349  ℝcr 11008  0cc0 11009  1c1 11010   + caddc 11012   < clt 11149  ℕcn 12128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-nn 12129

This theorem is referenced by:  nnneneg  12163  0nnn  12164  nndivre  12169  nndiv  12174  nndivtr  12175  nnne0d  12178  zdiv  12546  zdivadd  12547  zdivmul  12548  elq  12851  qmulz  12852  qre  12854  qaddcl  12866  qnegcl  12867  qmulcl  12868  qreccl  12870  rpnnen1lem5  12882  nn0ledivnn  13008  fzo1fzo0n0  13618  quoremz  13759  quoremnn0ALT  13761  intfracq  13763  fldiv  13764  fldiv2  13765  modmulnn  13793  modsumfzodifsn  13851  expnnval  13971  expneg  13976  digit2  14143  facdiv  14194  facndiv  14195  bcm1k  14222  bcp1n  14223  bcval5  14225  hashnncl  14273  cshwidxmod  14709  relexpsucnnr  14932  divcnv  15760  harmonic  15766  expcnv  15771  ef0lem  15985  ruclem6  16144  sqrt2irr  16158  dvdsval3  16167  nndivdvds  16172  modmulconst  16199  dvdsdivcl  16227  dvdsflip  16228  divalg2  16316  divalgmod  16317  ndvdssub  16320  nndvdslegcd  16416  divgcdz  16422  divgcdnn  16426  modgcd  16443  gcddiv  16462  gcdzeq  16463  eucalgf  16494  eucalginv  16495  lcmgcdlem  16517  lcmftp  16547  qredeq  16568  qredeu  16569  cncongr1  16578  cncongr2  16579  isprm6  16625  divnumden  16659  divdenle  16660  phimullem  16690  hashgcdlem  16699  phisum  16702  prm23lt5  16726  pythagtriplem10  16732  pythagtriplem8  16735  pythagtriplem9  16736  pccl  16761  pcdiv  16764  pcqcl  16768  pcdvds  16776  pcndvds  16778  pcndvds2  16780  pceq0  16783  pcneg  16786  pcz  16793  pcmpt  16804  fldivp1  16809  pcfac  16811  oddprmdvds  16815  infpnlem2  16823  cshwshashlem1  17007  smndex1n0mnd  18786  mulgnn  18954  mulgnegnn  18963  mulgmodid  18992  oddvdsnn0  19423  odmulgeq  19436  gexnnod  19467  qsssubdrg  21333  prmirredlem  21379  znf1o  21458  znhash  21465  znidomb  21468  znunithash  21471  znrrg  21472  cply1coe0  22186  cply1coe0bi  22187  m2cpm  22626  m2cpminvid2lem  22639  fvmptnn04ifc  22737  vitali  25512  mbfi1fseqlem3  25616  dvexp2  25856  plyeq0lem  26113  abelthlem9  26348  logtayllem  26566  logtayl  26567  logtaylsum  26568  logtayl2  26569  cxpexp  26575  cxproot  26597  root1id  26662  root1eq1  26663  cxpeq  26665  logbgcd1irr  26702  atantayl  26845  atantayl2  26846  leibpilem2  26849  leibpi  26850  birthdaylem2  26860  birthdaylem3  26861  dfef2  26879  emcllem2  26905  emcllem3  26906  zetacvg  26923  lgam1  26972  basellem4  26992  basellem8  26996  basellem9  26997  mumullem2  27088  fsumdvdscom  27093  chtublem  27120  dchrelbas4  27152  bclbnd  27189  lgsval4a  27228  lgsabs1  27245  lgssq2  27247  dchrmusumlema  27402  dchrmusum2  27403  dchrvmasumiflem1  27410  dchrvmaeq0  27413  dchrisum0flblem1  27417  dchrisum0flblem2  27418  dchrisum0re  27422  ostthlem1  27536  ostth1  27542  pthdlem2lem  29712  wspthsnonn0vne  29862  clwwisshclwwslem  29958  ipasslem4  30778  ipasslem5  30779  divnumden2  32760  1fldgenq  33261  qqhval2  33949  qqhnm  33957  signstfveq0  34545  subfacp1lem6  35158  circum  35647  fz0n  35704  divcnvlin  35706  iprodgam  35715  faclim  35719  nndivsub  36431  poimirlem29  37629  poimirlem31  37631  poimirlem32  37632  heiborlem4  37794  heiborlem6  37796  nnproddivdvdsd  41973  pellexlem1  42802  congrep  42946  jm2.20nn  42970  proot1ex  43169  hashnzfzclim  44295  binomcxplemnotnn0  44329  nnne1ge2  45273  mccllem  45578  clim1fr1  45582  dvnxpaek  45923  dvnprodlem2  45928  wallispilem5  46050  wallispi2lem1  46052  stirlinglem1  46055  stirlinglem3  46057  stirlinglem4  46058  stirlinglem5  46059  stirlinglem7  46061  stirlinglem10  46064  stirlinglem12  46066  stirlinglem14  46068  stirlinglem15  46069  fouriersw  46212  vonioolem2  46662  vonicclem2  46665  mod0mul  47340  modn0mul  47341  modlt0b  47347  iccpartiltu  47406  divgcdoddALTV  47666  fpprwppr  47723  isubgr3stgrlem7  47956  gpg3kgrtriexlem5  48071  nnsgrpnmnd  48162  eluz2cnn0n1  48496  blennn  48560  nnpw2blen  48565  digvalnn0  48584  nn0digval  48585  dignn0fr  48586  dignn0ldlem  48587  dig0  48591