Theorem nnne0 12227

Description: A positive integer is nonzero. See nnne0ALT 12231 for a shorter proof using ax-pre-mulgt0 11152. This proof avoids 0lt1 11707, and thus ax-pre-mulgt0 11152, by splitting ax-1ne0 11144 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11152. (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 11144	. . 3 ⊢ 1 ≠ 0
2		1re 11181	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11183	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11295	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 230	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5113	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5113	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5113	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5113	. . . . . . 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 12208	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11182	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11210	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11196	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11184	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11796	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11133	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11369	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5145	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11342	. . . . . . . 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 12211	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11750	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5114	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5114	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5114	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5114	. . . . . . 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 12208	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11182	. . . . . . . . 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 11760	. . . . . . . 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 12211	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11749	. . 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 2926   class class class wbr 5110  (class class class)co 7390  ℝcr 11074  0cc0 11075  1c1 11076   + caddc 11078   < clt 11215  ℕcn 12193

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-nn 12194

This theorem is referenced by:  nnneneg  12228  0nnn  12229  nndivre  12234  nndiv  12239  nndivtr  12240  nnne0d  12243  zdiv  12611  zdivadd  12612  zdivmul  12613  elq  12916  qmulz  12917  qre  12919  qaddcl  12931  qnegcl  12932  qmulcl  12933  qreccl  12935  rpnnen1lem5  12947  nn0ledivnn  13073  fzo1fzo0n0  13683  quoremz  13824  quoremnn0ALT  13826  intfracq  13828  fldiv  13829  fldiv2  13830  modmulnn  13858  modsumfzodifsn  13916  expnnval  14036  expneg  14041  digit2  14208  facdiv  14259  facndiv  14260  bcm1k  14287  bcp1n  14288  bcval5  14290  hashnncl  14338  cshwidxmod  14775  relexpsucnnr  14998  divcnv  15826  harmonic  15832  expcnv  15837  ef0lem  16051  ruclem6  16210  sqrt2irr  16224  dvdsval3  16233  nndivdvds  16238  modmulconst  16265  dvdsdivcl  16293  dvdsflip  16294  divalg2  16382  divalgmod  16383  ndvdssub  16386  nndvdslegcd  16482  divgcdz  16488  divgcdnn  16492  modgcd  16509  gcddiv  16528  gcdzeq  16529  eucalgf  16560  eucalginv  16561  lcmgcdlem  16583  lcmftp  16613  qredeq  16634  qredeu  16635  cncongr1  16644  cncongr2  16645  isprm6  16691  divnumden  16725  divdenle  16726  phimullem  16756  hashgcdlem  16765  phisum  16768  prm23lt5  16792  pythagtriplem10  16798  pythagtriplem8  16801  pythagtriplem9  16802  pccl  16827  pcdiv  16830  pcqcl  16834  pcdvds  16842  pcndvds  16844  pcndvds2  16846  pceq0  16849  pcneg  16852  pcz  16859  pcmpt  16870  fldivp1  16875  pcfac  16877  oddprmdvds  16881  infpnlem2  16889  cshwshashlem1  17073  smndex1n0mnd  18846  mulgnn  19014  mulgnegnn  19023  mulgmodid  19052  oddvdsnn0  19481  odmulgeq  19494  gexnnod  19525  qsssubdrg  21350  prmirredlem  21389  znf1o  21468  znhash  21475  znidomb  21478  znunithash  21481  znrrg  21482  cply1coe0  22195  cply1coe0bi  22196  m2cpm  22635  m2cpminvid2lem  22648  fvmptnn04ifc  22746  vitali  25521  mbfi1fseqlem3  25625  dvexp2  25865  plyeq0lem  26122  abelthlem9  26357  logtayllem  26575  logtayl  26576  logtaylsum  26577  logtayl2  26578  cxpexp  26584  cxproot  26606  root1id  26671  root1eq1  26672  cxpeq  26674  logbgcd1irr  26711  atantayl  26854  atantayl2  26855  leibpilem2  26858  leibpi  26859  birthdaylem2  26869  birthdaylem3  26870  dfef2  26888  emcllem2  26914  emcllem3  26915  zetacvg  26932  lgam1  26981  basellem4  27001  basellem8  27005  basellem9  27006  mumullem2  27097  fsumdvdscom  27102  chtublem  27129  dchrelbas4  27161  bclbnd  27198  lgsval4a  27237  lgsabs1  27254  lgssq2  27256  dchrmusumlema  27411  dchrmusum2  27412  dchrvmasumiflem1  27419  dchrvmaeq0  27422  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0re  27431  ostthlem1  27545  ostth1  27551  pthdlem2lem  29704  wspthsnonn0vne  29854  clwwisshclwwslem  29950  ipasslem4  30770  ipasslem5  30771  divnumden2  32747  1fldgenq  33279  qqhval2  33979  qqhnm  33987  signstfveq0  34575  subfacp1lem6  35179  circum  35668  fz0n  35725  divcnvlin  35727  iprodgam  35736  faclim  35740  nndivsub  36452  poimirlem29  37650  poimirlem31  37652  poimirlem32  37653  heiborlem4  37815  heiborlem6  37817  nnproddivdvdsd  41995  pellexlem1  42824  congrep  42969  jm2.20nn  42993  proot1ex  43192  hashnzfzclim  44318  binomcxplemnotnn0  44352  nnne1ge2  45296  mccllem  45602  clim1fr1  45606  dvnxpaek  45947  dvnprodlem2  45952  wallispilem5  46074  wallispi2lem1  46076  stirlinglem1  46079  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem7  46085  stirlinglem10  46088  stirlinglem12  46090  stirlinglem14  46092  stirlinglem15  46093  fouriersw  46236  vonioolem2  46686  vonicclem2  46689  mod0mul  47361  modn0mul  47362  modlt0b  47368  iccpartiltu  47427  divgcdoddALTV  47687  fpprwppr  47744  isubgr3stgrlem7  47975  gpg3kgrtriexlem5  48082  nnsgrpnmnd  48170  eluz2cnn0n1  48504  blennn  48568  nnpw2blen  48573  digvalnn0  48592  nn0digval  48593  dignn0fr  48594  dignn0ldlem  48595  dig0  48599