Theorem nnne0 12298

Description: A positive integer is nonzero. See nnne0ALT 12302 for a shorter proof using ax-pre-mulgt0 11205. This proof avoids 0lt1 11764, and thus ax-pre-mulgt0 11205, by splitting ax-1ne0 11197 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11205. (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 11197	. . 3 ⊢ 1 ≠ 0
2		1re 11236	. . . 4 ⊢ 1 ∈ ℝ
3		0re 11238	. . . 4 ⊢ 0 ∈ ℝ
4	2, 3	lttri2i 11352	. . 3 ⊢ (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
5	1, 4	mpbi 233	. 2 ⊢ (1 < 0 ∨ 0 < 1)
6		breq1 5110	. . . . . . 7 ⊢ (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
7	6	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8		breq1 5110	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
9	8	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10		breq1 5110	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
11	10	imbi2d 343	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12		breq1 5110	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
13	12	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14		id 23	. . . . . 6 ⊢ (1 < 0 → 1 < 0)
15		simp1 1154	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
16	15	nnred 12276	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17		1red 11237	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
18	16, 17	readdcld 11266	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
19	3, 2	readdcli 11252	. . . . . . . . . 10 ⊢ (0 + 1) ∈ ℝ
20	19	a1i 11	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21		0red 11239	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22		simp3 1156	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
23	16, 21, 17, 22	ltadd1dd 11853	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24		ax-1cn 11186	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
25	24	addlidi 11426	. . . . . . . . . 10 ⊢ (0 + 1) = 1
26		simp2 1155	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
27	25, 26	eqbrtrid 5144	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
28	18, 20, 21, 23, 27	lttrd 11399	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29	28	3exp 1137	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (1 < 0 → (𝑦 < 0 → (𝑦 + 1) < 0)))
30	29	a2d 30	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((1 < 0 → 𝑦 < 0) → (1 < 0 → (𝑦 + 1) < 0)))
31	7, 9, 11, 13, 14, 30	nnind 12279	. . . . 5 ⊢ (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
32	31	imp 412	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
33	32	lt0ne0d 11807	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
34		breq2 5111	. . . . . . 7 ⊢ (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
35	34	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
36		breq2 5111	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
37	36	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
38		breq2 5111	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
39	38	imbi2d 343	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
40		breq2 5111	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
41	40	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
42		id 23	. . . . . 6 ⊢ (0 < 1 → 0 < 1)
43		simp1 1154	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
44	43	nnred 12276	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
45		1red 11237	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
46		simp3 1156	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
47		simp2 1155	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
48	44, 45, 46, 47	addgt0d 11817	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
49	48	3exp 1137	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (0 < 1 → (0 < 𝑦 → 0 < (𝑦 + 1))))
50	49	a2d 30	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((0 < 1 → 0 < 𝑦) → (0 < 1 → 0 < (𝑦 + 1))))
51	35, 37, 39, 41, 42, 50	nnind 12279	. . . . 5 ⊢ (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
52	51	imp 412	. . . 4 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
53	52	gt0ne0d 11806	. . 3 ⊢ ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
54	33, 53	jaodan 972	. 2 ⊢ ((𝐴 ∈ ℕ ∧ (1 < 0 ∨ 0 < 1)) → 𝐴 ≠ 0)
55	5, 54	mpan2 704	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2957   class class class wbr 5107  (class class class)co 7417  ℝcr 11127  0cc0 11128  1c1 11129   + caddc 11131   < clt 11271  ℕcn 12261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-nn 12262

This theorem is used by:  nnneneg  12299  0nnn  12300  nndivre  12305  nndiv  12310  nndivtr  12311  nnne0d  12314  zdiv  12695  zdivadd  12696  zdivmul  12697  elq  13003  qmulz  13004  qre  13006  qaddcl  13019  qnegcl  13020  qmulcl  13021  qreccl  13023  rpnnen1lem5  13035  nn0ledivnn  13161  fzo1fzo0n0  13775  quoremz  13920  quoremnn0ALT  13922  intfracq  13924  fldiv  13925  fldiv2  13926  modmulnn  13954  modsumfzodifsn  14012  expnnval  14132  expneg  14137  digit2  14304  facdiv  14355  facndiv  14356  bcm1k  14383  bcp1n  14384  bcval5  14386  hashnncl  14434  cshwidxmod  14878  relexpsucnnr  15102  divcnv  15946  harmonic  15952  expcnv  15957  ef0lem  16170  ruclem6  16329  sqrt2irr  16343  dvdsval3  16352  nndivdvds  16357  modmulconst  16384  dvdsdivcl  16412  dvdsflip  16413  divalg2  16501  divalgmod  16502  ndvdssub  16505  nndvdslegcd  16601  divgcdz  16607  divgcdnn  16611  modgcd  16628  gcddiv  16647  gcdzeq  16648  eucalgf  16679  eucalginv  16680  lcmgcdlem  16702  lcmftp  16732  qredeq  16753  qredeu  16754  cncongr1  16763  cncongr2  16764  isprm6  16811  divnumden  16845  divdenle  16846  phimullem  16876  hashgcdlem  16885  phisum  16888  prm23lt5  16912  pythagtriplem10  16918  pythagtriplem8  16921  pythagtriplem9  16922  pccl  16947  pcdiv  16950  pcqcl  16954  pcdvds  16962  pcndvds  16964  pcndvds2  16966  pceq0  16969  pcneg  16972  pcz  16979  pcmpt  16990  fldivp1  16995  pcfac  16997  oddprmdvds  17001  infpnlem2  17009  cshwshashlem1  17193  smndex1n0mnd  19030  mulgnn  19204  mulgnegnn  19213  mulgmodid  19242  oddvdsnn0  19677  odmulgeq  19690  gexnnod  19721  qsssubdrg  21645  prmirredlem  21691  znf1o  21770  znhash  21777  znidomb  21780  znunithash  21783  znrrg  21784  cply1coe0  22532  cply1coe0bi  22533  m2cpm  22972  m2cpminvid2lem  22985  fvmptnn04ifc  23083  vitali  25847  mbfi1fseqlem3  25951  dvexp2  26188  plyeq0lem  26443  abelthlem9  26683  logtayllem  26904  logtayl  26905  logtaylsum  26906  logtayl2  26907  cxpexp  26913  cxproot  26935  root1id  26999  root1eq1  27000  cxpeq  27002  logbgcd1irr  27039  atantayl  27182  atantayl2  27183  leibpilem2  27186  leibpi  27187  birthdaylem2  27197  birthdaylem3  27198  dfef2  27215  emcllem2  27241  emcllem3  27242  zetacvg  27259  lgam1  27308  basellem4  27328  basellem8  27332  basellem9  27333  mumullem2  27424  fsumdvdscom  27429  chtublem  27455  dchrelbas4  27487  bclbnd  27524  lgsval4a  27563  lgsabs1  27580  lgssq2  27582  dchrmusumlema  27737  dchrmusum2  27738  dchrvmasumiflem1  27745  dchrvmaeq0  27748  dchrisum0flblem1  27752  dchrisum0flblem2  27753  dchrisum0re  27757  ostthlem1  27871  ostth1  27877  pthdlem2lem  30240  wspthsnonn0vne  30393  clwwisshclwwslem  30492  ipasslem4  31323  ipasslem5  31324  divnumden2  33294  1fldgenq  33771  qqhval2  34500  qqhnm  34508  signstfveq0  35093  subfacp1lem6  35772  circum  36261  fz0n  36318  divcnvlin  36320  iprodgam  36329  faclim  36333  nndivsub  37084  poimirlem29  38406  poimirlem31  38408  poimirlem32  38409  heiborlem4  38572  heiborlem6  38574  nnproddivdvdsd  42874  pellexlem1  43678  congrep  43822  jm2.20nn  43846  proot1ex  44045  hashnzfzclim  45154  binomcxplemnotnn0  45188  nnne1ge2  46132  mccllem  46435  clim1fr1  46439  dvnxpaek  46778  dvnprodlem2  46783  wallispilem5  46905  wallispi2lem1  46907  stirlinglem1  46910  stirlinglem3  46912  stirlinglem4  46913  stirlinglem5  46914  stirlinglem7  46916  stirlinglem10  46919  stirlinglem12  46921  stirlinglem14  46923  stirlinglem15  46924  fouriersw  47067  vonioolem2  47517  vonicclem2  47520  sqrtnnaa  47739  mod0mul  48258  modn0mul  48259  modlt0b  48265  iccpartiltu  48330  divgcdoddALTV  48606  fpprwppr  48663  isubgr3stgrlem7  48896  gpg3kgrtriexlem5  49011  nnsgrpnmnd  49101  eluz2cnn0n1  49449  blennn  49513  nnpw2blen  49518  digvalnn0  49537  nn0digval  49538  dignn0fr  49539  dignn0ldlem  49540  dig0  49544