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

Theorem peano2rem 10571
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 10262 . 2 1 ∈ ℝ
2 resubcl 10568 . 2 ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 − 1) ∈ ℝ)
31, 2mpan2 672 1 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2148  (class class class)co 6812  cr 10158  1c1 10160  cmin 10489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-opab 4860  df-mpt 4877  df-id 5171  df-po 5184  df-so 5185  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-er 7917  df-en 8131  df-dom 8132  df-sdom 8133  df-pnf 10299  df-mnf 10300  df-ltxr 10302  df-sub 10491  df-neg 10492
This theorem is referenced by:  lem1  11087  addltmul  11492  div4p1lem1div2  11511  nnunb  11512  suprzcl  11681  zbtwnre  12011  rebtwnz  12012  qbtwnre  12254  qbtwnxr  12255  xrinfmsslem  12362  xrub  12366  reltre  12394  elfznelfzo  12803  fldiv4p1lem1div2  12866  fldiv4lem1div2uz2  12867  ceile  12878  intfracq  12888  fldiv  12889  m1modnnsub1  12946  expubnd  13150  bernneq2  13220  expnbnd  13222  cshwidxm1  13784  isercolllem1  14625  tgioo  22839  icoopnst  22978  mbfi1fseqlem6  23728  dvfsumlem1  24030  dvfsumlem2  24031  dgreq0  24262  advlog  24642  atanlogsublem  24884  birthdaylem3  24922  wilthlem1  25036  ftalem5  25045  ppiub  25171  chtublem  25178  chtub  25179  logfaclbnd  25189  logfacbnd3  25190  perfectlem2  25197  lgsval2lem  25274  lgsqrlem2  25314  gausslemma2dlem0c  25325  gausslemma2dlem1a  25332  lgseisenlem2  25343  lgseisen  25346  lgsquadlem1  25347  lgsquadlem2  25348  2lgslem1c  25360  2lgsoddprmlem2  25376  rplogsumlem1  25415  selberg2lem  25481  pntrsumo1  25496  pntpbnd1a  25516  colinearalglem4  26031  axlowdimlem16  26079  axeuclidlem  26084  nbusgrvtxm1  26525  pthdlem1  26918  crctcshwlkn0lem1  26959  wwlksm1edg  27036  clwwlkel  27223  clwwlknonex2lem2  27305  numclwwlk7  27607  addltmulALT  29662  cvmliftlem2  31623  cvmliftlem6  31627  cvmliftlem8  31629  cvmliftlem9  31630  cvmliftlem10  31631  iooelexlt  33564  ltflcei  33747  poimirlem12  33771  poimirlem13  33772  poimirlem14  33773  poimirlem31  33790  poimirlem32  33791  itg2addnclem2  33811  itg2addnclem3  33812  monoords  40036  supxrgere  40073  infleinflem2  40111  unb2ltle  40165  limsupre3lem  40488  xlimxrre  40581  xlimmnfv  40584  stoweidlem14  40754  stoweidlem34  40774  fourierdlem11  40858  fourierdlem12  40859  fourierdlem15  40862  fourierdlem42  40889  fourierdlem50  40896  fourierdlem64  40910  fourierdlem79  40925  smfresal  41521  zm1nn  41868  m1mod0mod1  41891  nn0oALTV  42159  perfectALTVlem2  42183  m1modmmod  42868  difmodm1lt  42869  flnn0div2ge  42879  logbpw2m1  42913  fllog2  42914
  Copyright terms: Public domain W3C validator