Theorem peano2re 8210

Description: A theorem for reals analogous the second Peano postulate peano2 4644. (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 8073	. 2 |- 1 e. RR
2		readdcl 8053	. 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 2176  (class class class)co 5946   RRcr 7926   1c1 7928   + caddc 7930

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

This theorem is referenced by:  lep1  8920  letrp1  8923  p1le  8924  ledivp1  8978  nnssre  9042  nn1suc  9057  nnge1  9061  div4p1lem1div2  9293  zltp1le  9429  suprzclex  9473  zeo  9480  peano2uz2  9482  uzind  9486  btwnapz  9505  numltc  9531  ge0p1rp  9809  fznatpl1  10200  ubmelm1fzo  10357  infssuzex  10378  qbtwnxr  10402  flhalf  10447  fldiv4p1lem1div2  10450  seq3split  10635  seq3f1olemqsumk  10659  seqf1oglem1  10666  seqf1oglem2  10667  bernneq3  10809  facwordi  10887  faclbnd  10888  expcnvap0  11846  cvgratnnlemfm  11873  cvgratnnlemrate  11874  cvgratz  11876  mertenslemi1  11879  fprodntrivap  11928  divalglemnqt  12264  nonsq  12562  eulerthlema  12585  pcfac  12706  1arith  12723  ennnfonelemkh  12816  tgioo  15059  suplociccreex  15129  hoverb  15153  reeff1olem  15276  lgsvalmod  15529  gausslemma2dlem3  15573  lgsquadlem2  15588