Theorem peano2re 8162

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2167  (class class class)co 5922  ℝcr 7878  1c1 7880   + caddc 7882

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

This theorem is referenced by:  lep1  8872  letrp1  8875  p1le  8876  ledivp1  8930  nnssre  8994  nn1suc  9009  nnge1  9013  div4p1lem1div2  9245  zltp1le  9380  suprzclex  9424  zeo  9431  peano2uz2  9433  uzind  9437  btwnapz  9456  numltc  9482  ge0p1rp  9760  fznatpl1  10151  ubmelm1fzo  10302  infssuzex  10323  qbtwnxr  10347  flhalf  10392  fldiv4p1lem1div2  10395  seq3split  10580  seq3f1olemqsumk  10604  seqf1oglem1  10611  seqf1oglem2  10612  bernneq3  10754  facwordi  10832  faclbnd  10833  expcnvap0  11667  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratz  11697  mertenslemi1  11700  fprodntrivap  11749  divalglemnqt  12085  nonsq  12375  eulerthlema  12398  pcfac  12519  1arith  12536  ennnfonelemkh  12629  tgioo  14790  suplociccreex  14860  hoverb  14884  reeff1olem  15007  lgsvalmod  15260  gausslemma2dlem3  15304  lgsquadlem2  15319