Theorem peano2re 8305

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6013  ℝcr 8021  1c1 8023   + caddc 8025

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

This theorem is referenced by:  lep1  9015  letrp1  9018  p1le  9019  ledivp1  9073  nnssre  9137  nn1suc  9152  nnge1  9156  div4p1lem1div2  9388  zltp1le  9524  suprzclex  9568  zeo  9575  peano2uz2  9577  uzind  9581  btwnapz  9600  numltc  9626  ge0p1rp  9910  fznatpl1  10301  ubmelm1fzo  10461  infssuzex  10483  qbtwnxr  10507  flhalf  10552  fldiv4p1lem1div2  10555  seq3split  10740  seq3f1olemqsumk  10764  seqf1oglem1  10771  seqf1oglem2  10772  bernneq3  10914  facwordi  10992  faclbnd  10993  expcnvap0  12053  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratz  12083  mertenslemi1  12086  fprodntrivap  12135  divalglemnqt  12471  nonsq  12769  eulerthlema  12792  pcfac  12913  1arith  12930  ennnfonelemkh  13023  tgioo  15268  suplociccreex  15338  hoverb  15362  reeff1olem  15485  lgsvalmod  15738  gausslemma2dlem3  15782  lgsquadlem2  15797