Theorem peano2re 8425

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2205  (class class class)co 6058  ℝcr 8142  1c1 8144   + caddc 8146

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

This theorem is referenced by:  lep1  9136  letrp1  9139  p1le  9140  ledivp1  9194  nnssre  9258  nn1suc  9273  nnge1  9277  div4p1lem1div2  9509  zltp1le  9649  suprzclex  9694  zeo  9701  peano2uz2  9703  uzind  9707  btwnapz  9726  numltc  9752  ge0p1rp  10036  fznatpl1  10432  ubmelm1fzo  10593  infssuzex  10615  qbtwnxr  10641  flhalf  10686  fldiv4p1lem1div2  10689  seq3split  10874  seq3f1olemqsumk  10898  seqf1oglem1  10905  seqf1oglem2  10906  bernneq3  11049  facwordi  11127  faclbnd  11128  expcnvap0  12213  cvgratnnlemfm  12240  cvgratnnlemrate  12241  cvgratz  12243  mertenslemi1  12246  fprodntrivap  12295  divalglemnqt  12631  nonsq  12929  eulerthlema  12952  pcfac  13073  1arith  13090  ennnfonelemkh  13247  tgioo  15545  suplociccreex  15615  hoverb  15639  reeff1olem  15762  lgsvalmod  16018  gausslemma2dlem3  16062  lgsquadlem2  16077  eupth2lemsfi  16599