Theorem nnne0 12298

Description: A positive integer is nonzero. See nnne0ALT 12302 for a shorter proof using ax-pre-mulgt0 11230. This proof avoids 0lt1 11783, and thus ax-pre-mulgt0 11230, by splitting ax-1ne0 11222 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11230. (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 11222	. . 3 ⊢ 1 ≠ 0
2		1re 11259	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11261	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11373	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 230	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5151	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5151	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5151	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5151	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 22	. . . . . 6 ⊢ (1 < 0 → 1 < 0)
15		simp1 1135	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 12279	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11260	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11288	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11274	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11262	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11872	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11211	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11447	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1136	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5183	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11420	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1118	. . . . . . 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 12282	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11826	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5152	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5152	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5152	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5152	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
41	40	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
42		id 22	. . . . . 6 ⊢ (0 < 1 → 0 < 1)
43		simp1 1135	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
44	43	nnred 12279	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11260	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
46		simp3 1137	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
47		simp2 1136	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
48	44, 45, 46, 47	addgt0d 11836	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
49	48	3exp 1118	. . . . . . 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 12282	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11825	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 959	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 691	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106   ≠ wne 2938   class class class wbr 5148  (class class class)co 7431  ℝcr 11152  0cc0 11153  1c1 11154   + caddc 11156   < clt 11293  ℕcn 12264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-om 7888  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-nn 12265

This theorem is referenced by:  nnneneg  12299  0nnn  12300  nndivre  12305  nndiv  12310  nndivtr  12311  nnne0d  12314  zdiv  12686  zdivadd  12687  zdivmul  12688  elq  12990  qmulz  12991  qre  12993  qaddcl  13005  qnegcl  13006  qmulcl  13007  qreccl  13009  rpnnen1lem5  13021  nn0ledivnn  13146  fzo1fzo0n0  13751  quoremz  13892  quoremnn0ALT  13894  intfracq  13896  fldiv  13897  fldiv2  13898  modmulnn  13926  modsumfzodifsn  13982  expnnval  14102  expneg  14107  digit2  14272  facdiv  14323  facndiv  14324  bcm1k  14351  bcp1n  14352  bcval5  14354  hashnncl  14402  cshwidxmod  14838  relexpsucnnr  15061  divcnv  15886  harmonic  15892  expcnv  15897  ef0lem  16111  ruclem6  16268  sqrt2irr  16282  dvdsval3  16291  nndivdvds  16296  modmulconst  16322  dvdsdivcl  16350  dvdsflip  16351  divalg2  16439  divalgmod  16440  ndvdssub  16443  nndvdslegcd  16539  divgcdz  16545  divgcdnn  16549  modgcd  16566  gcddiv  16585  gcdzeq  16586  eucalgf  16617  eucalginv  16618  lcmgcdlem  16640  lcmftp  16670  qredeq  16691  qredeu  16692  cncongr1  16701  cncongr2  16702  isprm6  16748  divnumden  16782  divdenle  16783  phimullem  16813  hashgcdlem  16822  phisum  16824  prm23lt5  16848  pythagtriplem10  16854  pythagtriplem8  16857  pythagtriplem9  16858  pccl  16883  pcdiv  16886  pcqcl  16890  pcdvds  16898  pcndvds  16900  pcndvds2  16902  pceq0  16905  pcneg  16908  pcz  16915  pcmpt  16926  fldivp1  16931  pcfac  16933  oddprmdvds  16937  infpnlem2  16945  cshwshashlem1  17130  smndex1n0mnd  18938  mulgnn  19106  mulgnegnn  19115  mulgmodid  19144  oddvdsnn0  19577  odmulgeq  19590  gexnnod  19621  qsssubdrg  21462  prmirredlem  21501  znf1o  21588  znhash  21595  znidomb  21598  znunithash  21601  znrrg  21602  cply1coe0  22321  cply1coe0bi  22322  m2cpm  22763  m2cpminvid2lem  22776  fvmptnn04ifc  22874  vitali  25662  mbfi1fseqlem3  25767  dvexp2  26007  plyeq0lem  26264  abelthlem9  26499  logtayllem  26716  logtayl  26717  logtaylsum  26718  logtayl2  26719  cxpexp  26725  cxproot  26747  root1id  26812  root1eq1  26813  cxpeq  26815  logbgcd1irr  26852  atantayl  26995  atantayl2  26996  leibpilem2  26999  leibpi  27000  birthdaylem2  27010  birthdaylem3  27011  dfef2  27029  emcllem2  27055  emcllem3  27056  zetacvg  27073  lgam1  27122  basellem4  27142  basellem8  27146  basellem9  27147  mumullem2  27238  fsumdvdscom  27243  chtublem  27270  dchrelbas4  27302  bclbnd  27339  lgsval4a  27378  lgsabs1  27395  lgssq2  27397  dchrmusumlema  27552  dchrmusum2  27553  dchrvmasumiflem1  27560  dchrvmaeq0  27563  dchrisum0flblem1  27567  dchrisum0flblem2  27568  dchrisum0re  27572  ostthlem1  27686  ostth1  27692  pthdlem2lem  29800  wspthsnonn0vne  29947  clwwisshclwwslem  30043  ipasslem4  30863  ipasslem5  30864  divnumden2  32822  1fldgenq  33304  qqhval2  33945  qqhnm  33953  signstfveq0  34571  subfacp1lem6  35170  circum  35659  fz0n  35711  divcnvlin  35713  iprodgam  35722  faclim  35726  nndivsub  36440  poimirlem29  37636  poimirlem31  37638  poimirlem32  37639  heiborlem4  37801  heiborlem6  37803  nnproddivdvdsd  41982  pellexlem1  42817  congrep  42962  jm2.20nn  42986  proot1ex  43185  hashnzfzclim  44318  binomcxplemnotnn0  44352  nnne1ge2  45242  mccllem  45553  clim1fr1  45557  dvnxpaek  45898  dvnprodlem2  45903  wallispilem5  46025  wallispi2lem1  46027  stirlinglem1  46030  stirlinglem3  46032  stirlinglem4  46033  stirlinglem5  46034  stirlinglem7  46036  stirlinglem10  46039  stirlinglem12  46041  stirlinglem14  46043  stirlinglem15  46044  fouriersw  46187  vonioolem2  46637  vonicclem2  46640  iccpartiltu  47347  divgcdoddALTV  47607  fpprwppr  47664  isubgr3stgrlem7  47875  nnsgrpnmnd  48022  eluz2cnn0n1  48357  mod0mul  48369  modn0mul  48370  blennn  48425  nnpw2blen  48430  digvalnn0  48449  nn0digval  48450  dignn0fr  48451  dignn0ldlem  48452  dig0  48456