Theorem peano2rem 11618

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 11301	. 2 ⊢ 1 ∈ ℝ
2		resubcl 11615	. 2 ⊢ ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑁 − 1) ∈ ℝ)
3	1, 2	mpan2 704	1 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7418  ℝcr 11192  1c1 11194   − cmin 11534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341  df-sub 11536  df-neg 11537

This theorem is used by:  lem1  12153  addltmul  12575  div4p1lem1div2  12594  nnunb  12595  suprzcl  12772  zbtwnre  13066  rebtwnz  13067  qbtwnre  13322  qbtwnxr  13323  xnn0lem1lt  13367  xrinfmsslem  13431  xrub  13435  reltre  13464  elfznelfzo  13901  fldiv4p1lem1div2  13968  fldiv4lem1div2uz2  13969  ceile  13982  intfracq  13992  fldiv  13993  m1modnnsub1  14053  expubnd  14314  bernneq2  14367  expnbnd  14369  cshwidxm1  14951  isercolllem1  15825  chnccat  18793  tgioo  25108  icoopnst  25253  mbfi1fseqlem6  26034  dvfsumlem1  26339  dvfsumlem2  26340  dgreq0  26577  advlog  26975  atanlogsublem  27236  birthdaylem3  27274  wilthlem1  27388  ftalem5  27397  ppiub  27524  chtublem  27531  chtub  27532  logfaclbnd  27542  logfacbnd3  27543  perfectlem2  27550  lgsval2lem  27627  lgsqrlem2  27667  gausslemma2dlem0c  27678  gausslemma2dlem1a  27685  lgseisenlem2  27696  lgseisen  27699  lgsquadlem1  27700  lgsquadlem2  27701  2lgslem1c  27713  2lgsoddprmlem2  27729  rplogsumlem1  27804  selberg2lem  27870  pntrsumo1  27885  pntpbnd1a  27905  colinearalglem4  29480  axlowdimlem16  29528  axeuclidlem  29533  nbusgrvtxm1  29953  pthdlem1  30345  crctcshwlkn0lem1  30392  wwlksm1edg  30463  clwwlkel  30630  clwwlknonex2lem2  30692  numclwwlk7  30985  addltmulALT  33041  cvmliftlem2  36030  cvmliftlem6  36034  cvmliftlem8  36036  cvmliftlem9  36037  cvmliftlem10  36038  irrdiff  38227  iooelexlt  38265  ltflcei  38511  poimirlem12  38530  poimirlem13  38531  poimirlem14  38532  poimirlem31  38549  poimirlem32  38550  itg2addnclem2  38570  itg2addnclem3  38571  monoords  46282  supxrgere  46314  infleinflem2  46351  unb2ltle  46394  limsupre3lem  46711  xlimxrre  46810  xlimmnfv  46813  stoweidlem14  46993  stoweidlem34  47013  fourierdlem11  47097  fourierdlem12  47098  fourierdlem15  47101  fourierdlem42  47128  fourierdlem50  47135  fourierdlem64  47149  fourierdlem79  47164  smfresal  47767  chnsubseq  47859  zm1nn  48341  ceilbi  48376  m1mod0mod1  48399  m1modmmod  48403  2timesltsqm1  48418  nn0oALTV  48763  perfectALTVlem2  48789  flnn0div2ge  49614  logbpw2m1  49648  fllog2  49649