Theorem peano2re 8095

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

Assertion

Ref	Expression
peano2re	⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 7958	. 2 ⊢ 1 ∈ ℝ
2		readdcl 7939	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 425	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2148  (class class class)co 5877  ℝcr 7812  1c1 7814   + caddc 7816

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

This theorem is referenced by:  lep1  8804  letrp1  8807  p1le  8808  ledivp1  8862  nnssre  8925  nn1suc  8940  nnge1  8944  div4p1lem1div2  9174  zltp1le  9309  suprzclex  9353  zeo  9360  peano2uz2  9362  uzind  9366  btwnapz  9385  numltc  9411  ge0p1rp  9687  fznatpl1  10078  ubmelm1fzo  10228  qbtwnxr  10260  flhalf  10304  fldiv4p1lem1div2  10307  seq3split  10481  seq3f1olemqsumk  10501  bernneq3  10645  facwordi  10722  faclbnd  10723  expcnvap0  11512  cvgratnnlemfm  11539  cvgratnnlemrate  11540  cvgratz  11542  mertenslemi1  11545  fprodntrivap  11594  divalglemnqt  11927  infssuzex  11952  nonsq  12209  eulerthlema  12232  pcfac  12350  1arith  12367  ennnfonelemkh  12415  tgioo  14085  suplociccreex  14141  reeff1olem  14231  lgsvalmod  14459