Theorem peano2re 8315

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6018  ℝcr 8031  1c1 8033   + caddc 8035

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

This theorem is referenced by:  lep1  9025  letrp1  9028  p1le  9029  ledivp1  9083  nnssre  9147  nn1suc  9162  nnge1  9166  div4p1lem1div2  9398  zltp1le  9534  suprzclex  9578  zeo  9585  peano2uz2  9587  uzind  9591  btwnapz  9610  numltc  9636  ge0p1rp  9920  fznatpl1  10311  ubmelm1fzo  10472  infssuzex  10494  qbtwnxr  10518  flhalf  10563  fldiv4p1lem1div2  10566  seq3split  10751  seq3f1olemqsumk  10775  seqf1oglem1  10782  seqf1oglem2  10783  bernneq3  10925  facwordi  11003  faclbnd  11004  expcnvap0  12068  cvgratnnlemfm  12095  cvgratnnlemrate  12096  cvgratz  12098  mertenslemi1  12101  fprodntrivap  12150  divalglemnqt  12486  nonsq  12784  eulerthlema  12807  pcfac  12928  1arith  12945  ennnfonelemkh  13038  tgioo  15284  suplociccreex  15354  hoverb  15378  reeff1olem  15501  lgsvalmod  15754  gausslemma2dlem3  15798  lgsquadlem2  15813  eupth2lemsfi  16335