Theorem nnne0 12154

Description: A positive integer is nonzero. See nnne0ALT 12158 for a shorter proof using ax-pre-mulgt0 11078. This proof avoids 0lt1 11634, and thus ax-pre-mulgt0 11078, by splitting ax-1ne0 11070 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11078. (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 11070	. . 3 ⊢ 1 ≠ 0
2		1re 11107	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11109	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11222	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 230	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5089	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5089	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5089	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5089	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 22	. . . . . 6 ⊢ (1 < 0 → 1 < 0)
15		simp1 1136	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 12135	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11108	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11136	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11122	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11110	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11723	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11059	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11296	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5121	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11269	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1119	. . . . . . 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 12138	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11677	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5090	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5090	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5090	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5090	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
41	40	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
42		id 22	. . . . . 6 ⊢ (0 < 1 → 0 < 1)
43		simp1 1136	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
44	43	nnred 12135	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11108	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
46		simp3 1138	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
47		simp2 1137	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
48	44, 45, 46, 47	addgt0d 11687	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
49	48	3exp 1119	. . . . . . 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 12138	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11676	. . 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 1541   ∈ wcel 2111   ≠ wne 2928   class class class wbr 5086  (class class class)co 7341  ℝcr 11000  0cc0 11001  1c1 11002   + caddc 11004   < clt 11141  ℕcn 12120

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-nn 12121

This theorem is referenced by:  nnneneg  12155  0nnn  12156  nndivre  12161  nndiv  12166  nndivtr  12167  nnne0d  12170  zdiv  12538  zdivadd  12539  zdivmul  12540  elq  12843  qmulz  12844  qre  12846  qaddcl  12858  qnegcl  12859  qmulcl  12860  qreccl  12862  rpnnen1lem5  12874  nn0ledivnn  13000  fzo1fzo0n0  13610  quoremz  13754  quoremnn0ALT  13756  intfracq  13758  fldiv  13759  fldiv2  13760  modmulnn  13788  modsumfzodifsn  13846  expnnval  13966  expneg  13971  digit2  14138  facdiv  14189  facndiv  14190  bcm1k  14217  bcp1n  14218  bcval5  14220  hashnncl  14268  cshwidxmod  14705  relexpsucnnr  14927  divcnv  15755  harmonic  15761  expcnv  15766  ef0lem  15980  ruclem6  16139  sqrt2irr  16153  dvdsval3  16162  nndivdvds  16167  modmulconst  16194  dvdsdivcl  16222  dvdsflip  16223  divalg2  16311  divalgmod  16312  ndvdssub  16315  nndvdslegcd  16411  divgcdz  16417  divgcdnn  16421  modgcd  16438  gcddiv  16457  gcdzeq  16458  eucalgf  16489  eucalginv  16490  lcmgcdlem  16512  lcmftp  16542  qredeq  16563  qredeu  16564  cncongr1  16573  cncongr2  16574  isprm6  16620  divnumden  16654  divdenle  16655  phimullem  16685  hashgcdlem  16694  phisum  16697  prm23lt5  16721  pythagtriplem10  16727  pythagtriplem8  16730  pythagtriplem9  16731  pccl  16756  pcdiv  16759  pcqcl  16763  pcdvds  16771  pcndvds  16773  pcndvds2  16775  pceq0  16778  pcneg  16781  pcz  16788  pcmpt  16799  fldivp1  16804  pcfac  16806  oddprmdvds  16810  infpnlem2  16818  cshwshashlem1  17002  smndex1n0mnd  18815  mulgnn  18983  mulgnegnn  18992  mulgmodid  19021  oddvdsnn0  19451  odmulgeq  19464  gexnnod  19495  qsssubdrg  21358  prmirredlem  21404  znf1o  21483  znhash  21490  znidomb  21493  znunithash  21496  znrrg  21497  cply1coe0  22211  cply1coe0bi  22212  m2cpm  22651  m2cpminvid2lem  22664  fvmptnn04ifc  22762  vitali  25536  mbfi1fseqlem3  25640  dvexp2  25880  plyeq0lem  26137  abelthlem9  26372  logtayllem  26590  logtayl  26591  logtaylsum  26592  logtayl2  26593  cxpexp  26599  cxproot  26621  root1id  26686  root1eq1  26687  cxpeq  26689  logbgcd1irr  26726  atantayl  26869  atantayl2  26870  leibpilem2  26873  leibpi  26874  birthdaylem2  26884  birthdaylem3  26885  dfef2  26903  emcllem2  26929  emcllem3  26930  zetacvg  26947  lgam1  26996  basellem4  27016  basellem8  27020  basellem9  27021  mumullem2  27112  fsumdvdscom  27117  chtublem  27144  dchrelbas4  27176  bclbnd  27213  lgsval4a  27252  lgsabs1  27269  lgssq2  27271  dchrmusumlema  27426  dchrmusum2  27427  dchrvmasumiflem1  27434  dchrvmaeq0  27437  dchrisum0flblem1  27441  dchrisum0flblem2  27442  dchrisum0re  27446  ostthlem1  27560  ostth1  27566  pthdlem2lem  29740  wspthsnonn0vne  29890  clwwisshclwwslem  29986  ipasslem4  30806  ipasslem5  30807  divnumden2  32790  1fldgenq  33280  qqhval2  33987  qqhnm  33995  signstfveq0  34582  subfacp1lem6  35221  circum  35710  fz0n  35767  divcnvlin  35769  iprodgam  35778  faclim  35782  nndivsub  36491  poimirlem29  37689  poimirlem31  37691  poimirlem32  37692  heiborlem4  37854  heiborlem6  37856  nnproddivdvdsd  42033  pellexlem1  42862  congrep  43006  jm2.20nn  43030  proot1ex  43229  hashnzfzclim  44355  binomcxplemnotnn0  44389  nnne1ge2  45332  mccllem  45637  clim1fr1  45641  dvnxpaek  45980  dvnprodlem2  45985  wallispilem5  46107  wallispi2lem1  46109  stirlinglem1  46112  stirlinglem3  46114  stirlinglem4  46115  stirlinglem5  46116  stirlinglem7  46118  stirlinglem10  46121  stirlinglem12  46123  stirlinglem14  46125  stirlinglem15  46126  fouriersw  46269  vonioolem2  46719  vonicclem2  46722  mod0mul  47387  modn0mul  47388  modlt0b  47394  iccpartiltu  47453  divgcdoddALTV  47713  fpprwppr  47770  isubgr3stgrlem7  48003  gpg3kgrtriexlem5  48118  nnsgrpnmnd  48209  eluz2cnn0n1  48543  blennn  48607  nnpw2blen  48612  digvalnn0  48631  nn0digval  48632  dignn0fr  48633  dignn0ldlem  48634  dig0  48638