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

Theorem peano2rem 10196
Description: "Reverse" second Peano postulate analogue for reals. (Contributed by NM, 6-Feb-2007.)
Assertion
Ref Expression
peano2rem (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)

Proof of Theorem peano2rem
StepHypRef Expression
1 1re 9892 . 2 1 ∈ ℝ
2 resubcl 10193 . 2 ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 − 1) ∈ ℝ)
31, 2mpan2 702 1 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  (class class class)co 6524  cr 9788  1c1 9790  cmin 10114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-po 4946  df-so 4947  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-er 7603  df-en 7816  df-dom 7817  df-sdom 7818  df-pnf 9929  df-mnf 9930  df-ltxr 9932  df-sub 10116  df-neg 10117
This theorem is referenced by:  lem1  10710  addltmul  11112  div4p1lem1div2  11131  nnunb  11132  suprzcl  11286  zbtwnre  11615  rebtwnz  11616  qbtwnre  11860  qbtwnxr  11861  xrinfmsslem  11963  xrub  11967  reltre  11994  elfznelfzo  12391  fldiv4p1lem1div2  12450  fldiv4lem1div2uz2  12451  ceile  12462  intfracq  12472  fldiv  12473  m1modnnsub1  12530  expubnd  12735  bernneq2  12805  expnbnd  12807  cshwidxm1  13347  isercolllem1  14186  tgioo  22336  icoopnst  22474  mbfi1fseqlem6  23207  dvfsumlem1  23507  dvfsumlem2  23508  dgreq0  23739  advlog  24114  atanlogsublem  24356  birthdaylem3  24394  wilthlem1  24508  ftalem5  24517  ppiub  24643  chtublem  24650  chtub  24651  logfaclbnd  24661  logfacbnd3  24662  perfectlem2  24669  lgsval2lem  24746  lgsqrlem2  24786  gausslemma2dlem0c  24797  gausslemma2dlem1a  24804  lgseisenlem2  24815  lgseisen  24818  lgsquadlem1  24819  lgsquadlem2  24820  2lgslem1c  24832  2lgsoddprmlem2  24848  rplogsumlem1  24887  selberg2lem  24953  pntrsumo1  24968  pntpbnd1a  24988  colinearalglem4  25504  axlowdimlem16  25552  axeuclidlem  25557  wwlkm1edg  26026  clwwlkel  26084  eupap1  26266  usgreghash2spotv  26356  numclwwlkovf2ex  26376  numclwwlk5  26402  numclwwlk7  26404  addltmulALT  28492  cvmliftlem2  30325  cvmliftlem6  30329  cvmliftlem8  30331  cvmliftlem9  30332  cvmliftlem10  30333  iooelexlt  32186  ltflcei  32367  poimirlem12  32391  poimirlem13  32392  poimirlem14  32393  poimirlem31  32410  poimirlem32  32411  itg2addnclem2  32432  itg2addnclem3  32433  monoords  38252  supxrgere  38291  infleinflem2  38329  stoweidlem14  38708  stoweidlem34  38728  fourierdlem11  38812  fourierdlem12  38813  fourierdlem15  38816  fourierdlem42  38843  fourierdlem50  38850  fourierdlem64  38864  fourierdlem79  38879  smfresal  39474  m1mod0mod1  39751  nn0oALTV  39947  perfectALTVlem2  39967  zm1nn  40172  nbusgrvtxm1  40606  pthdlem1  40971  crctcsh1wlkn0lem1  41012  wwlksm1edg  41077  clwwlksel  41220  fusgreghash2wspv  41498  av-numclwwlkovf2ex  41516  av-numclwwlk7  41544  m1modmmod  42109  difmodm1lt  42110  flnn0div2ge  42120  logbpw2m1  42158  fllog2  42159
  Copyright terms: Public domain W3C validator