Theorem peano2re 8314

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6017  ℝcr 8030  1c1 8032   + caddc 8034

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

This theorem is referenced by:  lep1  9024  letrp1  9027  p1le  9028  ledivp1  9082  nnssre  9146  nn1suc  9161  nnge1  9165  div4p1lem1div2  9397  zltp1le  9533  suprzclex  9577  zeo  9584  peano2uz2  9586  uzind  9590  btwnapz  9609  numltc  9635  ge0p1rp  9919  fznatpl1  10310  ubmelm1fzo  10470  infssuzex  10492  qbtwnxr  10516  flhalf  10561  fldiv4p1lem1div2  10564  seq3split  10749  seq3f1olemqsumk  10773  seqf1oglem1  10780  seqf1oglem2  10781  bernneq3  10923  facwordi  11001  faclbnd  11002  expcnvap0  12062  cvgratnnlemfm  12089  cvgratnnlemrate  12090  cvgratz  12092  mertenslemi1  12095  fprodntrivap  12144  divalglemnqt  12480  nonsq  12778  eulerthlema  12801  pcfac  12922  1arith  12939  ennnfonelemkh  13032  tgioo  15277  suplociccreex  15347  hoverb  15371  reeff1olem  15494  lgsvalmod  15747  gausslemma2dlem3  15791  lgsquadlem2  15806