Theorem nnne0 12294

Description: A positive integer is nonzero. See nnne0ALT 12298 for a shorter proof using ax-pre-mulgt0 11201. This proof avoids 0lt1 11760, and thus ax-pre-mulgt0 11201, by splitting ax-1ne0 11193 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11201. (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 11193	. . 3 ⊢ 1 ≠ 0
2		1re 11232	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11234	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11348	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 233	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5106	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5106	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5106	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 343	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5106	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 23	. . . . . 6 ⊢ (1 < 0 → 1 < 0)
15		simp1 1154	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 12272	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11233	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11262	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11248	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11235	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1156	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11849	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11182	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11422	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1155	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5140	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11395	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1137	. . . . . . 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 12275	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 412	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11803	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5107	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5107	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5107	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 343	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5107	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
41	40	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
42		id 23	. . . . . 6 ⊢ (0 < 1 → 0 < 1)
43		simp1 1154	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
44	43	nnred 12272	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11233	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
46		simp3 1156	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
47		simp2 1155	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
48	44, 45, 46, 47	addgt0d 11813	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
49	48	3exp 1137	. . . . . . 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 12275	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 412	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11802	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 972	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 704	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2955   class class class wbr 5103  (class class class)co 7413  ℝcr 11123  0cc0 11124  1c1 11125   + caddc 11127   < clt 11267  ℕcn 12257

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-nn 12258

This theorem is used by:  nnneneg  12295  0nnn  12296  nndivre  12301  nndiv  12306  nndivtr  12307  nnne0d  12310  zdiv  12691  zdivadd  12692  zdivmul  12693  elq  12999  qmulz  13000  qre  13002  qaddcl  13015  qnegcl  13016  qmulcl  13017  qreccl  13019  rpnnen1lem5  13031  nn0ledivnn  13157  fzo1fzo0n0  13771  quoremz  13916  quoremnn0ALT  13918  intfracq  13920  fldiv  13921  fldiv2  13922  modmulnn  13950  modsumfzodifsn  14008  expnnval  14128  expneg  14133  digit2  14300  facdiv  14351  facndiv  14352  bcm1k  14379  bcp1n  14380  bcval5  14382  hashnncl  14430  cshwidxmod  14874  relexpsucnnr  15098  divcnv  15942  harmonic  15948  expcnv  15953  ef0lem  16164  ruclem6  16323  sqrt2irr  16337  dvdsval3  16346  nndivdvds  16351  modmulconst  16378  dvdsdivcl  16406  dvdsflip  16407  divalg2  16495  divalgmod  16496  ndvdssub  16499  nndvdslegcd  16595  divgcdz  16601  divgcdnn  16605  modgcd  16622  gcddiv  16641  gcdzeq  16642  eucalgf  16673  eucalginv  16674  lcmgcdlem  16696  lcmftp  16726  qredeq  16747  qredeu  16748  cncongr1  16757  cncongr2  16758  isprm6  16805  divnumden  16839  divdenle  16840  phimullem  16870  hashgcdlem  16879  phisum  16882  prm23lt5  16906  pythagtriplem10  16912  pythagtriplem8  16915  pythagtriplem9  16916  pccl  16941  pcdiv  16944  pcqcl  16948  pcdvds  16956  pcndvds  16958  pcndvds2  16960  pceq0  16963  pcneg  16966  pcz  16973  pcmpt  16984  fldivp1  16989  pcfac  16991  oddprmdvds  16995  infpnlem2  17003  cshwshashlem1  17187  smndex1n0mnd  19024  mulgnn  19198  mulgnegnn  19207  mulgmodid  19236  oddvdsnn0  19671  odmulgeq  19684  gexnnod  19715  qsssubdrg  21639  prmirredlem  21685  znf1o  21764  znhash  21771  znidomb  21774  znunithash  21777  znrrg  21778  cply1coe0  22526  cply1coe0bi  22527  m2cpm  22966  m2cpminvid2lem  22979  fvmptnn04ifc  23077  vitali  25841  mbfi1fseqlem3  25945  dvexp2  26181  plyeq0lem  26436  abelthlem9  26676  logtayllem  26896  logtayl  26897  logtaylsum  26898  logtayl2  26899  cxpexp  26905  cxproot  26927  root1id  26991  root1eq1  26992  cxpeq  26994  logbgcd1irr  27031  atantayl  27174  atantayl2  27175  leibpilem2  27178  leibpi  27179  birthdaylem2  27189  birthdaylem3  27190  dfef2  27207  emcllem2  27233  emcllem3  27234  zetacvg  27251  lgam1  27300  basellem4  27320  basellem8  27324  basellem9  27325  mumullem2  27416  fsumdvdscom  27421  chtublem  27447  dchrelbas4  27479  bclbnd  27516  lgsval4a  27555  lgsabs1  27572  lgssq2  27574  dchrmusumlema  27729  dchrmusum2  27730  dchrvmasumiflem1  27737  dchrvmaeq0  27740  dchrisum0flblem1  27744  dchrisum0flblem2  27745  dchrisum0re  27749  ostthlem1  27863  ostth1  27869  pthdlem2lem  30232  wspthsnonn0vne  30385  clwwisshclwwslem  30484  ipasslem4  31315  ipasslem5  31316  divnumden2  33286  1fldgenq  33763  qqhval2  34492  qqhnm  34500  signstfveq0  35085  subfacp1lem6  35764  circum  36253  fz0n  36310  divcnvlin  36312  iprodgam  36321  faclim  36325  nndivsub  37076  poimirlem29  38398  poimirlem31  38400  poimirlem32  38401  heiborlem4  38564  heiborlem6  38566  nnproddivdvdsd  42866  pellexlem1  43670  congrep  43814  jm2.20nn  43838  proot1ex  44037  hashnzfzclim  45146  binomcxplemnotnn0  45180  nnne1ge2  46124  mccllem  46427  clim1fr1  46431  dvnxpaek  46770  dvnprodlem2  46775  wallispilem5  46897  wallispi2lem1  46899  stirlinglem1  46902  stirlinglem3  46904  stirlinglem4  46905  stirlinglem5  46906  stirlinglem7  46908  stirlinglem10  46911  stirlinglem12  46913  stirlinglem14  46915  stirlinglem15  46916  fouriersw  47059  vonioolem2  47509  vonicclem2  47512  sqrtnnaa  47731  mod0mul  48250  modn0mul  48251  modlt0b  48257  iccpartiltu  48322  divgcdoddALTV  48598  fpprwppr  48655  isubgr3stgrlem7  48888  gpg3kgrtriexlem5  49003  nnsgrpnmnd  49093  eluz2cnn0n1  49441  blennn  49505  nnpw2blen  49510  digvalnn0  49529  nn0digval  49530  dignn0fr  49531  dignn0ldlem  49532  dig0  49536