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  11784  cvgratnnlemfm  11811  cvgratnnlemrate  11812  cvgratz  11814  mertenslemi1  11817  fprodntrivap  11866  divalglemnqt  12202  nonsq  12500  eulerthlema  12523  pcfac  12644  1arith  12661  ennnfonelemkh  12754  tgioo  14997  suplociccreex  15067  hoverb  15091  reeff1olem  15214  lgsvalmod  15467  gausslemma2dlem3  15511  lgsquadlem2  15526