Theorem peano2re 8464

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 8326	. 2 ⊢ 1 ∈ ℝ
2		readdcl 8306	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 429	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6085  ℝcr 8179  1c1 8181   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-1re 8274  ax-addrcl 8277

This theorem is used by:  lep1  9178  letrp1  9181  p1le  9182  ledivp1  9236  nnssre  9311  nn1suc  9326  nnge1  9330  div4p1lem1div2  9564  zltp1le  9704  suprzclex  9749  zeo  9756  peano2uz2  9758  uzind  9762  btwnapz  9781  numltc  9812  ge0p1rp  10097  fznatpl1  10494  ubmelm1fzo  10655  infssuzex  10677  qbtwnxr  10703  flaplt  10733  flhalf  10752  fldiv4p1lem1div2  10755  seq3split  10940  seq3f1olemqsumk  10964  seqf1oglem1  10971  seqf1oglem2  10972  bernneq3  11115  facwordi  11194  faclbnd  11195  expcnvap0  12288  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratz  12318  mertenslemi1  12321  fprodntrivap  12370  divalglemnqt  12706  nonsq  13006  eulerthlema  13031  pcfac  13152  1arith  13169  ennnfonelemkh  13355  tgioo  15746  suplociccreex  15816  hoverb  15840  reeff1olem  15963  ppiqltx  16242  ppiqub  16254  bcmono  16265  lgsvalmod  16304  gausslemma2dlem3  16348  lgsquadlem2  16363  eupth2lemsfi  16885