Theorem peano2re 8179

Description: A theorem for reals analogous the second Peano postulate peano2 4632. (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 8042	. 2 |- 1 e. RR
2		readdcl 8022	. 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 2167  (class class class)co 5925   RRcr 7895   1c1 7897   + caddc 7899

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

This theorem is referenced by:  lep1  8889  letrp1  8892  p1le  8893  ledivp1  8947  nnssre  9011  nn1suc  9026  nnge1  9030  div4p1lem1div2  9262  zltp1le  9397  suprzclex  9441  zeo  9448  peano2uz2  9450  uzind  9454  btwnapz  9473  numltc  9499  ge0p1rp  9777  fznatpl1  10168  ubmelm1fzo  10319  infssuzex  10340  qbtwnxr  10364  flhalf  10409  fldiv4p1lem1div2  10412  seq3split  10597  seq3f1olemqsumk  10621  seqf1oglem1  10628  seqf1oglem2  10629  bernneq3  10771  facwordi  10849  faclbnd  10850  expcnvap0  11684  cvgratnnlemfm  11711  cvgratnnlemrate  11712  cvgratz  11714  mertenslemi1  11717  fprodntrivap  11766  divalglemnqt  12102  nonsq  12400  eulerthlema  12423  pcfac  12544  1arith  12561  ennnfonelemkh  12654  tgioo  14874  suplociccreex  14944  hoverb  14968  reeff1olem  15091  lgsvalmod  15344  gausslemma2dlem3  15388  lgsquadlem2  15403