Theorem nnne0 12327

Description: A positive integer is nonzero. See nnne0ALT 12331 for a shorter proof using ax-pre-mulgt0 11261. This proof avoids 0lt1 11812, and thus ax-pre-mulgt0 11261, by splitting ax-1ne0 11253 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11261. (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 11253	. . 3 ⊢ 1 ≠ 0
2		1re 11290	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11292	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11404	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 230	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5169	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5169	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5169	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5169	. . . . . . 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 12308	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11291	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11319	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11305	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11293	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11901	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11242	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11478	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5201	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11451	. . . . . . . 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 12311	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11855	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5170	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5170	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5170	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5170	. . . . . . 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 12308	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11291	. . . . . . . . 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 11865	. . . . . . . 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 12311	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 406	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11854	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 958	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 690	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 846   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108   ≠ wne 2946   class class class wbr 5166  (class class class)co 7448  ℝcr 11183  0cc0 11184  1c1 11185   + caddc 11187   < clt 11324  ℕcn 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-nn 12294

This theorem is referenced by:  nnneneg  12328  0nnn  12329  nndivre  12334  nndiv  12339  nndivtr  12340  nnne0d  12343  zdiv  12713  zdivadd  12714  zdivmul  12715  elq  13015  qmulz  13016  qre  13018  qaddcl  13030  qnegcl  13031  qmulcl  13032  qreccl  13034  rpnnen1lem5  13046  nn0ledivnn  13170  fzo1fzo0n0  13767  quoremz  13906  quoremnn0ALT  13908  intfracq  13910  fldiv  13911  fldiv2  13912  modmulnn  13940  modsumfzodifsn  13995  expnnval  14115  expneg  14120  digit2  14285  facdiv  14336  facndiv  14337  bcm1k  14364  bcp1n  14365  bcval5  14367  hashnncl  14415  cshwidxmod  14851  relexpsucnnr  15074  divcnv  15901  harmonic  15907  expcnv  15912  ef0lem  16126  ruclem6  16283  sqrt2irr  16297  dvdsval3  16306  nndivdvds  16311  modmulconst  16336  dvdsdivcl  16364  dvdsflip  16365  divalg2  16453  divalgmod  16454  ndvdssub  16457  nndvdslegcd  16551  divgcdz  16557  divgcdnn  16561  modgcd  16579  gcddiv  16598  gcdzeq  16599  eucalgf  16630  eucalginv  16631  lcmgcdlem  16653  lcmftp  16683  qredeq  16704  qredeu  16705  cncongr1  16714  cncongr2  16715  isprm6  16761  divnumden  16795  divdenle  16796  phimullem  16826  hashgcdlem  16835  phisum  16837  prm23lt5  16861  pythagtriplem10  16867  pythagtriplem8  16870  pythagtriplem9  16871  pccl  16896  pcdiv  16899  pcqcl  16903  pcdvds  16911  pcndvds  16913  pcndvds2  16915  pceq0  16918  pcneg  16921  pcz  16928  pcmpt  16939  fldivp1  16944  pcfac  16946  oddprmdvds  16950  infpnlem2  16958  cshwshashlem1  17143  smndex1n0mnd  18947  mulgnn  19115  mulgnegnn  19124  mulgmodid  19153  oddvdsnn0  19586  odmulgeq  19599  gexnnod  19630  qsssubdrg  21467  prmirredlem  21506  znf1o  21593  znhash  21600  znidomb  21603  znunithash  21606  znrrg  21607  cply1coe0  22326  cply1coe0bi  22327  m2cpm  22768  m2cpminvid2lem  22781  fvmptnn04ifc  22879  vitali  25667  mbfi1fseqlem3  25772  dvexp2  26012  plyeq0lem  26269  abelthlem9  26502  logtayllem  26719  logtayl  26720  logtaylsum  26721  logtayl2  26722  cxpexp  26728  cxproot  26750  root1id  26815  root1eq1  26816  cxpeq  26818  logbgcd1irr  26855  atantayl  26998  atantayl2  26999  leibpilem2  27002  leibpi  27003  birthdaylem2  27013  birthdaylem3  27014  dfef2  27032  emcllem2  27058  emcllem3  27059  zetacvg  27076  lgam1  27125  basellem4  27145  basellem8  27149  basellem9  27150  mumullem2  27241  fsumdvdscom  27246  chtublem  27273  dchrelbas4  27305  bclbnd  27342  lgsval4a  27381  lgsabs1  27398  lgssq2  27400  dchrmusumlema  27555  dchrmusum2  27556  dchrvmasumiflem1  27563  dchrvmaeq0  27566  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0re  27575  ostthlem1  27689  ostth1  27695  pthdlem2lem  29803  wspthsnonn0vne  29950  clwwisshclwwslem  30046  ipasslem4  30866  ipasslem5  30867  divnumden2  32819  1fldgenq  33289  qqhval2  33928  qqhnm  33936  signstfveq0  34554  subfacp1lem6  35153  circum  35642  fz0n  35693  divcnvlin  35695  iprodgam  35704  faclim  35708  nndivsub  36423  poimirlem29  37609  poimirlem31  37611  poimirlem32  37612  heiborlem4  37774  heiborlem6  37776  nnproddivdvdsd  41957  pellexlem1  42785  congrep  42930  jm2.20nn  42954  proot1ex  43157  hashnzfzclim  44291  binomcxplemnotnn0  44325  nnne1ge2  45206  mccllem  45518  clim1fr1  45522  dvnxpaek  45863  dvnprodlem2  45868  wallispilem5  45990  wallispi2lem1  45992  stirlinglem1  45995  stirlinglem3  45997  stirlinglem4  45998  stirlinglem5  45999  stirlinglem7  46001  stirlinglem10  46004  stirlinglem12  46006  stirlinglem14  46008  stirlinglem15  46009  fouriersw  46152  vonioolem2  46602  vonicclem2  46605  iccpartiltu  47296  divgcdoddALTV  47556  fpprwppr  47613  nnsgrpnmnd  47901  eluz2cnn0n1  48240  mod0mul  48253  modn0mul  48254  blennn  48309  nnpw2blen  48314  digvalnn0  48333  nn0digval  48334  dignn0fr  48335  dignn0ldlem  48336  dig0  48340