Theorem nnne0 12179

Description: A positive integer is nonzero. See nnne0ALT 12183 for a shorter proof using ax-pre-mulgt0 11103. This proof avoids 0lt1 11659, and thus ax-pre-mulgt0 11103, by splitting ax-1ne0 11095 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11103. (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 11095	. . 3 ⊢ 1 ≠ 0
2		1re 11132	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11134	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11247	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 230	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5101	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5101	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5101	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5101	. . . . . . 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 12160	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11133	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11161	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11147	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11135	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11748	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11084	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11321	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5133	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11294	. . . . . . . 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 12163	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11702	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5102	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5102	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5102	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5102	. . . . . . 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 12160	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11133	. . . . . . . . 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 11712	. . . . . . . 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 12163	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11701	. . 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 2113   ≠ wne 2932   class class class wbr 5098  (class class class)co 7358  ℝcr 11025  0cc0 11026  1c1 11027   + caddc 11029   < clt 11166  ℕcn 12145

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-nn 12146

This theorem is referenced by:  nnneneg  12180  0nnn  12181  nndivre  12186  nndiv  12191  nndivtr  12192  nnne0d  12195  zdiv  12562  zdivadd  12563  zdivmul  12564  elq  12863  qmulz  12864  qre  12866  qaddcl  12878  qnegcl  12879  qmulcl  12880  qreccl  12882  rpnnen1lem5  12894  nn0ledivnn  13020  fzo1fzo0n0  13631  quoremz  13775  quoremnn0ALT  13777  intfracq  13779  fldiv  13780  fldiv2  13781  modmulnn  13809  modsumfzodifsn  13867  expnnval  13987  expneg  13992  digit2  14159  facdiv  14210  facndiv  14211  bcm1k  14238  bcp1n  14239  bcval5  14241  hashnncl  14289  cshwidxmod  14726  relexpsucnnr  14948  divcnv  15776  harmonic  15782  expcnv  15787  ef0lem  16001  ruclem6  16160  sqrt2irr  16174  dvdsval3  16183  nndivdvds  16188  modmulconst  16215  dvdsdivcl  16243  dvdsflip  16244  divalg2  16332  divalgmod  16333  ndvdssub  16336  nndvdslegcd  16432  divgcdz  16438  divgcdnn  16442  modgcd  16459  gcddiv  16478  gcdzeq  16479  eucalgf  16510  eucalginv  16511  lcmgcdlem  16533  lcmftp  16563  qredeq  16584  qredeu  16585  cncongr1  16594  cncongr2  16595  isprm6  16641  divnumden  16675  divdenle  16676  phimullem  16706  hashgcdlem  16715  phisum  16718  prm23lt5  16742  pythagtriplem10  16748  pythagtriplem8  16751  pythagtriplem9  16752  pccl  16777  pcdiv  16780  pcqcl  16784  pcdvds  16792  pcndvds  16794  pcndvds2  16796  pceq0  16799  pcneg  16802  pcz  16809  pcmpt  16820  fldivp1  16825  pcfac  16827  oddprmdvds  16831  infpnlem2  16839  cshwshashlem1  17023  smndex1n0mnd  18837  mulgnn  19005  mulgnegnn  19014  mulgmodid  19043  oddvdsnn0  19473  odmulgeq  19486  gexnnod  19517  qsssubdrg  21381  prmirredlem  21427  znf1o  21506  znhash  21513  znidomb  21516  znunithash  21519  znrrg  21520  cply1coe0  22245  cply1coe0bi  22246  m2cpm  22685  m2cpminvid2lem  22698  fvmptnn04ifc  22796  vitali  25570  mbfi1fseqlem3  25674  dvexp2  25914  plyeq0lem  26171  abelthlem9  26406  logtayllem  26624  logtayl  26625  logtaylsum  26626  logtayl2  26627  cxpexp  26633  cxproot  26655  root1id  26720  root1eq1  26721  cxpeq  26723  logbgcd1irr  26760  atantayl  26903  atantayl2  26904  leibpilem2  26907  leibpi  26908  birthdaylem2  26918  birthdaylem3  26919  dfef2  26937  emcllem2  26963  emcllem3  26964  zetacvg  26981  lgam1  27030  basellem4  27050  basellem8  27054  basellem9  27055  mumullem2  27146  fsumdvdscom  27151  chtublem  27178  dchrelbas4  27210  bclbnd  27247  lgsval4a  27286  lgsabs1  27303  lgssq2  27305  dchrmusumlema  27460  dchrmusum2  27461  dchrvmasumiflem1  27468  dchrvmaeq0  27471  dchrisum0flblem1  27475  dchrisum0flblem2  27476  dchrisum0re  27480  ostthlem1  27594  ostth1  27600  pthdlem2lem  29840  wspthsnonn0vne  29990  clwwisshclwwslem  30089  ipasslem4  30909  ipasslem5  30910  divnumden2  32896  1fldgenq  33404  qqhval2  34139  qqhnm  34147  signstfveq0  34734  subfacp1lem6  35379  circum  35868  fz0n  35925  divcnvlin  35927  iprodgam  35936  faclim  35940  nndivsub  36651  poimirlem29  37850  poimirlem31  37852  poimirlem32  37853  heiborlem4  38015  heiborlem6  38017  nnproddivdvdsd  42254  pellexlem1  43071  congrep  43215  jm2.20nn  43239  proot1ex  43438  hashnzfzclim  44563  binomcxplemnotnn0  44597  nnne1ge2  45539  mccllem  45843  clim1fr1  45847  dvnxpaek  46186  dvnprodlem2  46191  wallispilem5  46313  wallispi2lem1  46315  stirlinglem1  46318  stirlinglem3  46320  stirlinglem4  46321  stirlinglem5  46322  stirlinglem7  46324  stirlinglem10  46327  stirlinglem12  46329  stirlinglem14  46331  stirlinglem15  46332  fouriersw  46475  vonioolem2  46925  vonicclem2  46928  mod0mul  47602  modn0mul  47603  modlt0b  47609  iccpartiltu  47668  divgcdoddALTV  47928  fpprwppr  47985  isubgr3stgrlem7  48218  gpg3kgrtriexlem5  48333  nnsgrpnmnd  48424  eluz2cnn0n1  48757  blennn  48821  nnpw2blen  48826  digvalnn0  48845  nn0digval  48846  dignn0fr  48847  dignn0ldlem  48848  dig0  48852