Theorem nnne0 12007

Description: A positive integer is nonzero. See nnne0ALT 12011 for a shorter proof using ax-pre-mulgt0 10948. This proof avoids 0lt1 11497, and thus ax-pre-mulgt0 10948, by splitting ax-1ne0 10940 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 10948. (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 10940	. . 3 ⊢ 1 ≠ 0
2		1re 10975	. . . 4 ⊢ 1 ∈ ℝ
3		0re 10977	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11089	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 229	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5077	. . . . . . . 8 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5077	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5077	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5077	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 22	. . . . . . 7 ⊢ (1 < 0 → 1 < 0)
15		simp1 1135	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 11988	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 10976	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11004	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 10990	. . . . . . . . . . 11 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 10978	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1137	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11586	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 10929	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
25	24	addid2i 11163	. . . . . . . . . . 11 ⊢ (0 + 1) = 1
26		simp2 1136	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5109	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11136	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1118	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (1 < 0 → (𝑦 < 0 → (𝑦 + 1) < 0)))
30	29	a2d 29	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((1 < 0 → 𝑦 < 0) → (1 < 0 → (𝑦 + 1) < 0)))
31	7, 9, 11, 13, 14, 30	nnind 11991	. . . . . 6 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 407	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11540	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34	33	ex 413	. . 3 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 ≠ 0))
35		breq2 5078	. . . . . . . 8 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
36	35	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
37		breq2 5078	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
38	37	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
39		breq2 5078	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
40	39	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
41		breq2 5078	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
42	41	imbi2d 341	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
43		id 22	. . . . . . 7 ⊢ (0 < 1 → 0 < 1)
44		simp1 1135	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
45	44	nnred 11988	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
46		1red 10976	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
47		simp3 1137	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
48		simp2 1136	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
49	45, 46, 47, 48	addgt0d 11550	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
50	49	3exp 1118	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → (0 < 1 → (0 < 𝑦 → 0 < (𝑦 + 1))))
51	50	a2d 29	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → ((0 < 1 → 0 < 𝑦) → (0 < 1 → 0 < (𝑦 + 1))))
52	36, 38, 40, 42, 43, 51	nnind 11991	. . . . . 6 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
53	52	imp 407	. . . . 5 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
54	53	gt0ne0d 11539	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
55	54	ex 413	. . 3 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 𝐴 ≠ 0))
56	34, 55	jaod 856	. 2 ⊢ (𝐴 ∈ ℕ → ((1 < 0 ∨ 0 < 1) → 𝐴 ≠ 0))
57	5, 56	mpi 20	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943   class class class wbr 5074  (class class class)co 7275  ℝcr 10870  0cc0 10871  1c1 10872   + caddc 10874   < clt 11009  ℕcn 11973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-nn 11974

