Theorem nnne0 12241

Description: A positive integer is nonzero. See nnne0ALT 12245 for a shorter proof using ax-pre-mulgt0 11144. This proof avoids 0lt1 11703, and thus ax-pre-mulgt0 11144, by splitting ax-1ne0 11136 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11144. (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 11136	. . 3 ⊢ 1 ≠ 0
2		1re 11175	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11177	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11291	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 232	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5100	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 342	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5100	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 342	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5100	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 342	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5100	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 342	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 22	. . . . . 6 ⊢ (1 < 0 → 1 < 0)
15		simp1 1148	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 12219	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11176	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11205	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11191	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11178	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1150	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11792	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11125	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11365	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1149	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5132	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11338	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1131	. . . . . . 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 12222	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 410	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11746	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5101	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 342	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5101	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 342	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5101	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 342	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5101	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
41	40	imbi2d 342	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
42		id 22	. . . . . 6 ⊢ (0 < 1 → 0 < 1)
43		simp1 1148	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
44	43	nnred 12219	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11176	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
46		simp3 1150	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
47		simp2 1149	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
48	44, 45, 46, 47	addgt0d 11756	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
49	48	3exp 1131	. . . . . . 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 12222	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 410	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11745	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 970	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 701	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141   ≠ wne 2956   class class class wbr 5097  (class class class)co 7391  ℝcr 11066  0cc0 11067  1c1 11068   + caddc 11070   < clt 11210  ℕcn 12204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-nn 12205

This theorem is referenced by:  nnneneg  12242  0nnn  12243  nndivre  12248  nndiv  12253  nndivtr  12254  nnne0d  12257  zdiv  12637  zdivadd  12638  zdivmul  12639  elq  12945  qmulz  12946  qre  12948  qaddcl  12960  qnegcl  12961  qmulcl  12962  qreccl  12964  rpnnen1lem5  12976  nn0ledivnn  13102  fzo1fzo0n0  13715  quoremz  13859  quoremnn0ALT  13861  intfracq  13863  fldiv  13864  fldiv2  13865  modmulnn  13893  modsumfzodifsn  13951  expnnval  14071  expneg  14076  digit2  14243  facdiv  14294  facndiv  14295  bcm1k  14322  bcp1n  14323  bcval5  14325  hashnncl  14373  cshwidxmod  14810  relexpsucnnr  15032  divcnv  15874  harmonic  15880  expcnv  15885  ef0lem  16099  ruclem6  16258  sqrt2irr  16272  dvdsval3  16281  nndivdvds  16286  modmulconst  16313  dvdsdivcl  16341  dvdsflip  16342  divalg2  16430  divalgmod  16431  ndvdssub  16434  nndvdslegcd  16530  divgcdz  16536  divgcdnn  16540  modgcd  16557  gcddiv  16576  gcdzeq  16577  eucalgf  16608  eucalginv  16609  lcmgcdlem  16631  lcmftp  16661  qredeq  16682  qredeu  16683  cncongr1  16692  cncongr2  16693  isprm6  16740  divnumden  16774  divdenle  16775  phimullem  16805  hashgcdlem  16814  phisum  16817  prm23lt5  16841  pythagtriplem10  16847  pythagtriplem8  16850  pythagtriplem9  16851  pccl  16876  pcdiv  16879  pcqcl  16883  pcdvds  16891  pcndvds  16893  pcndvds2  16895  pceq0  16898  pcneg  16901  pcz  16908  pcmpt  16919  fldivp1  16924  pcfac  16926  oddprmdvds  16930  infpnlem2  16938  cshwshashlem1  17122  smndex1n0mnd  18940  mulgnn  19108  mulgnegnn  19117  mulgmodid  19146  oddvdsnn0  19575  odmulgeq  19588  gexnnod  19619  qsssubdrg  21466  prmirredlem  21512  znf1o  21591  znhash  21598  znidomb  21601  znunithash  21604  znrrg  21605  cply1coe0  22352  cply1coe0bi  22353  m2cpm  22789  m2cpminvid2lem  22802  fvmptnn04ifc  22900  vitali  25663  mbfi1fseqlem3  25767  dvexp2  26004  plyeq0lem  26258  abelthlem9  26491  logtayllem  26712  logtayl  26713  logtaylsum  26714  logtayl2  26715  cxpexp  26721  cxproot  26743  root1id  26807  root1eq1  26808  cxpeq  26810  logbgcd1irr  26847  atantayl  26990  atantayl2  26991  leibpilem2  26994  leibpi  26995  birthdaylem2  27005  birthdaylem3  27006  dfef2  27023  emcllem2  27049  emcllem3  27050  zetacvg  27067  lgam1  27116  basellem4  27136  basellem8  27140  basellem9  27141  mumullem2  27232  fsumdvdscom  27237  chtublem  27263  dchrelbas4  27295  bclbnd  27332  lgsval4a  27371  lgsabs1  27388  lgssq2  27390  dchrmusumlema  27545  dchrmusum2  27546  dchrvmasumiflem1  27553  dchrvmaeq0  27556  dchrisum0flblem1  27560  dchrisum0flblem2  27561  dchrisum0re  27565  ostthlem1  27679  ostth1  27685  pthdlem2lem  29924  wspthsnonn0vne  30074  clwwisshclwwslem  30173  ipasslem4  30994  ipasslem5  30995  divnumden2  32979  1fldgenq  33470  qqhval2  34240  qqhnm  34248  signstfveq0  34832  subfacp1lem6  35496  circum  35985  fz0n  36042  divcnvlin  36044  iprodgam  36053  faclim  36057  nndivsub  36778  poimirlem29  38109  poimirlem31  38111  poimirlem32  38112  heiborlem4  38274  heiborlem6  38276  nnproddivdvdsd  42578  pellexlem1  43367  congrep  43511  jm2.20nn  43535  proot1ex  43734  hashnzfzclim  44859  binomcxplemnotnn0  44893  nnne1ge2  45831  mccllem  46134  clim1fr1  46138  dvnxpaek  46477  dvnprodlem2  46482  wallispilem5  46604  wallispi2lem1  46606  stirlinglem1  46609  stirlinglem3  46611  stirlinglem4  46612  stirlinglem5  46613  stirlinglem7  46615  stirlinglem10  46618  stirlinglem12  46620  stirlinglem14  46622  stirlinglem15  46623  fouriersw  46766  vonioolem2  47216  vonicclem2  47219  mod0mul  47917  modn0mul  47918  modlt0b  47924  iccpartiltu  47989  divgcdoddALTV  48265  fpprwppr  48322  isubgr3stgrlem7  48555  gpg3kgrtriexlem5  48670  nnsgrpnmnd  48761  eluz2cnn0n1  49094  blennn  49158  nnpw2blen  49163  digvalnn0  49182  nn0digval  49183  dignn0fr  49184  dignn0ldlem  49185  dig0  49189