Theorem peano2rem 10984

Description: "Reverse" second Peano postulate analogue for reals. (Contributed by NM, 6-Feb-2007.)

Assertion

Ref	Expression
peano2rem	⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)

Proof of Theorem peano2rem

Step	Hyp	Ref	Expression
1		1re 10672	. 2 ⊢ 1 ∈ ℝ
2		resubcl 10981	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 − 1) ∈ ℝ)
3	1, 2	mpan2 691	1 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2112  (class class class)co 7151  ℝcr 10567  1c1 10569   − cmin 10901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-po 5444  df-so 5445  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10708  df-mnf 10709  df-ltxr 10711  df-sub 10903  df-neg 10904

This theorem is referenced by:  lem1  11514  addltmul  11903  div4p1lem1div2  11922  nnunb  11923  suprzcl  12094  zbtwnre  12379  rebtwnz  12380  qbtwnre  12626  qbtwnxr  12627  xnn0lem1lt  12671  xrinfmsslem  12735  xrub  12739  reltre  12767  elfznelfzo  13184  fldiv4p1lem1div2  13247  fldiv4lem1div2uz2  13248  ceile  13259  intfracq  13269  fldiv  13270  m1modnnsub1  13327  expubnd  13584  bernneq2  13634  expnbnd  13636  cshwidxm1  14209  isercolllem1  15062  tgioo  23490  icoopnst  23633  mbfi1fseqlem6  24413  dvfsumlem1  24718  dvfsumlem2  24719  dgreq0  24954  advlog  25337  atanlogsublem  25593  birthdaylem3  25631  wilthlem1  25745  ftalem5  25754  ppiub  25880  chtublem  25887  chtub  25888  logfaclbnd  25898  logfacbnd3  25899  perfectlem2  25906  lgsval2lem  25983  lgsqrlem2  26023  gausslemma2dlem0c  26034  gausslemma2dlem1a  26041  lgseisenlem2  26052  lgseisen  26055  lgsquadlem1  26056  lgsquadlem2  26057  2lgslem1c  26069  2lgsoddprmlem2  26085  rplogsumlem1  26160  selberg2lem  26226  pntrsumo1  26241  pntpbnd1a  26261  colinearalglem4  26795  axlowdimlem16  26843  axeuclidlem  26848  nbusgrvtxm1  27261  pthdlem1  27647  crctcshwlkn0lem1  27688  wwlksm1edg  27759  clwwlkel  27923  clwwlknonex2lem2  27985  numclwwlk7  28268  addltmulALT  30321  cvmliftlem2  32757  cvmliftlem6  32761  cvmliftlem8  32763  cvmliftlem9  32764  cvmliftlem10  32765  irrdiff  35013  iooelexlt  35052  ltflcei  35318  poimirlem12  35342  poimirlem13  35343  poimirlem14  35344  poimirlem31  35361  poimirlem32  35362  itg2addnclem2  35382  itg2addnclem3  35383  monoords  42290  supxrgere  42326  infleinflem2  42364  unb2ltle  42411  limsupre3lem  42733  xlimxrre  42832  xlimmnfv  42835  stoweidlem14  43015  stoweidlem34  43035  fourierdlem11  43119  fourierdlem12  43120  fourierdlem15  43123  fourierdlem42  43150  fourierdlem50  43157  fourierdlem64  43171  fourierdlem79  43186  smfresal  43779  zm1nn  44220  m1mod0mod1  44247  nn0oALTV  44574  perfectALTVlem2  44600  m1modmmod  45293  difmodm1lt  45294  flnn0div2ge  45305  logbpw2m1  45339  fllog2  45340