Theorem peano2re 8317

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2201  (class class class)co 6020  ℝcr 8033  1c1 8035   + caddc 8037

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

This theorem is referenced by:  lep1  9027  letrp1  9030  p1le  9031  ledivp1  9085  nnssre  9149  nn1suc  9164  nnge1  9168  div4p1lem1div2  9400  zltp1le  9536  suprzclex  9580  zeo  9587  peano2uz2  9589  uzind  9593  btwnapz  9612  numltc  9638  ge0p1rp  9922  fznatpl1  10313  ubmelm1fzo  10474  infssuzex  10496  qbtwnxr  10520  flhalf  10565  fldiv4p1lem1div2  10568  seq3split  10753  seq3f1olemqsumk  10777  seqf1oglem1  10784  seqf1oglem2  10785  bernneq3  10927  facwordi  11005  faclbnd  11006  expcnvap0  12083  cvgratnnlemfm  12110  cvgratnnlemrate  12111  cvgratz  12113  mertenslemi1  12116  fprodntrivap  12165  divalglemnqt  12501  nonsq  12799  eulerthlema  12822  pcfac  12943  1arith  12960  ennnfonelemkh  13053  tgioo  15304  suplociccreex  15374  hoverb  15398  reeff1olem  15521  lgsvalmod  15774  gausslemma2dlem3  15818  lgsquadlem2  15833  eupth2lemsfi  16355