Theorem nnne0 12242

Description: A positive integer is nonzero. See nnne0ALT 12246 for a shorter proof using ax-pre-mulgt0 11183. This proof avoids 0lt1 11732, and thus ax-pre-mulgt0 11183, by splitting ax-1ne0 11175 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11183. (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 11175	. . 3 ⊢ 1 ≠ 0
2		1re 11210	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11212	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11324	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 229	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5150	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5150	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5150	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5150	. . . . . . 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 12223	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11211	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11239	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11225	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11213	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11821	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11164	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11398	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5182	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11371	. . . . . . . 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 12226	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 407	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11775	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5151	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5151	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5151	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5151	. . . . . . 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 12223	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11211	. . . . . . . . 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 11785	. . . . . . . 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 12226	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 407	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11774	. . 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 2940   class class class wbr 5147  (class class class)co 7405  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   < clt 11244  ℕcn 12208

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 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-nn 12209

This theorem is referenced by:  nnneneg  12243  0nnn  12244  nndivre  12249  nndiv  12254  nndivtr  12255  nnne0d  12258  zdiv  12628  zdivadd  12629  zdivmul  12630  elq  12930  qmulz  12931  qre  12933  qaddcl  12945  qnegcl  12946  qmulcl  12947  qreccl  12949  rpnnen1lem5  12961  nn0ledivnn  13083  fzo1fzo0n0  13679  quoremz  13816  quoremnn0ALT  13818  intfracq  13820  fldiv  13821  fldiv2  13822  modmulnn  13850  modsumfzodifsn  13905  expnnval  14026  expneg  14031  digit2  14195  facdiv  14243  facndiv  14244  bcm1k  14271  bcp1n  14272  bcval5  14274  hashnncl  14322  cshwidxmod  14749  relexpsucnnr  14968  divcnv  15795  harmonic  15801  expcnv  15806  ef0lem  16018  ruclem6  16174  sqrt2irr  16188  dvdsval3  16197  nndivdvds  16202  modmulconst  16227  dvdsdivcl  16255  dvdsflip  16256  divalg2  16344  divalgmod  16345  ndvdssub  16348  nndvdslegcd  16442  divgcdz  16448  divgcdnn  16452  modgcd  16470  gcddiv  16489  gcdzeq  16490  eucalgf  16516  eucalginv  16517  lcmgcdlem  16539  lcmftp  16569  qredeq  16590  qredeu  16591  cncongr1  16600  cncongr2  16601  isprm6  16647  divnumden  16680  divdenle  16681  phimullem  16708  hashgcdlem  16717  phisum  16719  prm23lt5  16743  pythagtriplem10  16749  pythagtriplem8  16752  pythagtriplem9  16753  pccl  16778  pcdiv  16781  pcqcl  16785  pcdvds  16793  pcndvds  16795  pcndvds2  16797  pceq0  16800  pcneg  16803  pcz  16810  pcmpt  16821  fldivp1  16826  pcfac  16828  oddprmdvds  16832  infpnlem2  16840  cshwshashlem1  17025  smndex1n0mnd  18789  mulgnn  18952  mulgnegnn  18958  mulgmodid  18987  oddvdsnn0  19406  odmulgeq  19419  gexnnod  19450  qsssubdrg  20996  prmirredlem  21033  znf1o  21098  znhash  21105  znidomb  21108  znunithash  21111  znrrg  21112  cply1coe0  21814  cply1coe0bi  21815  m2cpm  22234  m2cpminvid2lem  22247  fvmptnn04ifc  22345  vitali  25121  mbfi1fseqlem3  25226  dvexp2  25462  plyeq0lem  25715  abelthlem9  25943  logtayllem  26158  logtayl  26159  logtaylsum  26160  logtayl2  26161  cxpexp  26167  cxproot  26189  root1id  26251  root1eq1  26252  cxpeq  26254  logbgcd1irr  26288  atantayl  26431  atantayl2  26432  leibpilem2  26435  leibpi  26436  birthdaylem2  26446  birthdaylem3  26447  dfef2  26464  emcllem2  26490  emcllem3  26491  zetacvg  26508  lgam1  26557  basellem4  26577  basellem8  26581  basellem9  26582  mumullem2  26673  fsumdvdscom  26678  chtublem  26703  dchrelbas4  26735  bclbnd  26772  lgsval4a  26811  lgsabs1  26828  lgssq2  26830  dchrmusumlema  26985  dchrmusum2  26986  dchrvmasumiflem1  26993  dchrvmaeq0  26996  dchrisum0flblem1  27000  dchrisum0flblem2  27001  dchrisum0re  27005  ostthlem1  27119  ostth1  27125  pthdlem2lem  29013  wspthsnonn0vne  29160  clwwisshclwwslem  29256  ipasslem4  30074  ipasslem5  30075  divnumden2  32011  1fldgenq  32400  qqhval2  32950  qqhnm  32958  signstfveq0  33576  subfacp1lem6  34164  circum  34647  fz0n  34688  divcnvlin  34690  iprodgam  34700  faclim  34704  nndivsub  35330  poimirlem29  36505  poimirlem31  36507  poimirlem32  36508  heiborlem4  36670  heiborlem6  36672  nnproddivdvdsd  40854  pellexlem1  41552  congrep  41697  jm2.20nn  41721  proot1ex  41928  hashnzfzclim  43066  binomcxplemnotnn0  43100  nnne1ge2  43987  mccllem  44299  clim1fr1  44303  dvnxpaek  44644  dvnprodlem2  44649  wallispilem5  44771  wallispi2lem1  44773  stirlinglem1  44776  stirlinglem3  44778  stirlinglem4  44779  stirlinglem5  44780  stirlinglem7  44782  stirlinglem10  44785  stirlinglem12  44787  stirlinglem14  44789  stirlinglem15  44790  fouriersw  44933  vonioolem2  45383  vonicclem2  45386  iccpartiltu  46076  divgcdoddALTV  46336  fpprwppr  46393  nnsgrpnmnd  46574  eluz2cnn0n1  47145  mod0mul  47158  modn0mul  47159  blennn  47214  nnpw2blen  47219  digvalnn0  47238  nn0digval  47239  dignn0fr  47240  dignn0ldlem  47241  dig0  47245