Theorem nnne0 12187

Description: A positive integer is nonzero. See nnne0ALT 12191 for a shorter proof using ax-pre-mulgt0 11128. This proof avoids 0lt1 11677, and thus ax-pre-mulgt0 11128, by splitting ax-1ne0 11120 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11128. (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 11120	. . 3 ⊢ 1 ≠ 0
2		1re 11155	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11157	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11269	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 229	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5108	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5108	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5108	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5108	. . . . . . 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 12168	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11156	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11184	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11170	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11158	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11766	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11109	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addid2i 11343	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1137	. . . . . . . . . 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 11316	. . . . . . . 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 12171	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 407	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11720	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5109	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5109	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5109	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5109	. . . . . . 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 12168	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11156	. . . . . . . . 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 11730	. . . . . . . 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 12171	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 407	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11719	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 956	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 689	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943   class class class wbr 5105  (class class class)co 7357  ℝcr 11050  0cc0 11051  1c1 11052   + caddc 11054   < clt 11189  ℕcn 12153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-nn 12154

This theorem is referenced by:  nnneneg  12188  0nnn  12189  nndivre  12194  nndiv  12199  nndivtr  12200  nnne0d  12203  zdiv  12573  zdivadd  12574  zdivmul  12575  elq  12875  qmulz  12876  qre  12878  qaddcl  12890  qnegcl  12891  qmulcl  12892  qreccl  12894  rpnnen1lem5  12906  nn0ledivnn  13028  fzo1fzo0n0  13623  quoremz  13760  quoremnn0ALT  13762  intfracq  13764  fldiv  13765  fldiv2  13766  modmulnn  13794  modsumfzodifsn  13849  expnnval  13970  expneg  13975  digit2  14139  facdiv  14187  facndiv  14188  bcm1k  14215  bcp1n  14216  bcval5  14218  hashnncl  14266  cshwidxmod  14691  relexpsucnnr  14910  divcnv  15738  harmonic  15744  expcnv  15749  ef0lem  15961  ruclem6  16117  sqrt2irr  16131  dvdsval3  16140  nndivdvds  16145  modmulconst  16170  dvdsdivcl  16198  dvdsflip  16199  divalg2  16287  divalgmod  16288  ndvdssub  16291  nndvdslegcd  16385  divgcdz  16391  divgcdnn  16395  modgcd  16413  gcddiv  16432  gcdzeq  16433  eucalgf  16459  eucalginv  16460  lcmgcdlem  16482  lcmftp  16512  qredeq  16533  qredeu  16534  cncongr1  16543  cncongr2  16544  isprm6  16590  divnumden  16623  divdenle  16624  phimullem  16651  hashgcdlem  16660  phisum  16662  prm23lt5  16686  pythagtriplem10  16692  pythagtriplem8  16695  pythagtriplem9  16696  pccl  16721  pcdiv  16724  pcqcl  16728  pcdvds  16736  pcndvds  16738  pcndvds2  16740  pceq0  16743  pcneg  16746  pcz  16753  pcmpt  16764  fldivp1  16769  pcfac  16771  oddprmdvds  16775  infpnlem2  16783  cshwshashlem1  16968  smndex1n0mnd  18722  mulgnn  18880  mulgnegnn  18886  mulgmodid  18915  oddvdsnn0  19326  odmulgeq  19339  gexnnod  19370  qsssubdrg  20856  prmirredlem  20893  znf1o  20958  znhash  20965  znidomb  20968  znunithash  20971  znrrg  20972  cply1coe0  21670  cply1coe0bi  21671  m2cpm  22090  m2cpminvid2lem  22103  fvmptnn04ifc  22201  vitali  24977  mbfi1fseqlem3  25082  dvexp2  25318  plyeq0lem  25571  abelthlem9  25799  logtayllem  26014  logtayl  26015  logtaylsum  26016  logtayl2  26017  cxpexp  26023  cxproot  26045  root1id  26107  root1eq1  26108  cxpeq  26110  logbgcd1irr  26144  atantayl  26287  atantayl2  26288  leibpilem2  26291  leibpi  26292  birthdaylem2  26302  birthdaylem3  26303  dfef2  26320  emcllem2  26346  emcllem3  26347  zetacvg  26364  lgam1  26413  basellem4  26433  basellem8  26437  basellem9  26438  mumullem2  26529  fsumdvdscom  26534  chtublem  26559  dchrelbas4  26591  bclbnd  26628  lgsval4a  26667  lgsabs1  26684  lgssq2  26686  dchrmusumlema  26841  dchrmusum2  26842  dchrvmasumiflem1  26849  dchrvmaeq0  26852  dchrisum0flblem1  26856  dchrisum0flblem2  26857  dchrisum0re  26861  ostthlem1  26975  ostth1  26981  pthdlem2lem  28715  wspthsnonn0vne  28862  clwwisshclwwslem  28958  ipasslem4  29776  ipasslem5  29777  divnumden2  31714  1fldgenq  32089  qqhval2  32563  qqhnm  32571  signstfveq0  33189  subfacp1lem6  33779  circum  34262  fz0n  34303  divcnvlin  34305  iprodgam  34315  faclim  34319  nndivsub  34929  poimirlem29  36107  poimirlem31  36109  poimirlem32  36110  heiborlem4  36273  heiborlem6  36275  nnproddivdvdsd  40458  pellexlem1  41138  congrep  41283  jm2.20nn  41307  proot1ex  41514  hashnzfzclim  42592  binomcxplemnotnn0  42626  nnne1ge2  43515  mccllem  43828  clim1fr1  43832  dvnxpaek  44173  dvnprodlem2  44178  wallispilem5  44300  wallispi2lem1  44302  stirlinglem1  44305  stirlinglem3  44307  stirlinglem4  44308  stirlinglem5  44309  stirlinglem7  44311  stirlinglem10  44314  stirlinglem12  44316  stirlinglem14  44318  stirlinglem15  44319  fouriersw  44462  vonioolem2  44912  vonicclem2  44915  iccpartiltu  45604  divgcdoddALTV  45864  fpprwppr  45921  nnsgrpnmnd  46102  eluz2cnn0n1  46582  mod0mul  46595  modn0mul  46596  blennn  46651  nnpw2blen  46656  digvalnn0  46675  nn0digval  46676  dignn0fr  46677  dignn0ldlem  46678  dig0  46682