Theorem peano2re 8092

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2148  (class class class)co 5874  ℝcr 7809  1c1 7811   + caddc 7813

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

This theorem is referenced by:  lep1  8801  letrp1  8804  p1le  8805  ledivp1  8859  nnssre  8922  nn1suc  8937  nnge1  8941  div4p1lem1div2  9171  zltp1le  9306  suprzclex  9350  zeo  9357  peano2uz2  9359  uzind  9363  btwnapz  9382  numltc  9408  ge0p1rp  9684  fznatpl1  10075  ubmelm1fzo  10225  qbtwnxr  10257  flhalf  10301  fldiv4p1lem1div2  10304  seq3split  10478  seq3f1olemqsumk  10498  bernneq3  10642  facwordi  10719  faclbnd  10720  expcnvap0  11509  cvgratnnlemfm  11536  cvgratnnlemrate  11537  cvgratz  11539  mertenslemi1  11542  fprodntrivap  11591  divalglemnqt  11924  infssuzex  11949  nonsq  12206  eulerthlema  12229  pcfac  12347  1arith  12364  ennnfonelemkh  12412  tgioo  13982  suplociccreex  14038  reeff1olem  14128  lgsvalmod  14356