Theorem nnne0 12202

Description: A positive integer is nonzero. See nnne0ALT 12206 for a shorter proof using ax-pre-mulgt0 11106. This proof avoids 0lt1 11663, and thus ax-pre-mulgt0 11106, by splitting ax-1ne0 11098 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11106. (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 11098	. . 3 ⊢ 1 ≠ 0
2		1re 11135	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11137	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11251	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 230	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5089	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5089	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5089	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5089	. . . . . . 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 12180	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11136	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11165	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11151	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11138	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1139	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11752	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11087	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11325	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5121	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11298	. . . . . . . 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 12183	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11706	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5090	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5090	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5090	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5090	. . . . . . 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 12180	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11136	. . . . . . . . 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 11716	. . . . . . . 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 12183	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11705	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 960	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 692	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933   class class class wbr 5086  (class class class)co 7360  ℝcr 11028  0cc0 11029  1c1 11030   + caddc 11032   < clt 11170  ℕcn 12165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-nn 12166

This theorem is referenced by:  nnneneg  12203  0nnn  12204  nndivre  12209  nndiv  12214  nndivtr  12215  nnne0d  12218  zdiv  12590  zdivadd  12591  zdivmul  12592  elq  12891  qmulz  12892  qre  12894  qaddcl  12906  qnegcl  12907  qmulcl  12908  qreccl  12910  rpnnen1lem5  12922  nn0ledivnn  13048  fzo1fzo0n0  13661  quoremz  13805  quoremnn0ALT  13807  intfracq  13809  fldiv  13810  fldiv2  13811  modmulnn  13839  modsumfzodifsn  13897  expnnval  14017  expneg  14022  digit2  14189  facdiv  14240  facndiv  14241  bcm1k  14268  bcp1n  14269  bcval5  14271  hashnncl  14319  cshwidxmod  14756  relexpsucnnr  14978  divcnv  15809  harmonic  15815  expcnv  15820  ef0lem  16034  ruclem6  16193  sqrt2irr  16207  dvdsval3  16216  nndivdvds  16221  modmulconst  16248  dvdsdivcl  16276  dvdsflip  16277  divalg2  16365  divalgmod  16366  ndvdssub  16369  nndvdslegcd  16465  divgcdz  16471  divgcdnn  16475  modgcd  16492  gcddiv  16511  gcdzeq  16512  eucalgf  16543  eucalginv  16544  lcmgcdlem  16566  lcmftp  16596  qredeq  16617  qredeu  16618  cncongr1  16627  cncongr2  16628  isprm6  16675  divnumden  16709  divdenle  16710  phimullem  16740  hashgcdlem  16749  phisum  16752  prm23lt5  16776  pythagtriplem10  16782  pythagtriplem8  16785  pythagtriplem9  16786  pccl  16811  pcdiv  16814  pcqcl  16818  pcdvds  16826  pcndvds  16828  pcndvds2  16830  pceq0  16833  pcneg  16836  pcz  16843  pcmpt  16854  fldivp1  16859  pcfac  16861  oddprmdvds  16865  infpnlem2  16873  cshwshashlem1  17057  smndex1n0mnd  18874  mulgnn  19042  mulgnegnn  19051  mulgmodid  19080  oddvdsnn0  19510  odmulgeq  19523  gexnnod  19554  qsssubdrg  21416  prmirredlem  21462  znf1o  21541  znhash  21548  znidomb  21551  znunithash  21554  znrrg  21555  cply1coe0  22276  cply1coe0bi  22277  m2cpm  22716  m2cpminvid2lem  22729  fvmptnn04ifc  22827  vitali  25590  mbfi1fseqlem3  25694  dvexp2  25931  plyeq0lem  26185  abelthlem9  26418  logtayllem  26636  logtayl  26637  logtaylsum  26638  logtayl2  26639  cxpexp  26645  cxproot  26667  root1id  26731  root1eq1  26732  cxpeq  26734  logbgcd1irr  26771  atantayl  26914  atantayl2  26915  leibpilem2  26918  leibpi  26919  birthdaylem2  26929  birthdaylem3  26930  dfef2  26948  emcllem2  26974  emcllem3  26975  zetacvg  26992  lgam1  27041  basellem4  27061  basellem8  27065  basellem9  27066  mumullem2  27157  fsumdvdscom  27162  chtublem  27188  dchrelbas4  27220  bclbnd  27257  lgsval4a  27296  lgsabs1  27313  lgssq2  27315  dchrmusumlema  27470  dchrmusum2  27471  dchrvmasumiflem1  27478  dchrvmaeq0  27481  dchrisum0flblem1  27485  dchrisum0flblem2  27486  dchrisum0re  27490  ostthlem1  27604  ostth1  27610  pthdlem2lem  29850  wspthsnonn0vne  30000  clwwisshclwwslem  30099  ipasslem4  30920  ipasslem5  30921  divnumden2  32904  1fldgenq  33398  qqhval2  34142  qqhnm  34150  signstfveq0  34737  subfacp1lem6  35383  circum  35872  fz0n  35929  divcnvlin  35931  iprodgam  35940  faclim  35944  nndivsub  36655  poimirlem29  37984  poimirlem31  37986  poimirlem32  37987  heiborlem4  38149  heiborlem6  38151  nnproddivdvdsd  42453  pellexlem1  43275  congrep  43419  jm2.20nn  43443  proot1ex  43642  hashnzfzclim  44767  binomcxplemnotnn0  44801  nnne1ge2  45742  mccllem  46045  clim1fr1  46049  dvnxpaek  46388  dvnprodlem2  46393  wallispilem5  46515  wallispi2lem1  46517  stirlinglem1  46520  stirlinglem3  46522  stirlinglem4  46523  stirlinglem5  46524  stirlinglem7  46526  stirlinglem10  46529  stirlinglem12  46531  stirlinglem14  46533  stirlinglem15  46534  fouriersw  46677  vonioolem2  47127  vonicclem2  47130  mod0mul  47822  modn0mul  47823  modlt0b  47829  iccpartiltu  47894  divgcdoddALTV  48170  fpprwppr  48227  isubgr3stgrlem7  48460  gpg3kgrtriexlem5  48575  nnsgrpnmnd  48666  eluz2cnn0n1  48999  blennn  49063  nnpw2blen  49068  digvalnn0  49087  nn0digval  49088  dignn0fr  49089  dignn0ldlem  49090  dig0  49094