This theorem is referenced by:  nnneneg  12008  0nnn  12009  nndivre  12014  nndiv  12019  nndivtr  12020  nnne0d  12023  zdiv  12390  zdivadd  12391  zdivmul  12392  elq  12690  qmulz  12691  qre  12693  qaddcl  12705  qnegcl  12706  qmulcl  12707  qreccl  12709  rpnnen1lem5  12721  nn0ledivnn  12843  fzo1fzo0n0  13438  quoremz  13575  quoremnn0ALT  13577  intfracq  13579  fldiv  13580  fldiv2  13581  modmulnn  13609  modsumfzodifsn  13664  expnnval  13785  expneg  13790  digit2  13951  facdiv  14001  facndiv  14002  bcm1k  14029  bcp1n  14030  bcval5  14032  hashnncl  14081  cshwidxmod  14516  relexpsucnnr  14736  divcnv  15565  harmonic  15571  expcnv  15576  ef0lem  15788  ruclem6  15944  sqrt2irr  15958  dvdsval3  15967  nndivdvds  15972  modmulconst  15997  dvdsdivcl  16025  dvdsflip  16026  divalg2  16114  divalgmod  16115  ndvdssub  16118  nndvdslegcd  16212  divgcdz  16218  divgcdnn  16222  modgcd  16240  gcddiv  16259  gcdzeq  16262  eucalgf  16288  eucalginv  16289  lcmgcdlem  16311  lcmftp  16341  qredeq  16362  qredeu  16363  cncongr1  16372  cncongr2  16373  isprm6  16419  divnumden  16452  divdenle  16453  phimullem  16480  hashgcdlem  16489  phisum  16491  prm23lt5  16515  pythagtriplem10  16521  pythagtriplem8  16524  pythagtriplem9  16525  pccl  16550  pcdiv  16553  pcqcl  16557  pcdvds  16565  pcndvds  16567  pcndvds2  16569  pceq0  16572  pcneg  16575  pcz  16582  pcmpt  16593  fldivp1  16598  pcfac  16600  oddprmdvds  16604  infpnlem2  16612  cshwshashlem1  16797  smndex1n0mnd  18551  mulgnn  18708  mulgnegnn  18714  mulgmodid  18742  oddvdsnn0  19152  odmulgeq  19164  gexnnod  19193  qsssubdrg  20657  prmirredlem  20694  znf1o  20759  znhash  20766  znidomb  20769  znunithash  20772  znrrg  20773  cply1coe0  21470  cply1coe0bi  21471  m2cpm  21890  m2cpminvid2lem  21903  fvmptnn04ifc  22001  vitali  24777  mbfi1fseqlem3  24882  dvexp2  25118  plyeq0lem  25371  abelthlem9  25599  logtayllem  25814  logtayl  25815  logtaylsum  25816  logtayl2  25817  cxpexp  25823  cxproot  25845  root1id  25907  root1eq1  25908  cxpeq  25910  logbgcd1irr  25944  atantayl  26087  atantayl2  26088  leibpilem2  26091  leibpi  26092  birthdaylem2  26102  birthdaylem3  26103  dfef2  26120  emcllem2  26146  emcllem3  26147  zetacvg  26164  lgam1  26213  basellem4  26233  basellem8  26237  basellem9  26238  mumullem2  26329  fsumdvdscom  26334  chtublem  26359  dchrelbas4  26391  bclbnd  26428  lgsval4a  26467  lgsabs1  26484  lgssq2  26486  dchrmusumlema  26641  dchrmusum2  26642  dchrvmasumiflem1  26649  dchrvmaeq0  26652  dchrisum0flblem1  26656  dchrisum0flblem2  26657  dchrisum0re  26661  ostthlem1  26775  ostth1  26781  pthdlem2lem  28135  wspthsnonn0vne  28282  clwwisshclwwslem  28378  ipasslem4  29196  ipasslem5  29197  divnumden2  31132  qqhval2  31932  qqhnm  31940  signstfveq0  32556  subfacp1lem6  33147  circum  33632  fz0n  33696  divcnvlin  33698  iprodgam  33708  faclim  33712  nndivsub  34646  poimirlem29  35806  poimirlem31  35808  poimirlem32  35809  heiborlem4  35972  heiborlem6  35974  nnproddivdvdsd  40009  pellexlem1  40651  congrep  40795  jm2.20nn  40819  proot1ex  41026  hashnzfzclim  41940  binomcxplemnotnn0  41974  nnne1ge2  42830  mccllem  43138  clim1fr1  43142  dvnxpaek  43483  dvnprodlem2  43488  wallispilem5  43610  wallispi2lem1  43612  stirlinglem1  43615  stirlinglem3  43617  stirlinglem4  43618  stirlinglem5  43619  stirlinglem7  43621  stirlinglem10  43624  stirlinglem12  43626  stirlinglem14  43628  stirlinglem15  43629  fouriersw  43772  vonioolem2  44219  vonicclem2  44222  iccpartiltu  44874  divgcdoddALTV  45134  fpprwppr  45191  nnsgrpnmnd  45372  eluz2cnn0n1  45852  mod0mul  45865  modn0mul  45866  blennn  45921  nnpw2blen  45926  digvalnn0  45945  nn0digval  45946  dignn0fr  45947  dignn0ldlem  45948  dig0  45952