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

Theorem peano2rem 10945
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 10633 . 2 1 ∈ ℝ
2 resubcl 10942 . 2 ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 − 1) ∈ ℝ)
31, 2mpan2 689 1 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  (class class class)co 7148  cr 10528  1c1 10530  cmin 10862
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 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  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 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  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-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-ltxr 10672  df-sub 10864  df-neg 10865
This theorem is referenced by:  lem1  11475  addltmul  11865  div4p1lem1div2  11884  nnunb  11885  suprzcl  12054  zbtwnre  12338  rebtwnz  12339  qbtwnre  12584  qbtwnxr  12585  xnn0lem1lt  12629  xrinfmsslem  12693  xrub  12697  reltre  12725  elfznelfzo  13134  fldiv4p1lem1div2  13197  fldiv4lem1div2uz2  13198  ceile  13209  intfracq  13219  fldiv  13220  m1modnnsub1  13277  expubnd  13533  bernneq2  13583  expnbnd  13585  cshwidxm1  14161  isercolllem1  15013  tgioo  23396  icoopnst  23535  mbfi1fseqlem6  24313  dvfsumlem1  24615  dvfsumlem2  24616  dgreq0  24847  advlog  25229  atanlogsublem  25485  birthdaylem3  25523  wilthlem1  25637  ftalem5  25646  ppiub  25772  chtublem  25779  chtub  25780  logfaclbnd  25790  logfacbnd3  25791  perfectlem2  25798  lgsval2lem  25875  lgsqrlem2  25915  gausslemma2dlem0c  25926  gausslemma2dlem1a  25933  lgseisenlem2  25944  lgseisen  25947  lgsquadlem1  25948  lgsquadlem2  25949  2lgslem1c  25961  2lgsoddprmlem2  25977  rplogsumlem1  26052  selberg2lem  26118  pntrsumo1  26133  pntpbnd1a  26153  colinearalglem4  26687  axlowdimlem16  26735  axeuclidlem  26740  nbusgrvtxm1  27153  pthdlem1  27539  crctcshwlkn0lem1  27580  wwlksm1edg  27651  clwwlkel  27817  clwwlknonex2lem2  27879  numclwwlk7  28162  addltmulALT  30215  cvmliftlem2  32521  cvmliftlem6  32525  cvmliftlem8  32527  cvmliftlem9  32528  cvmliftlem10  32529  iooelexlt  34630  ltflcei  34867  poimirlem12  34891  poimirlem13  34892  poimirlem14  34893  poimirlem31  34910  poimirlem32  34911  itg2addnclem2  34931  itg2addnclem3  34932  monoords  41548  supxrgere  41585  infleinflem2  41623  unb2ltle  41673  limsupre3lem  41997  xlimxrre  42096  xlimmnfv  42099  stoweidlem14  42284  stoweidlem34  42304  fourierdlem11  42388  fourierdlem12  42389  fourierdlem15  42392  fourierdlem42  42419  fourierdlem50  42426  fourierdlem64  42440  fourierdlem79  42455  smfresal  43048  zm1nn  43487  m1mod0mod1  43514  nn0oALTV  43846  perfectALTVlem2  43872  m1modmmod  44566  difmodm1lt  44567  flnn0div2ge  44578  logbpw2m1  44612  fllog2  44613
  Copyright terms: Public domain W3C validator