Theorem nnne0 12285

Description: A positive integer is nonzero. See nnne0ALT 12289 for a shorter proof using ax-pre-mulgt0 11192. This proof avoids 0lt1 11751, and thus ax-pre-mulgt0 11192, by splitting ax-1ne0 11184 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11192. (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 11184	. . 3 ⊢ 1 ≠ 0
2		1re 11223	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11225	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11339	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 233	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5114	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5114	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5114	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 343	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5114	. . . . . . 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 12263	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11224	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11253	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11239	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11226	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1156	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11840	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11173	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11413	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1155	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5148	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11386	. . . . . . . 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 12266	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 412	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11794	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5115	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5115	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5115	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 343	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5115	. . . . . . 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 12263	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11224	. . . . . . . . 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 11804	. . . . . . . 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 12266	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 412	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11793	. . 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 2146   ≠ wne 2960   class class class wbr 5111  (class class class)co 7419  ℝcr 11114  0cc0 11115  1c1 11116   + caddc 11118   < clt 11258  ℕcn 12248

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-nn 12249

This theorem is used by:  nnneneg  12286  0nnn  12287  nndivre  12292  nndiv  12297  nndivtr  12298  nnne0d  12301  zdiv  12682  zdivadd  12683  zdivmul  12684  elq  12990  qmulz  12991  qre  12993  qaddcl  13005  qnegcl  13006  qmulcl  13007  qreccl  13009  rpnnen1lem5  13021  nn0ledivnn  13147  fzo1fzo0n0  13761  quoremz  13906  quoremnn0ALT  13908  intfracq  13910  fldiv  13911  fldiv2  13912  modmulnn  13940  modsumfzodifsn  13998  expnnval  14118  expneg  14123  digit2  14290  facdiv  14341  facndiv  14342  bcm1k  14369  bcp1n  14370  bcval5  14372  hashnncl  14420  cshwidxmod  14864  relexpsucnnr  15086  divcnv  15930  harmonic  15936  expcnv  15941  ef0lem  16154  ruclem6  16313  sqrt2irr  16327  dvdsval3  16336  nndivdvds  16341  modmulconst  16368  dvdsdivcl  16396  dvdsflip  16397  divalg2  16485  divalgmod  16486  ndvdssub  16489  nndvdslegcd  16585  divgcdz  16591  divgcdnn  16595  modgcd  16612  gcddiv  16631  gcdzeq  16632  eucalgf  16663  eucalginv  16664  lcmgcdlem  16686  lcmftp  16716  qredeq  16737  qredeu  16738  cncongr1  16747  cncongr2  16748  isprm6  16795  divnumden  16829  divdenle  16830  phimullem  16860  hashgcdlem  16869  phisum  16872  prm23lt5  16896  pythagtriplem10  16902  pythagtriplem8  16905  pythagtriplem9  16906  pccl  16931  pcdiv  16934  pcqcl  16938  pcdvds  16946  pcndvds  16948  pcndvds2  16950  pceq0  16953  pcneg  16956  pcz  16963  pcmpt  16974  fldivp1  16979  pcfac  16981  oddprmdvds  16985  infpnlem2  16993  cshwshashlem1  17177  smndex1n0mnd  19011  mulgnn  19185  mulgnegnn  19194  mulgmodid  19223  oddvdsnn0  19658  odmulgeq  19671  gexnnod  19702  qsssubdrg  21626  prmirredlem  21672  znf1o  21751  znhash  21758  znidomb  21761  znunithash  21764  znrrg  21765  cply1coe0  22511  cply1coe0bi  22512  m2cpm  22948  m2cpminvid2lem  22961  fvmptnn04ifc  23059  vitali  25823  mbfi1fseqlem3  25927  dvexp2  26164  plyeq0lem  26418  abelthlem9  26654  logtayllem  26875  logtayl  26876  logtaylsum  26877  logtayl2  26878  cxpexp  26884  cxproot  26906  root1id  26970  root1eq1  26971  cxpeq  26973  logbgcd1irr  27010  atantayl  27153  atantayl2  27154  leibpilem2  27157  leibpi  27158  birthdaylem2  27168  birthdaylem3  27169  dfef2  27186  emcllem2  27212  emcllem3  27213  zetacvg  27230  lgam1  27279  basellem4  27299  basellem8  27303  basellem9  27304  mumullem2  27395  fsumdvdscom  27400  chtublem  27426  dchrelbas4  27458  bclbnd  27495  lgsval4a  27534  lgsabs1  27551  lgssq2  27553  dchrmusumlema  27708  dchrmusum2  27709  dchrvmasumiflem1  27716  dchrvmaeq0  27719  dchrisum0flblem1  27723  dchrisum0flblem2  27724  dchrisum0re  27728  ostthlem1  27842  ostth1  27848  pthdlem2lem  30180  wspthsnonn0vne  30333  clwwisshclwwslem  30432  ipasslem4  31257  ipasslem5  31258  divnumden2  33230  1fldgenq  33707  qqhval2  34436  qqhnm  34444  signstfveq0  35029  subfacp1lem6  35714  circum  36203  fz0n  36260  divcnvlin  36262  iprodgam  36271  faclim  36275  nndivsub  37025  poimirlem29  38357  poimirlem31  38359  poimirlem32  38360  heiborlem4  38523  heiborlem6  38525  nnproddivdvdsd  42825  pellexlem1  43614  congrep  43758  jm2.20nn  43782  proot1ex  43981  hashnzfzclim  45090  binomcxplemnotnn0  45124  nnne1ge2  46068  mccllem  46371  clim1fr1  46375  dvnxpaek  46714  dvnprodlem2  46719  wallispilem5  46841  wallispi2lem1  46843  stirlinglem1  46846  stirlinglem3  46848  stirlinglem4  46849  stirlinglem5  46850  stirlinglem7  46852  stirlinglem10  46855  stirlinglem12  46857  stirlinglem14  46859  stirlinglem15  46860  fouriersw  47003  vonioolem2  47453  vonicclem2  47456  sqrtnnaa  47662  mod0mul  48157  modn0mul  48158  modlt0b  48164  iccpartiltu  48229  divgcdoddALTV  48505  fpprwppr  48562  isubgr3stgrlem7  48795  gpg3kgrtriexlem5  48910  nnsgrpnmnd  49000  eluz2cnn0n1  49348  blennn  49412  nnpw2blen  49417  digvalnn0  49436  nn0digval  49437  dignn0fr  49438  dignn0ldlem  49439  dig0  49443