Theorem peano2rem 11548

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7403  ℝcr 11126  1c1 11128   − cmin 11464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-ltxr 11272  df-sub 11466  df-neg 11467

This theorem is referenced by:  lem1  12082  addltmul  12475  div4p1lem1div2  12494  nnunb  12495  suprzcl  12671  zbtwnre  12960  rebtwnz  12961  qbtwnre  13213  qbtwnxr  13214  xnn0lem1lt  13258  xrinfmsslem  13322  xrub  13326  reltre  13355  elfznelfzo  13786  fldiv4p1lem1div2  13850  fldiv4lem1div2uz2  13851  ceile  13864  intfracq  13874  fldiv  13875  m1modnnsub1  13933  expubnd  14194  bernneq2  14246  expnbnd  14248  cshwidxm1  14823  isercolllem1  15679  tgioo  24733  icoopnst  24885  mbfi1fseqlem6  25671  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dgreq0  26221  advlog  26613  atanlogsublem  26875  birthdaylem3  26913  wilthlem1  27028  ftalem5  27037  ppiub  27165  chtublem  27172  chtub  27173  logfaclbnd  27183  logfacbnd3  27184  perfectlem2  27191  lgsval2lem  27268  lgsqrlem2  27308  gausslemma2dlem0c  27319  gausslemma2dlem1a  27326  lgseisenlem2  27337  lgseisen  27340  lgsquadlem1  27341  lgsquadlem2  27342  2lgslem1c  27354  2lgsoddprmlem2  27370  rplogsumlem1  27445  selberg2lem  27511  pntrsumo1  27526  pntpbnd1a  27546  colinearalglem4  28834  axlowdimlem16  28882  axeuclidlem  28887  nbusgrvtxm1  29304  pthdlem1  29694  crctcshwlkn0lem1  29738  wwlksm1edg  29809  clwwlkel  29973  clwwlknonex2lem2  30035  numclwwlk7  30318  addltmulALT  32373  cvmliftlem2  35254  cvmliftlem6  35258  cvmliftlem8  35260  cvmliftlem9  35261  cvmliftlem10  35262  irrdiff  37290  iooelexlt  37326  ltflcei  37578  poimirlem12  37602  poimirlem13  37603  poimirlem14  37604  poimirlem31  37621  poimirlem32  37622  itg2addnclem2  37642  itg2addnclem3  37643  monoords  45274  supxrgere  45308  infleinflem2  45346  unb2ltle  45390  limsupre3lem  45709  xlimxrre  45808  xlimmnfv  45811  stoweidlem14  45991  stoweidlem34  46011  fourierdlem11  46095  fourierdlem12  46096  fourierdlem15  46099  fourierdlem42  46126  fourierdlem50  46133  fourierdlem64  46147  fourierdlem79  46162  smfresal  46765  zm1nn  47279  ceilbi  47310  m1mod0mod1  47331  nn0oALTV  47658  perfectALTVlem2  47684  m1modmmod  48449  difmodm1lt  48450  flnn0div2ge  48461  logbpw2m1  48495  fllog2  48496