Theorem peano2re 8282

Description: A theorem for reals analogous the second Peano postulate peano2 4687. (Contributed by NM, 5-Jul-2005.)

Assertion

Ref	Expression
peano2re	|- ( A e. RR -> ( A + 1 ) e. RR )

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 8145	. 2 |- 1 e. RR
2		readdcl 8125	. 2 |- ( ( A e. RR /\ 1 e. RR ) -> ( A + 1 ) e. RR )
3	1, 2	mpan2 425	1 |- ( A e. RR -> ( A + 1 ) e. RR )

Syntax hints:   -> wi 4   e. wcel 2200  (class class class)co 6001   RRcr 7998   1c1 8000   + caddc 8002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-1re 8093  ax-addrcl 8096

This theorem is referenced by:  lep1  8992  letrp1  8995  p1le  8996  ledivp1  9050  nnssre  9114  nn1suc  9129  nnge1  9133  div4p1lem1div2  9365  zltp1le  9501  suprzclex  9545  zeo  9552  peano2uz2  9554  uzind  9558  btwnapz  9577  numltc  9603  ge0p1rp  9881  fznatpl1  10272  ubmelm1fzo  10432  infssuzex  10453  qbtwnxr  10477  flhalf  10522  fldiv4p1lem1div2  10525  seq3split  10710  seq3f1olemqsumk  10734  seqf1oglem1  10741  seqf1oglem2  10742  bernneq3  10884  facwordi  10962  faclbnd  10963  expcnvap0  12013  cvgratnnlemfm  12040  cvgratnnlemrate  12041  cvgratz  12043  mertenslemi1  12046  fprodntrivap  12095  divalglemnqt  12431  nonsq  12729  eulerthlema  12752  pcfac  12873  1arith  12890  ennnfonelemkh  12983  tgioo  15228  suplociccreex  15298  hoverb  15322  reeff1olem  15445  lgsvalmod  15698  gausslemma2dlem3  15742  lgsquadlem2  15757