Theorem nnne0 12266

Description: A positive integer is nonzero. See nnne0ALT 12270 for a shorter proof using ax-pre-mulgt0 11173. This proof avoids 0lt1 11732, and thus ax-pre-mulgt0 11173, by splitting ax-1ne0 11165 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11173. (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 11165	. . 3 ⊢ 1 ≠ 0
2		1re 11204	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11206	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11320	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 233	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5113	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5113	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5113	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 343	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5113	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 23	. . . . . 6 ⊢ (1 < 0 → 1 < 0)
15		simp1 1152	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 12244	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11205	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11234	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11220	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11207	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1154	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11821	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11154	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11394	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1153	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5147	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11367	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1135	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (1 < 0 → (𝑦 < 0 → (𝑦 + 1) < 0)))
30	29	a2d 30	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((1 < 0 → 𝑦 < 0) → (1 < 0 → (𝑦 + 1) < 0)))
31	7, 9, 11, 13, 14, 30	nnind 12247	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 411	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11775	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5114	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5114	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5114	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 343	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5114	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
41	40	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
42		id 23	. . . . . 6 ⊢ (0 < 1 → 0 < 1)
43		simp1 1152	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
44	43	nnred 12244	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11205	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
46		simp3 1154	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
47		simp2 1153	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
48	44, 45, 46, 47	addgt0d 11785	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
49	48	3exp 1135	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (0 < 1 → (0 < 𝑦 → 0 < (𝑦 + 1))))
50	49	a2d 30	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((0 < 1 → 0 < 𝑦) → (0 < 1 → 0 < (𝑦 + 1))))
51	35, 37, 39, 41, 42, 50	nnind 12247	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 411	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11774	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 972	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 703	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964   class class class wbr 5110  (class class class)co 7408  ℝcr 11095  0cc0 11096  1c1 11097   + caddc 11099   < clt 11239  ℕcn 12229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6300  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ov 7411  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-nn 12230

This theorem is referenced by:  nnneneg  12267  0nnn  12268  nndivre  12273  nndiv  12278  nndivtr  12279  nnne0d  12282  zdiv  12662  zdivadd  12663  zdivmul  12664  elq  12970  qmulz  12971  qre  12973  qaddcl  12985  qnegcl  12986  qmulcl  12987  qreccl  12989  rpnnen1lem5  13001  nn0ledivnn  13127  fzo1fzo0n0  13740  quoremz  13884  quoremnn0ALT  13886  intfracq  13888  fldiv  13889  fldiv2  13890  modmulnn  13918  modsumfzodifsn  13976  expnnval  14096  expneg  14101  digit2  14268  facdiv  14319  facndiv  14320  bcm1k  14347  bcp1n  14348  bcval5  14350  hashnncl  14398  cshwidxmod  14836  relexpsucnnr  15058  divcnv  15903  harmonic  15909  expcnv  15914  ef0lem  16128  ruclem6  16287  sqrt2irr  16301  dvdsval3  16310  nndivdvds  16315  modmulconst  16342  dvdsdivcl  16370  dvdsflip  16371  divalg2  16459  divalgmod  16460  ndvdssub  16463  nndvdslegcd  16559  divgcdz  16565  divgcdnn  16569  modgcd  16586  gcddiv  16605  gcdzeq  16606  eucalgf  16637  eucalginv  16638  lcmgcdlem  16660  lcmftp  16690  qredeq  16711  qredeu  16712  cncongr1  16721  cncongr2  16722  isprm6  16769  divnumden  16803  divdenle  16804  phimullem  16834  hashgcdlem  16843  phisum  16846  prm23lt5  16870  pythagtriplem10  16876  pythagtriplem8  16879  pythagtriplem9  16880  pccl  16905  pcdiv  16908  pcqcl  16912  pcdvds  16920  pcndvds  16922  pcndvds2  16924  pceq0  16927  pcneg  16930  pcz  16937  pcmpt  16948  fldivp1  16953  pcfac  16955  oddprmdvds  16959  infpnlem2  16967  cshwshashlem1  17151  smndex1n0mnd  18970  mulgnn  19137  mulgnegnn  19146  mulgmodid  19175  oddvdsnn0  19610  odmulgeq  19623  gexnnod  19654  qsssubdrg  21541  prmirredlem  21587  znf1o  21666  znhash  21673  znidomb  21676  znunithash  21679  znrrg  21680  cply1coe0  22426  cply1coe0bi  22427  m2cpm  22863  m2cpminvid2lem  22876  fvmptnn04ifc  22974  vitali  25737  mbfi1fseqlem3  25841  dvexp2  26078  plyeq0lem  26332  abelthlem9  26565  logtayllem  26786  logtayl  26787  logtaylsum  26788  logtayl2  26789  cxpexp  26795  cxproot  26817  root1id  26881  root1eq1  26882  cxpeq  26884  logbgcd1irr  26921  atantayl  27064  atantayl2  27065  leibpilem2  27068  leibpi  27069  birthdaylem2  27079  birthdaylem3  27080  dfef2  27097  emcllem2  27123  emcllem3  27124  zetacvg  27141  lgam1  27190  basellem4  27210  basellem8  27214  basellem9  27215  mumullem2  27306  fsumdvdscom  27311  chtublem  27337  dchrelbas4  27369  bclbnd  27406  lgsval4a  27445  lgsabs1  27462  lgssq2  27464  dchrmusumlema  27619  dchrmusum2  27620  dchrvmasumiflem1  27627  dchrvmaeq0  27630  dchrisum0flblem1  27634  dchrisum0flblem2  27635  dchrisum0re  27639  ostthlem1  27753  ostth1  27759  pthdlem2lem  30053  wspthsnonn0vne  30203  clwwisshclwwslem  30302  ipasslem4  31123  ipasslem5  31124  divnumden2  33097  1fldgenq  33582  qqhval2  34313  qqhnm  34321  signstfveq0  34905  subfacp1lem6  35572  circum  36061  fz0n  36118  divcnvlin  36120  iprodgam  36129  faclim  36133  nndivsub  36853  poimirlem29  38183  poimirlem31  38185  poimirlem32  38186  heiborlem4  38348  heiborlem6  38350  nnproddivdvdsd  42652  pellexlem1  43443  congrep  43587  jm2.20nn  43611  proot1ex  43810  hashnzfzclim  44919  binomcxplemnotnn0  44953  nnne1ge2  45897  mccllem  46200  clim1fr1  46204  dvnxpaek  46543  dvnprodlem2  46548  wallispilem5  46670  wallispi2lem1  46672  stirlinglem1  46675  stirlinglem3  46677  stirlinglem4  46678  stirlinglem5  46679  stirlinglem7  46681  stirlinglem10  46684  stirlinglem12  46686  stirlinglem14  46688  stirlinglem15  46689  fouriersw  46832  vonioolem2  47282  vonicclem2  47285  mod0mul  47983  modn0mul  47984  modlt0b  47990  iccpartiltu  48055  divgcdoddALTV  48331  fpprwppr  48388  isubgr3stgrlem7  48621  gpg3kgrtriexlem5  48736  nnsgrpnmnd  48827  eluz2cnn0n1  49171  blennn  49235  nnpw2blen  49240  digvalnn0  49259  nn0digval  49260  dignn0fr  49261  dignn0ldlem  49262  dig0  49266