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

Theorem nnne0 11663
Description: A positive integer is nonzero. See nnne0ALT 11667 for a shorter proof using ax-pre-mulgt0 10606. This proof avoids 0lt1 11154, and thus ax-pre-mulgt0 10606, by splitting ax-1ne0 10598 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 10606. (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 10598 . . 3 1 ≠ 0
2 1re 10633 . . . 4 1 ∈ ℝ
3 0re 10635 . . . 4 0 ∈ ℝ
42, 3lttri2i 10746 . . 3 (1 ≠ 0 ↔ (1 < 0 ∨ 0 < 1))
51, 4mpbi 231 . 2 (1 < 0 ∨ 0 < 1)
6 breq1 5065 . . . . . . . 8 (𝑥 = 1 → (𝑥 < 0 ↔ 1 < 0))
76imbi2d 342 . . . . . . 7 (𝑥 = 1 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 1 < 0)))
8 breq1 5065 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 < 0 ↔ 𝑦 < 0))
98imbi2d 342 . . . . . . 7 (𝑥 = 𝑦 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝑦 < 0)))
10 breq1 5065 . . . . . . . 8 (𝑥 = (𝑦 + 1) → (𝑥 < 0 ↔ (𝑦 + 1) < 0))
1110imbi2d 342 . . . . . . 7 (𝑥 = (𝑦 + 1) → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → (𝑦 + 1) < 0)))
12 breq1 5065 . . . . . . . 8 (𝑥 = 𝐴 → (𝑥 < 0 ↔ 𝐴 < 0))
1312imbi2d 342 . . . . . . 7 (𝑥 = 𝐴 → ((1 < 0 → 𝑥 < 0) ↔ (1 < 0 → 𝐴 < 0)))
14 id 22 . . . . . . 7 (1 < 0 → 1 < 0)
15 simp1 1130 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℕ)
1615nnred 11645 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 ∈ ℝ)
17 1red 10634 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 ∈ ℝ)
1816, 17readdcld 10662 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) ∈ ℝ)
193, 2readdcli 10648 . . . . . . . . . . 11 (0 + 1) ∈ ℝ
2019a1i 11 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) ∈ ℝ)
21 0red 10636 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 0 ∈ ℝ)
22 simp3 1132 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 𝑦 < 0)
2316, 21, 17, 22ltadd1dd 11243 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < (0 + 1))
24 ax-1cn 10587 . . . . . . . . . . . 12 1 ∈ ℂ
2524addid2i 10820 . . . . . . . . . . 11 (0 + 1) = 1
26 simp2 1131 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → 1 < 0)
2725, 26eqbrtrid 5097 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (0 + 1) < 0)
2818, 20, 21, 23, 27lttrd 10793 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0) → (𝑦 + 1) < 0)
29283exp 1113 . . . . . . . 8 (𝑦 ∈ ℕ → (1 < 0 → (𝑦 < 0 → (𝑦 + 1) < 0)))
3029a2d 29 . . . . . . 7 (𝑦 ∈ ℕ → ((1 < 0 → 𝑦 < 0) → (1 < 0 → (𝑦 + 1) < 0)))
317, 9, 11, 13, 14, 30nnind 11648 . . . . . 6 (𝐴 ∈ ℕ → (1 < 0 → 𝐴 < 0))
3231imp 407 . . . . 5 ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 < 0)
3332lt0ne0d 11197 . . . 4 ((𝐴 ∈ ℕ ∧ 1 < 0) → 𝐴 ≠ 0)
3433ex 413 . . 3 (𝐴 ∈ ℕ → (1 < 0 → 𝐴 ≠ 0))
35 breq2 5066 . . . . . . . 8 (𝑥 = 1 → (0 < 𝑥 ↔ 0 < 1))
3635imbi2d 342 . . . . . . 7 (𝑥 = 1 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 1)))
37 breq2 5066 . . . . . . . 8 (𝑥 = 𝑦 → (0 < 𝑥 ↔ 0 < 𝑦))
3837imbi2d 342 . . . . . . 7 (𝑥 = 𝑦 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝑦)))
39 breq2 5066 . . . . . . . 8 (𝑥 = (𝑦 + 1) → (0 < 𝑥 ↔ 0 < (𝑦 + 1)))
4039imbi2d 342 . . . . . . 7 (𝑥 = (𝑦 + 1) → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < (𝑦 + 1))))
41 breq2 5066 . . . . . . . 8 (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴))
4241imbi2d 342 . . . . . . 7 (𝑥 = 𝐴 → ((0 < 1 → 0 < 𝑥) ↔ (0 < 1 → 0 < 𝐴)))
43 id 22 . . . . . . 7 (0 < 1 → 0 < 1)
44 simp1 1130 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℕ)
4544nnred 11645 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 𝑦 ∈ ℝ)
46 1red 10634 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 1 ∈ ℝ)
47 simp3 1132 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 𝑦)
48 simp2 1131 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < 1)
4945, 46, 47, 48addgt0d 11207 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦) → 0 < (𝑦 + 1))
50493exp 1113 . . . . . . . 8 (𝑦 ∈ ℕ → (0 < 1 → (0 < 𝑦 → 0 < (𝑦 + 1))))
5150a2d 29 . . . . . . 7 (𝑦 ∈ ℕ → ((0 < 1 → 0 < 𝑦) → (0 < 1 → 0 < (𝑦 + 1))))
5236, 38, 40, 42, 43, 51nnind 11648 . . . . . 6 (𝐴 ∈ ℕ → (0 < 1 → 0 < 𝐴))
5352imp 407 . . . . 5 ((𝐴 ∈ ℕ ∧ 0 < 1) → 0 < 𝐴)
5453gt0ne0d 11196 . . . 4 ((𝐴 ∈ ℕ ∧ 0 < 1) → 𝐴 ≠ 0)
5554ex 413 . . 3 (𝐴 ∈ ℕ → (0 < 1 → 𝐴 ≠ 0))
5634, 55jaod 855 . 2 (𝐴 ∈ ℕ → ((1 < 0 ∨ 0 < 1) → 𝐴 ≠ 0))
575, 56mpi 20 1 (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 843  w3a 1081   = wceq 1530  wcel 2106  wne 3020   class class class wbr 5062  (class class class)co 7151  cr 10528  0cc0 10529  1c1 10530   + caddc 10532   < clt 10667  cn 11630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-ov 7154  df-om 7572  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8282  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-nn 11631
This theorem is referenced by:  nnneneg  11664  0nnn  11665  nndivre  11670  nndiv  11675  nndivtr  11676  nnne0d  11679  zdiv  12044  zdivadd  12045  zdivmul  12046  elq  12342  qmulz  12343  qre  12345  qaddcl  12357  qnegcl  12358  qmulcl  12359  qreccl  12361  rpnnen1lem5  12373  nn0ledivnn  12495  fzo1fzo0n0  13081  quoremz  13216  quoremnn0ALT  13218  intfracq  13220  fldiv  13221  fldiv2  13222  modmulnn  13250  modsumfzodifsn  13305  expnnval  13425  expneg  13430  digit2  13590  facdiv  13640  facndiv  13641  bcm1k  13668  bcp1n  13669  bcval5  13671  hashnncl  13720  cshwidxmod  14158  relexpsucnnr  14377  divcnv  15200  harmonic  15206  expcnv  15211  ef0lem  15424  ruclem6  15580  sqrt2irr  15594  dvdsval3  15603  nndivdvds  15608  modmulconst  15633  dvdsdivcl  15658  dvdsflip  15659  divalg2  15748  divalgmod  15749  ndvdssub  15752  nndvdslegcd  15846  divgcdz  15852  divgcdnn  15855  modgcd  15872  gcddiv  15891  gcdzeq  15894  eucalgf  15919  eucalginv  15920  lcmgcdlem  15942  lcmftp  15972  qredeq  15993  qredeu  15994  cncongr1  16003  cncongr2  16004  isprm6  16050  divnumden  16080  divdenle  16081  phimullem  16108  hashgcdlem  16117  phisum  16119  prm23lt5  16143  pythagtriplem10  16149  pythagtriplem8  16152  pythagtriplem9  16153  pccl  16178  pcdiv  16181  pcqcl  16185  pcdvds  16192  pcndvds  16194  pcndvds2  16196  pceq0  16199  pcneg  16202  pcz  16209  pcmpt  16220  fldivp1  16225  pcfac  16227  oddprmdvds  16231  infpnlem2  16239  cshwshashlem1  16421  mulgnn  18164  mulgnegnn  18170  mulgmodid  18198  oddvdsnn0  18594  odmulgeq  18606  gexnnod  18635  cply1coe0  20384  cply1coe0bi  20385  qsssubdrg  20520  prmirredlem  20556  znf1o  20614  znhash  20621  znidomb  20624  znunithash  20627  znrrg  20628  m2cpm  21265  m2cpminvid2lem  21278  fvmptnn04ifc  21376  vitali  24129  mbfi1fseqlem3  24233  dvexp2  24466  plyeq0lem  24715  abelthlem9  24943  logtayllem  25155  logtayl  25156  logtaylsum  25157  logtayl2  25158  cxpexp  25164  cxproot  25186  root1id  25248  root1eq1  25249  cxpeq  25251  logbgcd1irr  25285  atantayl  25428  atantayl2  25429  leibpilem2  25433  leibpi  25434  birthdaylem2  25444  birthdaylem3  25445  dfef2  25462  emcllem2  25488  emcllem3  25489  zetacvg  25506  lgam1  25555  basellem4  25575  basellem8  25579  basellem9  25580  mumullem2  25671  fsumdvdscom  25676  chtublem  25701  dchrelbas4  25733  bclbnd  25770  lgsval4a  25809  lgsabs1  25826  lgssq2  25828  dchrmusumlema  25983  dchrmusum2  25984  dchrvmasumiflem1  25991  dchrvmaeq0  25994  dchrisum0flblem1  25998  dchrisum0flblem2  25999  dchrisum0re  26003  ostthlem1  26117  ostth1  26123  pthdlem2lem  27463  wspthsnonn0vne  27611  clwwisshclwwslem  27707  ipasslem4  28526  ipasslem5  28527  divnumden2  30448  qqhval2  31110  qqhnm  31118  signstfveq0  31734  subfacp1lem6  32317  circum  32802  fz0n  32847  divcnvlin  32849  iprodgam  32859  faclim  32863  nndivsub  33690  poimirlem29  34789  poimirlem31  34791  poimirlem32  34792  heiborlem4  34961  heiborlem6  34963  pellexlem1  39288  congrep  39432  jm2.20nn  39456  proot1ex  39663  hashnzfzclim  40516  binomcxplemnotnn0  40550  nnne1ge2  41420  mccllem  41740  clim1fr1  41744  dvnxpaek  42089  dvnprodlem2  42094  wallispilem5  42217  wallispi2lem1  42219  stirlinglem1  42222  stirlinglem3  42224  stirlinglem4  42225  stirlinglem5  42226  stirlinglem7  42228  stirlinglem10  42231  stirlinglem12  42233  stirlinglem14  42235  stirlinglem15  42236  fouriersw  42379  vonioolem2  42826  vonicclem2  42829  iccpartiltu  43411  divgcdoddALTV  43676  fpprwppr  43733  nnsgrpnmnd  43914  eluz2cnn0n1  44395  mod0mul  44408  modn0mul  44409  blennn  44464  nnpw2blen  44469  digvalnn0  44488  nn0digval  44489  dignn0fr  44490  dignn0ldlem  44491  dig0  44495
  Copyright terms: Public domain W3C validator