Theorem peano2re 8357

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6028  ℝcr 8074  1c1 8076   + caddc 8078

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

This theorem is referenced by:  lep1  9067  letrp1  9070  p1le  9071  ledivp1  9125  nnssre  9189  nn1suc  9204  nnge1  9208  div4p1lem1div2  9440  zltp1le  9578  suprzclex  9622  zeo  9629  peano2uz2  9631  uzind  9635  btwnapz  9654  numltc  9680  ge0p1rp  9964  fznatpl1  10356  ubmelm1fzo  10517  infssuzex  10539  qbtwnxr  10563  flhalf  10608  fldiv4p1lem1div2  10611  seq3split  10796  seq3f1olemqsumk  10820  seqf1oglem1  10827  seqf1oglem2  10828  bernneq3  10970  facwordi  11048  faclbnd  11049  expcnvap0  12126  cvgratnnlemfm  12153  cvgratnnlemrate  12154  cvgratz  12156  mertenslemi1  12159  fprodntrivap  12208  divalglemnqt  12544  nonsq  12842  eulerthlema  12865  pcfac  12986  1arith  13003  ennnfonelemkh  13096  tgioo  15348  suplociccreex  15418  hoverb  15442  reeff1olem  15565  lgsvalmod  15821  gausslemma2dlem3  15865  lgsquadlem2  15880  eupth2lemsfi  16402