Theorem nnne0 11674

Description: A positive integer is nonzero. See nnne0ALT 11678 for a shorter proof using ax-pre-mulgt0 10616. This proof avoids 0lt1 11164, and thus ax-pre-mulgt0 10616, by splitting ax-1ne0 10608 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 10616. (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 10608	. . 3 ⊢ 1 ≠ 0
2		1re 10643	. . . 4 ⊢ 1 ∈ ℝ
3		0re 10645	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 10756	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 232	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5071	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5071	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5071	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5071	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 22	. . . . . . 7 ⊢ (1 < 0 → 1 < 0)
15		simp1 1132	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 11655	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 10644	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 10672	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 10658	. . . . . . . . . . 11 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 10646	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1134	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11253	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 10597	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
25	24	addid2i 10830	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
26		simp2 1133	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5103	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 10803	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1115	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (1 < 0 → (𝑦 < 0 → (𝑦 + 1) < 0)))
30	29	a2d 29	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((1 < 0 → 𝑦 < 0) → (1 < 0 → (𝑦 + 1) < 0)))
31	7, 9, 11, 13, 14, 30	nnind 11658	. . . . . 6 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 409	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11207	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34	33	ex 415	. . 3 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 ≠ 0))
35		breq2 5072	. . . . . . . 8 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
36	35	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
37		breq2 5072	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
38	37	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
39		breq2 5072	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
40	39	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
41		breq2 5072	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
42	41	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
43		id 22	. . . . . . 7 ⊢ (0 < 1 → 0 < 1)
44		simp1 1132	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
45	44	nnred 11655	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
46		1red 10644	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
47		simp3 1134	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
48		simp2 1133	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
49	45, 46, 47, 48	addgt0d 11217	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
50	49	3exp 1115	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (0 < 1 → (0 < 𝑦 → 0 < (𝑦 + 1))))
51	50	a2d 29	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((0 < 1 → 0 < 𝑦) → (0 < 1 → 0 < (𝑦 + 1))))
52	36, 38, 40, 42, 43, 51	nnind 11658	. . . . . 6 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
53	52	imp 409	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
54	53	gt0ne0d 11206	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
55	54	ex 415	. . 3 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 𝐴 ≠ 0))
56	34, 55	jaod 855	. 2 ⊢ (𝐴 ∈ ℕ → ((1 < 0 ∨ 0 < 1) → 𝐴 ≠ 0))
57	5, 56	mpi 20	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3018   class class class wbr 5068  (class class class)co 7158  ℝcr 10538  0cc0 10539  1c1 10540   + caddc 10542   < clt 10677  ℕcn 11640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-nn 11641

