Theorem peano2re 8034

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 7898	. 2 ⊢ 1 ∈ ℝ
2		readdcl 7879	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 422	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2136  (class class class)co 5842  ℝcr 7752  1c1 7754   + caddc 7756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-1re 7847  ax-addrcl 7850

This theorem is referenced by:  lep1  8740  letrp1  8743  p1le  8744  ledivp1  8798  nnssre  8861  nn1suc  8876  nnge1  8880  div4p1lem1div2  9110  zltp1le  9245  suprzclex  9289  zeo  9296  peano2uz2  9298  uzind  9302  btwnapz  9321  numltc  9347  ge0p1rp  9621  fznatpl1  10011  ubmelm1fzo  10161  qbtwnxr  10193  flhalf  10237  fldiv4p1lem1div2  10240  seq3split  10414  seq3f1olemqsumk  10434  bernneq3  10577  facwordi  10653  faclbnd  10654  expcnvap0  11443  cvgratnnlemfm  11470  cvgratnnlemrate  11471  cvgratz  11473  mertenslemi1  11476  fprodntrivap  11525  divalglemnqt  11857  infssuzex  11882  nonsq  12139  eulerthlema  12162  pcfac  12280  1arith  12297  ennnfonelemkh  12345  tgioo  13186  suplociccreex  13242  reeff1olem  13332  lgsvalmod  13560