Theorem nnne0 11659

Description: A positive integer is nonzero. See nnne0ALT 11663 for a shorter proof using ax-pre-mulgt0 10603. This proof avoids 0lt1 11151, and thus ax-pre-mulgt0 10603, by splitting ax-1ne0 10595 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 10603. (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 10595	. . 3 ⊢ 1 ≠ 0
2		1re 10630	. . . 4 ⊢ 1 ∈ ℝ
3		0re 10632	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 10743	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 233	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5033	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5033	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5033	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5033	. . . . . . . 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 11640	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 10631	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 10659	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 10645	. . . . . . . . . . 11 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 10633	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1135	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11240	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 10584	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
25	24	addid2i 10817	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
26		simp2 1134	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5065	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 10790	. . . . . . . . 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 11643	. . . . . 6 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 410	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11194	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34	33	ex 416	. . 3 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 ≠ 0))
35		breq2 5034	. . . . . . . 8 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
36	35	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
37		breq2 5034	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
38	37	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
39		breq2 5034	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
40	39	imbi2d 344	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
41		breq2 5034	. . . . . . . 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 11640	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
46		1red 10631	. . . . . . . . . 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 11204	. . . . . . . . 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 11643	. . . . . 6 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
53	52	imp 410	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
54	53	gt0ne0d 11193	. . . 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 2987   class class class wbr 5030  (class class class)co 7135  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529   < clt 10664  ℕcn 11625

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 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-nn 11626

This theorem is referenced by:  nnneneg  11660  0nnn  11661  nndivre  11666  nndiv  11671  nndivtr  11672  nnne0d  11675  zdiv  12040  zdivadd  12041  zdivmul  12042  elq  12338  qmulz  12339  qre  12341  qaddcl  12352  qnegcl  12353  qmulcl  12354  qreccl  12356  rpnnen1lem5  12368  nn0ledivnn  12490  fzo1fzo0n0  13083  quoremz  13218  quoremnn0ALT  13220  intfracq  13222  fldiv  13223  fldiv2  13224  modmulnn  13252  modsumfzodifsn  13307  expnnval  13428  expneg  13433  digit2  13593  facdiv  13643  facndiv  13644  bcm1k  13671  bcp1n  13672  bcval5  13674  hashnncl  13723  cshwidxmod  14156  relexpsucnnr  14376  divcnv  15200  harmonic  15206  expcnv  15211  ef0lem  15424  ruclem6  15580  sqrt2irr  15594  dvdsval3  15603  nndivdvds  15608  modmulconst  15633  dvdsdivcl  15658  dvdsflip  15659  divalg2  15746  divalgmod  15747  ndvdssub  15750  nndvdslegcd  15844  divgcdz  15850  divgcdnn  15853  modgcd  15870  gcddiv  15889  gcdzeq  15892  eucalgf  15917  eucalginv  15918  lcmgcdlem  15940  lcmftp  15970  qredeq  15991  qredeu  15992  cncongr1  16001  cncongr2  16002  isprm6  16048  divnumden  16078  divdenle  16079  phimullem  16106  hashgcdlem  16115  phisum  16117  prm23lt5  16141  pythagtriplem10  16147  pythagtriplem8  16150  pythagtriplem9  16151  pccl  16176  pcdiv  16179  pcqcl  16183  pcdvds  16190  pcndvds  16192  pcndvds2  16194  pceq0  16197  pcneg  16200  pcz  16207  pcmpt  16218  fldivp1  16223  pcfac  16225  oddprmdvds  16229  infpnlem2  16237  cshwshashlem1  16421  smndex1n0mnd  18069  mulgnn  18224  mulgnegnn  18230  mulgmodid  18258  oddvdsnn0  18664  odmulgeq  18676  gexnnod  18705  qsssubdrg  20150  prmirredlem  20186  znf1o  20243  znhash  20250  znidomb  20253  znunithash  20256  znrrg  20257  cply1coe0  20928  cply1coe0bi  20929  m2cpm  21346  m2cpminvid2lem  21359  fvmptnn04ifc  21457  vitali  24217  mbfi1fseqlem3  24321  dvexp2  24557  plyeq0lem  24807  abelthlem9  25035  logtayllem  25250  logtayl  25251  logtaylsum  25252  logtayl2  25253  cxpexp  25259  cxproot  25281  root1id  25343  root1eq1  25344  cxpeq  25346  logbgcd1irr  25380  atantayl  25523  atantayl2  25524  leibpilem2  25527  leibpi  25528  birthdaylem2  25538  birthdaylem3  25539  dfef2  25556  emcllem2  25582  emcllem3  25583  zetacvg  25600  lgam1  25649  basellem4  25669  basellem8  25673  basellem9  25674  mumullem2  25765  fsumdvdscom  25770  chtublem  25795  dchrelbas4  25827  bclbnd  25864  lgsval4a  25903  lgsabs1  25920  lgssq2  25922  dchrmusumlema  26077  dchrmusum2  26078  dchrvmasumiflem1  26085  dchrvmaeq0  26088  dchrisum0flblem1  26092  dchrisum0flblem2  26093  dchrisum0re  26097  ostthlem1  26211  ostth1  26217  pthdlem2lem  27556  wspthsnonn0vne  27703  clwwisshclwwslem  27799  ipasslem4  28617  ipasslem5  28618  divnumden2  30560  qqhval2  31333  qqhnm  31341  signstfveq0  31957  subfacp1lem6  32545  circum  33030  fz0n  33075  divcnvlin  33077  iprodgam  33087  faclim  33091  nndivsub  33918  poimirlem29  35086  poimirlem31  35088  poimirlem32  35089  heiborlem4  35252  heiborlem6  35254  nnproddivdvdsd  39289  pellexlem1  39770  congrep  39914  jm2.20nn  39938  proot1ex  40145  hashnzfzclim  41026  binomcxplemnotnn0  41060  nnne1ge2  41923  mccllem  42239  clim1fr1  42243  dvnxpaek  42584  dvnprodlem2  42589  wallispilem5  42711  wallispi2lem1  42713  stirlinglem1  42716  stirlinglem3  42718  stirlinglem4  42719  stirlinglem5  42720  stirlinglem7  42722  stirlinglem10  42725  stirlinglem12  42727  stirlinglem14  42729  stirlinglem15  42730  fouriersw  42873  vonioolem2  43320  vonicclem2  43323  iccpartiltu  43939  divgcdoddALTV  44200  fpprwppr  44257  nnsgrpnmnd  44438  eluz2cnn0n1  44920  mod0mul  44933  modn0mul  44934  blennn  44989  nnpw2blen  44994  digvalnn0  45013  nn0digval  45014  dignn0fr  45015  dignn0ldlem  45016  dig0  45020