Theorem peano2re 8469

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

Assertion

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

Proof of Theorem peano2re

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  (class class class)co 6088  ℝcr 8184  1c1 8186   + caddc 8188

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

This theorem is used by:  lep1  9183  letrp1  9186  p1le  9187  ledivp1  9241  nnssre  9317  nn1suc  9332  nnge1  9336  div4p1lem1div2  9570  zltp1le  9708  suprzclex  9754  zeo  9761  peano2uz2  9763  uzind  9767  btwnapz  9786  numltc  9817  ge0p1rp  10102  fznatpl1  10499  ubmelm1fzo  10660  infssuzex  10682  qbtwnxr  10708  flaplt  10738  flhalf  10757  fldiv4p1lem1div2  10760  seq3split  10945  seq3f1olemqsumk  10969  seqf1oglem1  10976  seqf1oglem2  10977  bernneq3  11120  facwordi  11199  faclbnd  11200  expcnvap0  12293  cvgratnnlemfm  12320  cvgratnnlemrate  12321  cvgratz  12323  mertenslemi1  12326  fprodntrivap  12375  divalglemnqt  12711  nonsq  13011  eulerthlema  13036  pcfac  13157  1arith  13174  ennnfonelemkh  13360  tgioo  15797  suplociccreex  15867  hoverb  15891  reeff1olem  16014  ppiqltx  16298  ppiqub  16310  bcmono  16321  lgsvalmod  16360  gausslemma2dlem3  16404  lgsquadlem2  16419  eupth2lemsfi  16941