Theorem nnne0 12202

Description: A positive integer is nonzero. See nnne0ALT 12206 for a shorter proof using ax-pre-mulgt0 11106. This proof avoids 0lt1 11663, and thus ax-pre-mulgt0 11106, by splitting ax-1ne0 11098 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11106. (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 11098	. . 3 ⊢ 1 ≠ 0
2		1re 11135	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11137	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11251	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 231	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5075	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 341	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5075	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 341	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5075	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 341	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5075	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 341	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 22	. . . . . 6 ⊢ (1 < 0 → 1 < 0)
15		simp1 1142	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 12180	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11136	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11165	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11151	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11138	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1144	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11752	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11087	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11325	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1143	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5107	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11298	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1125	. . . . . . 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 12183	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 407	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11706	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5076	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 341	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5076	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 341	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5076	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 341	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5076	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
41	40	imbi2d 341	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
42		id 22	. . . . . 6 ⊢ (0 < 1 → 0 < 1)
43		simp1 1142	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
44	43	nnred 12180	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11136	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
46		simp3 1144	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
47		simp2 1143	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
48	44, 45, 46, 47	addgt0d 11716	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
49	48	3exp 1125	. . . . . . 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 12183	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 407	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11705	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 965	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 697	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 853   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   ≠ wne 2934   class class class wbr 5072  (class class class)co 7356  ℝcr 11028  0cc0 11029  1c1 11030   + caddc 11032   < clt 11170  ℕcn 12165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-nn 12166

This theorem is referenced by:  nnneneg  12203  0nnn  12204  nndivre  12209  nndiv  12214  nndivtr  12215  nnne0d  12218  zdiv  12590  zdivadd  12591  zdivmul  12592  elq  12891  qmulz  12892  qre  12894  qaddcl  12906  qnegcl  12907  qmulcl  12908  qreccl  12910  rpnnen1lem5  12922  nn0ledivnn  13048  fzo1fzo0n0  13661  quoremz  13805  quoremnn0ALT  13807  intfracq  13809  fldiv  13810  fldiv2  13811  modmulnn  13839  modsumfzodifsn  13897  expnnval  14017  expneg  14022  digit2  14189  facdiv  14240  facndiv  14241  bcm1k  14268  bcp1n  14269  bcval5  14271  hashnncl  14319  cshwidxmod  14756  relexpsucnnr  14978  divcnv  15809  harmonic  15815  expcnv  15820  ef0lem  16034  ruclem6  16193  sqrt2irr  16207  dvdsval3  16216  nndivdvds  16221  modmulconst  16248  dvdsdivcl  16276  dvdsflip  16277  divalg2  16365  divalgmod  16366  ndvdssub  16369  nndvdslegcd  16465  divgcdz  16471  divgcdnn  16475  modgcd  16492  gcddiv  16511  gcdzeq  16512  eucalgf  16543  eucalginv  16544  lcmgcdlem  16566  lcmftp  16596  qredeq  16617  qredeu  16618  cncongr1  16627  cncongr2  16628  isprm6  16675  divnumden  16709  divdenle  16710  phimullem  16740  hashgcdlem  16749  phisum  16752  prm23lt5  16776  pythagtriplem10  16782  pythagtriplem8  16785  pythagtriplem9  16786  pccl  16811  pcdiv  16814  pcqcl  16818  pcdvds  16826  pcndvds  16828  pcndvds2  16830  pceq0  16833  pcneg  16836  pcz  16843  pcmpt  16854  fldivp1  16859  pcfac  16861  oddprmdvds  16865  infpnlem2  16873  cshwshashlem1  17057  smndex1n0mnd  18874  mulgnn  19042  mulgnegnn  19051  mulgmodid  19080  oddvdsnn0  19510  odmulgeq  19523  gexnnod  19554  qsssubdrg  21401  prmirredlem  21447  znf1o  21526  znhash  21533  znidomb  21536  znunithash  21539  znrrg  21540  cply1coe0  22287  cply1coe0bi  22288  m2cpm  22724  m2cpminvid2lem  22737  fvmptnn04ifc  22835  vitali  25598  mbfi1fseqlem3  25702  dvexp2  25939  plyeq0lem  26193  abelthlem9  26423  logtayllem  26641  logtayl  26642  logtaylsum  26643  logtayl2  26644  cxpexp  26650  cxproot  26672  root1id  26736  root1eq1  26737  cxpeq  26739  logbgcd1irr  26776  atantayl  26919  atantayl2  26920  leibpilem2  26923  leibpi  26924  birthdaylem2  26934  birthdaylem3  26935  dfef2  26952  emcllem2  26978  emcllem3  26979  zetacvg  26996  lgam1  27045  basellem4  27065  basellem8  27069  basellem9  27070  mumullem2  27161  fsumdvdscom  27166  chtublem  27192  dchrelbas4  27224  bclbnd  27261  lgsval4a  27300  lgsabs1  27317  lgssq2  27319  dchrmusumlema  27474  dchrmusum2  27475  dchrvmasumiflem1  27482  dchrvmaeq0  27485  dchrisum0flblem1  27489  dchrisum0flblem2  27490  dchrisum0re  27494  ostthlem1  27608  ostth1  27614  pthdlem2lem  29853  wspthsnonn0vne  30003  clwwisshclwwslem  30102  ipasslem4  30923  ipasslem5  30924  divnumden2  32908  1fldgenq  33406  qqhval2  34166  qqhnm  34174  signstfveq0  34761  subfacp1lem6  35413  circum  35902  fz0n  35959  divcnvlin  35961  iprodgam  35970  faclim  35974  nndivsub  36685  poimirlem29  38016  poimirlem31  38018  poimirlem32  38019  heiborlem4  38181  heiborlem6  38183  nnproddivdvdsd  42485  pellexlem1  43274  congrep  43418  jm2.20nn  43442  proot1ex  43641  hashnzfzclim  44766  binomcxplemnotnn0  44800  nnne1ge2  45739  mccllem  46042  clim1fr1  46046  dvnxpaek  46385  dvnprodlem2  46390  wallispilem5  46512  wallispi2lem1  46514  stirlinglem1  46517  stirlinglem3  46519  stirlinglem4  46520  stirlinglem5  46521  stirlinglem7  46523  stirlinglem10  46526  stirlinglem12  46528  stirlinglem14  46530  stirlinglem15  46531  fouriersw  46674  vonioolem2  47124  vonicclem2  47127  mod0mul  47825  modn0mul  47826  modlt0b  47832  iccpartiltu  47897  divgcdoddALTV  48173  fpprwppr  48230  isubgr3stgrlem7  48463  gpg3kgrtriexlem5  48578  nnsgrpnmnd  48669  eluz2cnn0n1  49002  blennn  49066  nnpw2blen  49071  digvalnn0  49090  nn0digval  49091  dignn0fr  49092  dignn0ldlem  49093  dig0  49097