Theorem peano2re 8463

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 8325	. 2 ⊢ 1 ∈ ℝ
2		readdcl 8305	. 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 8178  1c1 8180   + caddc 8182

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

This theorem is used by:  lep1  9177  letrp1  9180  p1le  9181  ledivp1  9235  nnssre  9310  nn1suc  9325  nnge1  9329  div4p1lem1div2  9563  zltp1le  9703  suprzclex  9748  zeo  9755  peano2uz2  9757  uzind  9761  btwnapz  9780  numltc  9811  ge0p1rp  10096  fznatpl1  10493  ubmelm1fzo  10654  infssuzex  10676  qbtwnxr  10702  flhalf  10750  fldiv4p1lem1div2  10753  seq3split  10938  seq3f1olemqsumk  10962  seqf1oglem1  10969  seqf1oglem2  10970  bernneq3  11113  facwordi  11192  faclbnd  11193  expcnvap0  12285  cvgratnnlemfm  12312  cvgratnnlemrate  12313  cvgratz  12315  mertenslemi1  12318  fprodntrivap  12367  divalglemnqt  12703  nonsq  13003  eulerthlema  13028  pcfac  13149  1arith  13166  ennnfonelemkh  13352  tgioo  15704  suplociccreex  15774  hoverb  15798  reeff1olem  15921  ppiqltx  16183  ppiqub  16194  bcmono  16202  lgsvalmod  16236  gausslemma2dlem3  16280  lgsquadlem2  16295  eupth2lemsfi  16817