Theorem peano2re 8181

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2167  (class class class)co 5925  ℝcr 7897  1c1 7899   + caddc 7901

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

This theorem is referenced by:  lep1  8891  letrp1  8894  p1le  8895  ledivp1  8949  nnssre  9013  nn1suc  9028  nnge1  9032  div4p1lem1div2  9264  zltp1le  9399  suprzclex  9443  zeo  9450  peano2uz2  9452  uzind  9456  btwnapz  9475  numltc  9501  ge0p1rp  9779  fznatpl1  10170  ubmelm1fzo  10321  infssuzex  10342  qbtwnxr  10366  flhalf  10411  fldiv4p1lem1div2  10414  seq3split  10599  seq3f1olemqsumk  10623  seqf1oglem1  10630  seqf1oglem2  10631  bernneq3  10773  facwordi  10851  faclbnd  10852  expcnvap0  11686  cvgratnnlemfm  11713  cvgratnnlemrate  11714  cvgratz  11716  mertenslemi1  11719  fprodntrivap  11768  divalglemnqt  12104  nonsq  12402  eulerthlema  12425  pcfac  12546  1arith  12563  ennnfonelemkh  12656  tgioo  14898  suplociccreex  14968  hoverb  14992  reeff1olem  15115  lgsvalmod  15368  gausslemma2dlem3  15412  lgsquadlem2  15427