Theorem nnne0 11721

Description: A positive integer is nonzero. See nnne0ALT 11725 for a shorter proof using ax-pre-mulgt0 10665. This proof avoids 0lt1 11213, and thus ax-pre-mulgt0 10665, by splitting ax-1ne0 10657 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 10665. (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 10657	. . 3 ⊢ 1 ≠ 0
2		1re 10692	. . . 4 ⊢ 1 ∈ ℝ
3		0re 10694	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 10805	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 233	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5039	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5039	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5039	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5039	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 22	. . . . . . 7 ⊢ (1 < 0 → 1 < 0)
15		simp1 1133	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 11702	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 10693	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 10721	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 10707	. . . . . . . . . . 11 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 10695	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1135	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11302	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 10646	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
25	24	addid2i 10879	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
26		simp2 1134	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5071	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 10852	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1116	. . . . . . . 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 11705	. . . . . 6 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 410	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11256	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34	33	ex 416	. . 3 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 ≠ 0))
35		breq2 5040	. . . . . . . 8 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
36	35	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
37		breq2 5040	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
38	37	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
39		breq2 5040	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
40	39	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
41		breq2 5040	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
42	41	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
43		id 22	. . . . . . 7 ⊢ (0 < 1 → 0 < 1)
44		simp1 1133	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
45	44	nnred 11702	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
46		1red 10693	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
47		simp3 1135	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
48		simp2 1134	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
49	45, 46, 47, 48	addgt0d 11266	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
50	49	3exp 1116	. . . . . . . 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 11705	. . . . . 6 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
53	52	imp 410	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
54	53	gt0ne0d 11255	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
55	54	ex 416	. . 3 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 𝐴 ≠ 0))
56	34, 55	jaod 856	. 2 ⊢ (𝐴 ∈ ℕ → ((1 < 0 ∨ 0 < 1) → 𝐴 ≠ 0))
57	5, 56	mpi 20	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951   class class class wbr 5036  (class class class)co 7156  ℝcr 10587  0cc0 10588  1c1 10589   + caddc 10591   < clt 10726  ℕcn 11687

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-ov 7159  df-om 7586  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-er 8305  df-en 8541  df-dom 8542  df-sdom 8543  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-nn 11688

This theorem is referenced by:  nnneneg  11722  0nnn  11723  nndivre  11728  nndiv  11733  nndivtr  11734  nnne0d  11737  zdiv  12104  zdivadd  12105  zdivmul  12106  elq  12403  qmulz  12404  qre  12406  qaddcl  12418  qnegcl  12419  qmulcl  12420  qreccl  12422  rpnnen1lem5  12434  nn0ledivnn  12556  fzo1fzo0n0  13150  quoremz  13285  quoremnn0ALT  13287  intfracq  13289  fldiv  13290  fldiv2  13291  modmulnn  13319  modsumfzodifsn  13374  expnnval  13495  expneg  13500  digit2  13660  facdiv  13710  facndiv  13711  bcm1k  13738  bcp1n  13739  bcval5  13741  hashnncl  13790  cshwidxmod  14225  relexpsucnnr  14445  divcnv  15269  harmonic  15275  expcnv  15280  ef0lem  15493  ruclem6  15649  sqrt2irr  15663  dvdsval3  15672  nndivdvds  15677  modmulconst  15702  dvdsdivcl  15730  dvdsflip  15731  divalg2  15819  divalgmod  15820  ndvdssub  15823  nndvdslegcd  15917  divgcdz  15923  divgcdnn  15927  modgcd  15944  gcddiv  15963  gcdzeq  15966  eucalgf  15992  eucalginv  15993  lcmgcdlem  16015  lcmftp  16045  qredeq  16066  qredeu  16067  cncongr1  16076  cncongr2  16077  isprm6  16123  divnumden  16156  divdenle  16157  phimullem  16184  hashgcdlem  16193  phisum  16195  prm23lt5  16219  pythagtriplem10  16225  pythagtriplem8  16228  pythagtriplem9  16229  pccl  16254  pcdiv  16257  pcqcl  16261  pcdvds  16268  pcndvds  16270  pcndvds2  16272  pceq0  16275  pcneg  16278  pcz  16285  pcmpt  16296  fldivp1  16301  pcfac  16303  oddprmdvds  16307  infpnlem2  16315  cshwshashlem1  16500  smndex1n0mnd  18156  mulgnn  18312  mulgnegnn  18318  mulgmodid  18346  oddvdsnn0  18752  odmulgeq  18764  gexnnod  18793  qsssubdrg  20238  prmirredlem  20275  znf1o  20332  znhash  20339  znidomb  20342  znunithash  20345  znrrg  20346  cply1coe0  21036  cply1coe0bi  21037  m2cpm  21454  m2cpminvid2lem  21467  fvmptnn04ifc  21565  vitali  24326  mbfi1fseqlem3  24430  dvexp2  24666  plyeq0lem  24919  abelthlem9  25147  logtayllem  25362  logtayl  25363  logtaylsum  25364  logtayl2  25365  cxpexp  25371  cxproot  25393  root1id  25455  root1eq1  25456  cxpeq  25458  logbgcd1irr  25492  atantayl  25635  atantayl2  25636  leibpilem2  25639  leibpi  25640  birthdaylem2  25650  birthdaylem3  25651  dfef2  25668  emcllem2  25694  emcllem3  25695  zetacvg  25712  lgam1  25761  basellem4  25781  basellem8  25785  basellem9  25786  mumullem2  25877  fsumdvdscom  25882  chtublem  25907  dchrelbas4  25939  bclbnd  25976  lgsval4a  26015  lgsabs1  26032  lgssq2  26034  dchrmusumlema  26189  dchrmusum2  26190  dchrvmasumiflem1  26197  dchrvmaeq0  26200  dchrisum0flblem1  26204  dchrisum0flblem2  26205  dchrisum0re  26209  ostthlem1  26323  ostth1  26329  pthdlem2lem  27668  wspthsnonn0vne  27815  clwwisshclwwslem  27911  ipasslem4  28729  ipasslem5  28730  divnumden2  30668  qqhval2  31463  qqhnm  31471  signstfveq0  32087  subfacp1lem6  32675  circum  33160  fz0n  33223  divcnvlin  33225  iprodgam  33235  faclim  33239  nndivsub  34229  poimirlem29  35400  poimirlem31  35402  poimirlem32  35403  heiborlem4  35566  heiborlem6  35568  nnproddivdvdsd  39602  pellexlem1  40178  congrep  40322  jm2.20nn  40346  proot1ex  40553  hashnzfzclim  41434  binomcxplemnotnn0  41468  nnne1ge2  42326  mccllem  42640  clim1fr1  42644  dvnxpaek  42985  dvnprodlem2  42990  wallispilem5  43112  wallispi2lem1  43114  stirlinglem1  43117  stirlinglem3  43119  stirlinglem4  43120  stirlinglem5  43121  stirlinglem7  43123  stirlinglem10  43126  stirlinglem12  43128  stirlinglem14  43130  stirlinglem15  43131  fouriersw  43274  vonioolem2  43721  vonicclem2  43724  iccpartiltu  44356  divgcdoddALTV  44616  fpprwppr  44673  nnsgrpnmnd  44854  eluz2cnn0n1  45334  mod0mul  45347  modn0mul  45348  blennn  45403  nnpw2blen  45408  digvalnn0  45427  nn0digval  45428  dignn0fr  45429  dignn0ldlem  45430  dig0  45434