Theorem peano2re 7715

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 7584	. 2 ⊢ 1 ∈ ℝ
2		readdcl 7565	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 417	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1445  (class class class)co 5690  ℝcr 7446  1c1 7448   + caddc 7450

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

This theorem is referenced by:  lep1  8403  letrp1  8406  p1le  8407  ledivp1  8461  nnssre  8524  nn1suc  8539  nnge1  8543  div4p1lem1div2  8767  zltp1le  8902  suprzclex  8943  zeo  8950  peano2uz2  8952  uzind  8956  btwnapz  8975  numltc  9001  ge0p1rp  9264  fznatpl1  9639  ubmelm1fzo  9786  qbtwnxr  9818  flhalf  9858  fldiv4p1lem1div2  9861  seq3split  10045  seq3f1olemqsumk  10065  bernneq3  10207  facwordi  10279  faclbnd  10280  expcnvap0  11061  cvgratnnlemfm  11088  cvgratnnlemrate  11089  cvgratz  11091  mertenslemi1  11094  divalglemnqt  11363  infssuzex  11388  nonsq  11628  tgioo  12336