Theorem peano2re 8055

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 7919	. 2 ⊢ 1 ∈ ℝ
2		readdcl 7900	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 423	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2141  (class class class)co 5853  ℝcr 7773  1c1 7775   + caddc 7777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-1re 7868  ax-addrcl 7871

This theorem is referenced by:  lep1  8761  letrp1  8764  p1le  8765  ledivp1  8819  nnssre  8882  nn1suc  8897  nnge1  8901  div4p1lem1div2  9131  zltp1le  9266  suprzclex  9310  zeo  9317  peano2uz2  9319  uzind  9323  btwnapz  9342  numltc  9368  ge0p1rp  9642  fznatpl1  10032  ubmelm1fzo  10182  qbtwnxr  10214  flhalf  10258  fldiv4p1lem1div2  10261  seq3split  10435  seq3f1olemqsumk  10455  bernneq3  10598  facwordi  10674  faclbnd  10675  expcnvap0  11465  cvgratnnlemfm  11492  cvgratnnlemrate  11493  cvgratz  11495  mertenslemi1  11498  fprodntrivap  11547  divalglemnqt  11879  infssuzex  11904  nonsq  12161  eulerthlema  12184  pcfac  12302  1arith  12319  ennnfonelemkh  12367  tgioo  13340  suplociccreex  13396  reeff1olem  13486  lgsvalmod  13714