Theorem nnne0 12300

Description: A positive integer is nonzero. See nnne0ALT 12304 for a shorter proof using ax-pre-mulgt0 11232. This proof avoids 0lt1 11785, and thus ax-pre-mulgt0 11232, by splitting ax-1ne0 11224 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11232. (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 11224	. . 3 ⊢ 1 ≠ 0
2		1re 11261	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11263	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11375	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 230	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5146	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5146	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5146	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5146	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 22	. . . . . 6 ⊢ (1 < 0 → 1 < 0)
15		simp1 1137	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 12281	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11262	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11290	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11276	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11264	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1139	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11874	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11213	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11449	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5178	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11422	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1120	. . . . . . 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 12284	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11828	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5147	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5147	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5147	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5147	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
41	40	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
42		id 22	. . . . . 6 ⊢ (0 < 1 → 0 < 1)
43		simp1 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
44	43	nnred 12281	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11262	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
46		simp3 1139	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
47		simp2 1138	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
48	44, 45, 46, 47	addgt0d 11838	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
49	48	3exp 1120	. . . . . . 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 12284	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11827	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 960	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 691	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108   ≠ wne 2940   class class class wbr 5143  (class class class)co 7431  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158   < clt 11295  ℕcn 12266

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-nn 12267

This theorem is referenced by:  nnneneg  12301  0nnn  12302  nndivre  12307  nndiv  12312  nndivtr  12313  nnne0d  12316  zdiv  12688  zdivadd  12689  zdivmul  12690  elq  12992  qmulz  12993  qre  12995  qaddcl  13007  qnegcl  13008  qmulcl  13009  qreccl  13011  rpnnen1lem5  13023  nn0ledivnn  13148  fzo1fzo0n0  13754  quoremz  13895  quoremnn0ALT  13897  intfracq  13899  fldiv  13900  fldiv2  13901  modmulnn  13929  modsumfzodifsn  13985  expnnval  14105  expneg  14110  digit2  14275  facdiv  14326  facndiv  14327  bcm1k  14354  bcp1n  14355  bcval5  14357  hashnncl  14405  cshwidxmod  14841  relexpsucnnr  15064  divcnv  15889  harmonic  15895  expcnv  15900  ef0lem  16114  ruclem6  16271  sqrt2irr  16285  dvdsval3  16294  nndivdvds  16299  modmulconst  16325  dvdsdivcl  16353  dvdsflip  16354  divalg2  16442  divalgmod  16443  ndvdssub  16446  nndvdslegcd  16542  divgcdz  16548  divgcdnn  16552  modgcd  16569  gcddiv  16588  gcdzeq  16589  eucalgf  16620  eucalginv  16621  lcmgcdlem  16643  lcmftp  16673  qredeq  16694  qredeu  16695  cncongr1  16704  cncongr2  16705  isprm6  16751  divnumden  16785  divdenle  16786  phimullem  16816  hashgcdlem  16825  phisum  16828  prm23lt5  16852  pythagtriplem10  16858  pythagtriplem8  16861  pythagtriplem9  16862  pccl  16887  pcdiv  16890  pcqcl  16894  pcdvds  16902  pcndvds  16904  pcndvds2  16906  pceq0  16909  pcneg  16912  pcz  16919  pcmpt  16930  fldivp1  16935  pcfac  16937  oddprmdvds  16941  infpnlem2  16949  cshwshashlem1  17133  smndex1n0mnd  18925  mulgnn  19093  mulgnegnn  19102  mulgmodid  19131  oddvdsnn0  19562  odmulgeq  19575  gexnnod  19606  qsssubdrg  21444  prmirredlem  21483  znf1o  21570  znhash  21577  znidomb  21580  znunithash  21583  znrrg  21584  cply1coe0  22305  cply1coe0bi  22306  m2cpm  22747  m2cpminvid2lem  22760  fvmptnn04ifc  22858  vitali  25648  mbfi1fseqlem3  25752  dvexp2  25992  plyeq0lem  26249  abelthlem9  26484  logtayllem  26701  logtayl  26702  logtaylsum  26703  logtayl2  26704  cxpexp  26710  cxproot  26732  root1id  26797  root1eq1  26798  cxpeq  26800  logbgcd1irr  26837  atantayl  26980  atantayl2  26981  leibpilem2  26984  leibpi  26985  birthdaylem2  26995  birthdaylem3  26996  dfef2  27014  emcllem2  27040  emcllem3  27041  zetacvg  27058  lgam1  27107  basellem4  27127  basellem8  27131  basellem9  27132  mumullem2  27223  fsumdvdscom  27228  chtublem  27255  dchrelbas4  27287  bclbnd  27324  lgsval4a  27363  lgsabs1  27380  lgssq2  27382  dchrmusumlema  27537  dchrmusum2  27538  dchrvmasumiflem1  27545  dchrvmaeq0  27548  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0re  27557  ostthlem1  27671  ostth1  27677  pthdlem2lem  29787  wspthsnonn0vne  29937  clwwisshclwwslem  30033  ipasslem4  30853  ipasslem5  30854  divnumden2  32817  1fldgenq  33324  qqhval2  33983  qqhnm  33991  signstfveq0  34592  subfacp1lem6  35190  circum  35679  fz0n  35731  divcnvlin  35733  iprodgam  35742  faclim  35746  nndivsub  36458  poimirlem29  37656  poimirlem31  37658  poimirlem32  37659  heiborlem4  37821  heiborlem6  37823  nnproddivdvdsd  42001  pellexlem1  42840  congrep  42985  jm2.20nn  43009  proot1ex  43208  hashnzfzclim  44341  binomcxplemnotnn0  44375  nnne1ge2  45303  mccllem  45612  clim1fr1  45616  dvnxpaek  45957  dvnprodlem2  45962  wallispilem5  46084  wallispi2lem1  46086  stirlinglem1  46089  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem7  46095  stirlinglem10  46098  stirlinglem12  46100  stirlinglem14  46102  stirlinglem15  46103  fouriersw  46246  vonioolem2  46696  vonicclem2  46699  iccpartiltu  47409  divgcdoddALTV  47669  fpprwppr  47726  isubgr3stgrlem7  47939  gpg3kgrtriexlem5  48043  nnsgrpnmnd  48094  eluz2cnn0n1  48428  mod0mul  48440  modn0mul  48441  blennn  48496  nnpw2blen  48501  digvalnn0  48520  nn0digval  48521  dignn0fr  48522  dignn0ldlem  48523  dig0  48527