This theorem is referenced by:  nnneneg  11675  0nnn  11676  nndivre  11681  nndiv  11686  nndivtr  11687  nnne0d  11690  zdiv  12055  zdivadd  12056  zdivmul  12057  elq  12353  qmulz  12354  qre  12356  qaddcl  12367  qnegcl  12368  qmulcl  12369  qreccl  12371  rpnnen1lem5  12383  nn0ledivnn  12505  fzo1fzo0n0  13091  quoremz  13226  quoremnn0ALT  13228  intfracq  13230  fldiv  13231  fldiv2  13232  modmulnn  13260  modsumfzodifsn  13315  expnnval  13435  expneg  13440  digit2  13600  facdiv  13650  facndiv  13651  bcm1k  13678  bcp1n  13679  bcval5  13681  hashnncl  13730  cshwidxmod  14167  relexpsucnnr  14386  divcnv  15210  harmonic  15216  expcnv  15221  ef0lem  15434  ruclem6  15590  sqrt2irr  15604  dvdsval3  15613  nndivdvds  15618  modmulconst  15643  dvdsdivcl  15668  dvdsflip  15669  divalg2  15758  divalgmod  15759  ndvdssub  15762  nndvdslegcd  15856  divgcdz  15862  divgcdnn  15865  modgcd  15882  gcddiv  15901  gcdzeq  15904  eucalgf  15929  eucalginv  15930  lcmgcdlem  15952  lcmftp  15982  qredeq  16003  qredeu  16004  cncongr1  16013  cncongr2  16014  isprm6  16060  divnumden  16090  divdenle  16091  phimullem  16118  hashgcdlem  16127  phisum  16129  prm23lt5  16153  pythagtriplem10  16159  pythagtriplem8  16162  pythagtriplem9  16163  pccl  16188  pcdiv  16191  pcqcl  16195  pcdvds  16202  pcndvds  16204  pcndvds2  16206  pceq0  16209  pcneg  16212  pcz  16219  pcmpt  16230  fldivp1  16235  pcfac  16237  oddprmdvds  16241  infpnlem2  16249  cshwshashlem1  16431  smndex1n0mnd  18079  mulgnn  18234  mulgnegnn  18240  mulgmodid  18268  oddvdsnn0  18674  odmulgeq  18686  gexnnod  18715  cply1coe0  20469  cply1coe0bi  20470  qsssubdrg  20606  prmirredlem  20642  znf1o  20700  znhash  20707  znidomb  20710  znunithash  20713  znrrg  20714  m2cpm  21351  m2cpminvid2lem  21364  fvmptnn04ifc  21462  vitali  24216  mbfi1fseqlem3  24320  dvexp2  24553  plyeq0lem  24802  abelthlem9  25030  logtayllem  25244  logtayl  25245  logtaylsum  25246  logtayl2  25247  cxpexp  25253  cxproot  25275  root1id  25337  root1eq1  25338  cxpeq  25340  logbgcd1irr  25374  atantayl  25517  atantayl2  25518  leibpilem2  25521  leibpi  25522  birthdaylem2  25532  birthdaylem3  25533  dfef2  25550  emcllem2  25576  emcllem3  25577  zetacvg  25594  lgam1  25643  basellem4  25663  basellem8  25667  basellem9  25668  mumullem2  25759  fsumdvdscom  25764  chtublem  25789  dchrelbas4  25821  bclbnd  25858  lgsval4a  25897  lgsabs1  25914  lgssq2  25916  dchrmusumlema  26071  dchrmusum2  26072  dchrvmasumiflem1  26079  dchrvmaeq0  26082  dchrisum0flblem1  26086  dchrisum0flblem2  26087  dchrisum0re  26091  ostthlem1  26205  ostth1  26211  pthdlem2lem  27550  wspthsnonn0vne  27698  clwwisshclwwslem  27794  ipasslem4  28613  ipasslem5  28614  divnumden2  30536  qqhval2  31225  qqhnm  31233  signstfveq0  31849  subfacp1lem6  32434  circum  32919  fz0n  32964  divcnvlin  32966  iprodgam  32976  faclim  32980  nndivsub  33807  poimirlem29  34923  poimirlem31  34925  poimirlem32  34926  heiborlem4  35094  heiborlem6  35096  pellexlem1  39433  congrep  39577  jm2.20nn  39601  proot1ex  39808  hashnzfzclim  40661  binomcxplemnotnn0  40695  nnne1ge2  41565  mccllem  41885  clim1fr1  41889  dvnxpaek  42234  dvnprodlem2  42239  wallispilem5  42361  wallispi2lem1  42363  stirlinglem1  42366  stirlinglem3  42368  stirlinglem4  42369  stirlinglem5  42370  stirlinglem7  42372  stirlinglem10  42375  stirlinglem12  42377  stirlinglem14  42379  stirlinglem15  42380  fouriersw  42523  vonioolem2  42970  vonicclem2  42973  iccpartiltu  43589  divgcdoddALTV  43854  fpprwppr  43911  nnsgrpnmnd  44092  eluz2cnn0n1  44573  mod0mul  44586  modn0mul  44587  blennn  44642  nnpw2blen  44647  digvalnn0  44666  nn0digval  44667  dignn0fr  44668  dignn0ldlem  44669  dig0  44673