Theorem nnne0 12196

Description: A positive integer is nonzero. See nnne0ALT 12200 for a shorter proof using ax-pre-mulgt0 11121. This proof avoids 0lt1 11676, and thus ax-pre-mulgt0 11121, by splitting ax-1ne0 11113 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11121. (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 11113	. . 3 ⊢ 1 ≠ 0
2		1re 11150	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11152	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11264	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 230	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5105	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5105	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5105	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5105	. . . . . . 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 12177	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11151	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11179	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11165	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11153	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11765	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11102	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11338	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5137	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11311	. . . . . . . 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 12180	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11719	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5106	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5106	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5106	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5106	. . . . . . 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 12177	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11151	. . . . . . . . 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 11729	. . . . . . . 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 12180	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11718	. . 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 1540   ∈ wcel 2109   ≠ wne 2925   class class class wbr 5102  (class class class)co 7369  ℝcr 11043  0cc0 11044  1c1 11045   + caddc 11047   < clt 11184  ℕcn 12162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-nn 12163

This theorem is referenced by:  nnneneg  12197  0nnn  12198  nndivre  12203  nndiv  12208  nndivtr  12209  nnne0d  12212  zdiv  12580  zdivadd  12581  zdivmul  12582  elq  12885  qmulz  12886  qre  12888  qaddcl  12900  qnegcl  12901  qmulcl  12902  qreccl  12904  rpnnen1lem5  12916  nn0ledivnn  13042  fzo1fzo0n0  13652  quoremz  13793  quoremnn0ALT  13795  intfracq  13797  fldiv  13798  fldiv2  13799  modmulnn  13827  modsumfzodifsn  13885  expnnval  14005  expneg  14010  digit2  14177  facdiv  14228  facndiv  14229  bcm1k  14256  bcp1n  14257  bcval5  14259  hashnncl  14307  cshwidxmod  14744  relexpsucnnr  14967  divcnv  15795  harmonic  15801  expcnv  15806  ef0lem  16020  ruclem6  16179  sqrt2irr  16193  dvdsval3  16202  nndivdvds  16207  modmulconst  16234  dvdsdivcl  16262  dvdsflip  16263  divalg2  16351  divalgmod  16352  ndvdssub  16355  nndvdslegcd  16451  divgcdz  16457  divgcdnn  16461  modgcd  16478  gcddiv  16497  gcdzeq  16498  eucalgf  16529  eucalginv  16530  lcmgcdlem  16552  lcmftp  16582  qredeq  16603  qredeu  16604  cncongr1  16613  cncongr2  16614  isprm6  16660  divnumden  16694  divdenle  16695  phimullem  16725  hashgcdlem  16734  phisum  16737  prm23lt5  16761  pythagtriplem10  16767  pythagtriplem8  16770  pythagtriplem9  16771  pccl  16796  pcdiv  16799  pcqcl  16803  pcdvds  16811  pcndvds  16813  pcndvds2  16815  pceq0  16818  pcneg  16821  pcz  16828  pcmpt  16839  fldivp1  16844  pcfac  16846  oddprmdvds  16850  infpnlem2  16858  cshwshashlem1  17042  smndex1n0mnd  18815  mulgnn  18983  mulgnegnn  18992  mulgmodid  19021  oddvdsnn0  19450  odmulgeq  19463  gexnnod  19494  qsssubdrg  21319  prmirredlem  21358  znf1o  21437  znhash  21444  znidomb  21447  znunithash  21450  znrrg  21451  cply1coe0  22164  cply1coe0bi  22165  m2cpm  22604  m2cpminvid2lem  22617  fvmptnn04ifc  22715  vitali  25490  mbfi1fseqlem3  25594  dvexp2  25834  plyeq0lem  26091  abelthlem9  26326  logtayllem  26544  logtayl  26545  logtaylsum  26546  logtayl2  26547  cxpexp  26553  cxproot  26575  root1id  26640  root1eq1  26641  cxpeq  26643  logbgcd1irr  26680  atantayl  26823  atantayl2  26824  leibpilem2  26827  leibpi  26828  birthdaylem2  26838  birthdaylem3  26839  dfef2  26857  emcllem2  26883  emcllem3  26884  zetacvg  26901  lgam1  26950  basellem4  26970  basellem8  26974  basellem9  26975  mumullem2  27066  fsumdvdscom  27071  chtublem  27098  dchrelbas4  27130  bclbnd  27167  lgsval4a  27206  lgsabs1  27223  lgssq2  27225  dchrmusumlema  27380  dchrmusum2  27381  dchrvmasumiflem1  27388  dchrvmaeq0  27391  dchrisum0flblem1  27395  dchrisum0flblem2  27396  dchrisum0re  27400  ostthlem1  27514  ostth1  27520  pthdlem2lem  29670  wspthsnonn0vne  29820  clwwisshclwwslem  29916  ipasslem4  30736  ipasslem5  30737  divnumden2  32713  1fldgenq  33245  qqhval2  33945  qqhnm  33953  signstfveq0  34541  subfacp1lem6  35145  circum  35634  fz0n  35691  divcnvlin  35693  iprodgam  35702  faclim  35706  nndivsub  36418  poimirlem29  37616  poimirlem31  37618  poimirlem32  37619  heiborlem4  37781  heiborlem6  37783  nnproddivdvdsd  41961  pellexlem1  42790  congrep  42935  jm2.20nn  42959  proot1ex  43158  hashnzfzclim  44284  binomcxplemnotnn0  44318  nnne1ge2  45262  mccllem  45568  clim1fr1  45572  dvnxpaek  45913  dvnprodlem2  45918  wallispilem5  46040  wallispi2lem1  46042  stirlinglem1  46045  stirlinglem3  46047  stirlinglem4  46048  stirlinglem5  46049  stirlinglem7  46051  stirlinglem10  46054  stirlinglem12  46056  stirlinglem14  46058  stirlinglem15  46059  fouriersw  46202  vonioolem2  46652  vonicclem2  46655  mod0mul  47330  modn0mul  47331  modlt0b  47337  iccpartiltu  47396  divgcdoddALTV  47656  fpprwppr  47713  isubgr3stgrlem7  47944  gpg3kgrtriexlem5  48051  nnsgrpnmnd  48139  eluz2cnn0n1  48473  blennn  48537  nnpw2blen  48542  digvalnn0  48561  nn0digval  48562  dignn0fr  48563  dignn0ldlem  48564  dig0  48568