MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnne0 Structured version   Visualization version   GIF version

Theorem nnne0 11659
Description: A positive integer is nonzero. See nnne0ALT 11663 for a shorter proof using ax-pre-mulgt0 10602. This proof avoids 0lt1 11150, and thus ax-pre-mulgt0 10602, by splitting ax-1ne0 10594 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 10602. (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.
StepHypRef Expression
1 ax-1ne0 10594 . . 3 1 ≠ 0
2 1re 10629 . . . 4 1 ∈ ℝ
3 0re 10631 . . . 4 0 ∈ ℝ
42, 3lttri2i 10742 . . 3 (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
51, 4mpbi 231 . 2 (1 < 0 ∨ 0 < 1)
6 breq1 5060 . . . . . . . 8 (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
76imbi2d 342 . . . . . . 7 (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8 breq1 5060 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
98imbi2d 342 . . . . . . 7 (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10 breq1 5060 . . . . . . . 8 (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
1110imbi2d 342 . . . . . . 7 (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12 breq1 5060 . . . . . . . 8 (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
1312imbi2d 342 . . . . . . 7 (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14 id 22 . . . . . . 7 (1 < 0 → 1 < 0)
15 simp1 1128 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
1615nnred 11641 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17 1red 10630 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
1816, 17readdcld 10658 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
193, 2readdcli 10644 . . . . . . . . . . 11 (0 + 1) ∈ ℝ
2019a1i 11 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21 0red 10632 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22 simp3 1130 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
2316, 21, 17, 22ltadd1dd 11239 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24 ax-1cn 10583 . . . . . . . . . . . 12 1 ∈ ℂ
2524addid2i 10816 . . . . . . . . . . 11 (0 + 1) = 1
26 simp2 1129 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
2725, 26eqbrtrid 5092 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
2818, 20, 21, 23, 27lttrd 10789 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29283exp 1111 . . . . . . . 8 (𝑦 ∈ ℕ → (1 < 0 → (𝑦 < 0 → (𝑦 + 1) < 0)))
3029a2d 29 . . . . . . 7 (𝑦 ∈ ℕ → ((1 < 0 → 𝑦 < 0) → (1 < 0 → (𝑦 + 1) < 0)))
317, 9, 11, 13, 14, 30nnind 11644 . . . . . 6 (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
3231imp 407 . . . . 5 ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
3332lt0ne0d 11193 . . . 4 ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
3433ex 413 . . 3 (𝐴 ∈ ℕ → (1 < 0 → 𝐴 ≠ 0))
35 breq2 5061 . . . . . . . 8 (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
3635imbi2d 342 . . . . . . 7 (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
37 breq2 5061 . . . . . . . 8 (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
3837imbi2d 342 . . . . . . 7 (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
39 breq2 5061 . . . . . . . 8 (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
4039imbi2d 342 . . . . . . 7 (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
41 breq2 5061 . . . . . . . 8 (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
4241imbi2d 342 . . . . . . 7 (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
43 id 22 . . . . . . 7 (0 < 1 → 0 < 1)
44 simp1 1128 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
4544nnred 11641 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
46 1red 10630 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
47 simp3 1130 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
48 simp2 1129 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
4945, 46, 47, 48addgt0d 11203 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
50493exp 1111 . . . . . . . 8 (𝑦 ∈ ℕ → (0 < 1 → (0 < 𝑦 → 0 < (𝑦 + 1))))
5150a2d 29 . . . . . . 7 (𝑦 ∈ ℕ → ((0 < 1 → 0 < 𝑦) → (0 < 1 → 0 < (𝑦 + 1))))
5236, 38, 40, 42, 43, 51nnind 11644 . . . . . 6 (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
5352imp 407 . . . . 5 ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
5453gt0ne0d 11192 . . . 4 ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
5554ex 413 . . 3 (𝐴 ∈ ℕ → (0 < 1 → 𝐴 ≠ 0))
5634, 55jaod 853 . 2 (𝐴 ∈ ℕ → ((1 < 0 ∨ 0 < 1) → 𝐴 ≠ 0))
575, 56mpi 20 1 (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 841  w3a 1079   = wceq 1528  wcel 2105  wne 3013   class class class wbr 5057  (class class class)co 7145  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   < clt 10663  cn 11626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-om 7570  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-nn 11627
This theorem is referenced by:  nnneneg  11660  0nnn  11661  nndivre  11666  nndiv  11671  nndivtr  11672  nnne0d  11675  zdiv  12040  zdivadd  12041  zdivmul  12042  elq  12338  qmulz  12339  qre  12341  qaddcl  12352  qnegcl  12353  qmulcl  12354  qreccl  12356  rpnnen1lem5  12368  nn0ledivnn  12490  fzo1fzo0n0  13076  quoremz  13211  quoremnn0ALT  13213  intfracq  13215  fldiv  13216  fldiv2  13217  modmulnn  13245  modsumfzodifsn  13300  expnnval  13420  expneg  13425  digit2  13585  facdiv  13635  facndiv  13636  bcm1k  13663  bcp1n  13664  bcval5  13666  hashnncl  13715  cshwidxmod  14153  relexpsucnnr  14372  divcnv  15196  harmonic  15202  expcnv  15207  ef0lem  15420  ruclem6  15576  sqrt2irr  15590  dvdsval3  15599  nndivdvds  15604  modmulconst  15629  dvdsdivcl  15654  dvdsflip  15655  divalg2  15744  divalgmod  15745  ndvdssub  15748  nndvdslegcd  15842  divgcdz  15848  divgcdnn  15851  modgcd  15868  gcddiv  15887  gcdzeq  15890  eucalgf  15915  eucalginv  15916  lcmgcdlem  15938  lcmftp  15968  qredeq  15989  qredeu  15990  cncongr1  15999  cncongr2  16000  isprm6  16046  divnumden  16076  divdenle  16077  phimullem  16104  hashgcdlem  16113  phisum  16115  prm23lt5  16139  pythagtriplem10  16145  pythagtriplem8  16148  pythagtriplem9  16149  pccl  16174  pcdiv  16177  pcqcl  16181  pcdvds  16188  pcndvds  16190  pcndvds2  16192  pceq0  16195  pcneg  16198  pcz  16205  pcmpt  16216  fldivp1  16221  pcfac  16223  oddprmdvds  16227  infpnlem2  16235  cshwshashlem1  16417  mulgnn  18170  mulgnegnn  18176  mulgmodid  18204  oddvdsnn0  18601  odmulgeq  18613  gexnnod  18642  cply1coe0  20395  cply1coe0bi  20396  qsssubdrg  20532  prmirredlem  20568  znf1o  20626  znhash  20633  znidomb  20636  znunithash  20639  znrrg  20640  m2cpm  21277  m2cpminvid2lem  21290  fvmptnn04ifc  21388  vitali  24141  mbfi1fseqlem3  24245  dvexp2  24478  plyeq0lem  24727  abelthlem9  24955  logtayllem  25169  logtayl  25170  logtaylsum  25171  logtayl2  25172  cxpexp  25178  cxproot  25200  root1id  25262  root1eq1  25263  cxpeq  25265  logbgcd1irr  25299  atantayl  25442  atantayl2  25443  leibpilem2  25446  leibpi  25447  birthdaylem2  25457  birthdaylem3  25458  dfef2  25475  emcllem2  25501  emcllem3  25502  zetacvg  25519  lgam1  25568  basellem4  25588  basellem8  25592  basellem9  25593  mumullem2  25684  fsumdvdscom  25689  chtublem  25714  dchrelbas4  25746  bclbnd  25783  lgsval4a  25822  lgsabs1  25839  lgssq2  25841  dchrmusumlema  25996  dchrmusum2  25997  dchrvmasumiflem1  26004  dchrvmaeq0  26007  dchrisum0flblem1  26011  dchrisum0flblem2  26012  dchrisum0re  26016  ostthlem1  26130  ostth1  26136  pthdlem2lem  27475  wspthsnonn0vne  27623  clwwisshclwwslem  27719  ipasslem4  28538  ipasslem5  28539  divnumden2  30460  qqhval2  31122  qqhnm  31130  signstfveq0  31746  subfacp1lem6  32329  circum  32814  fz0n  32859  divcnvlin  32861  iprodgam  32871  faclim  32875  nndivsub  33702  poimirlem29  34802  poimirlem31  34804  poimirlem32  34805  heiborlem4  34973  heiborlem6  34975  pellexlem1  39304  congrep  39448  jm2.20nn  39472  proot1ex  39679  hashnzfzclim  40531  binomcxplemnotnn0  40565  nnne1ge2  41434  mccllem  41754  clim1fr1  41758  dvnxpaek  42103  dvnprodlem2  42108  wallispilem5  42231  wallispi2lem1  42233  stirlinglem1  42236  stirlinglem3  42238  stirlinglem4  42239  stirlinglem5  42240  stirlinglem7  42242  stirlinglem10  42245  stirlinglem12  42247  stirlinglem14  42249  stirlinglem15  42250  fouriersw  42393  vonioolem2  42840  vonicclem2  42843  iccpartiltu  43459  divgcdoddALTV  43724  fpprwppr  43781  nnsgrpnmnd  43962  smndex1n0mnd  44012  eluz2cnn0n1  44494  mod0mul  44507  modn0mul  44508  blennn  44563  nnpw2blen  44568  digvalnn0  44587  nn0digval  44588  dignn0fr  44589  dignn0ldlem  44590  dig0  44594
  Copyright terms: Public domain W3C validator