Theorem peano2re 8207

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2175  (class class class)co 5943  ℝcr 7923  1c1 7925   + caddc 7927

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

This theorem is referenced by:  lep1  8917  letrp1  8920  p1le  8921  ledivp1  8975  nnssre  9039  nn1suc  9054  nnge1  9058  div4p1lem1div2  9290  zltp1le  9426  suprzclex  9470  zeo  9477  peano2uz2  9479  uzind  9483  btwnapz  9502  numltc  9528  ge0p1rp  9806  fznatpl1  10197  ubmelm1fzo  10353  infssuzex  10374  qbtwnxr  10398  flhalf  10443  fldiv4p1lem1div2  10446  seq3split  10631  seq3f1olemqsumk  10655  seqf1oglem1  10662  seqf1oglem2  10663  bernneq3  10805  facwordi  10883  faclbnd  10884  expcnvap0  11755  cvgratnnlemfm  11782  cvgratnnlemrate  11783  cvgratz  11785  mertenslemi1  11788  fprodntrivap  11837  divalglemnqt  12173  nonsq  12471  eulerthlema  12494  pcfac  12615  1arith  12632  ennnfonelemkh  12725  tgioo  14968  suplociccreex  15038  hoverb  15062  reeff1olem  15185  lgsvalmod  15438  gausslemma2dlem3  15482  lgsquadlem2  15497