Theorem peano2re 8157

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2164  (class class class)co 5919  ℝcr 7873  1c1 7875   + caddc 7877

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

This theorem is referenced by:  lep1  8866  letrp1  8869  p1le  8870  ledivp1  8924  nnssre  8988  nn1suc  9003  nnge1  9007  div4p1lem1div2  9239  zltp1le  9374  suprzclex  9418  zeo  9425  peano2uz2  9427  uzind  9431  btwnapz  9450  numltc  9476  ge0p1rp  9754  fznatpl1  10145  ubmelm1fzo  10296  qbtwnxr  10329  flhalf  10374  fldiv4p1lem1div2  10377  seq3split  10562  seq3f1olemqsumk  10586  seqf1oglem1  10593  seqf1oglem2  10594  bernneq3  10736  facwordi  10814  faclbnd  10815  expcnvap0  11648  cvgratnnlemfm  11675  cvgratnnlemrate  11676  cvgratz  11678  mertenslemi1  11681  fprodntrivap  11730  divalglemnqt  12064  infssuzex  12089  nonsq  12348  eulerthlema  12371  pcfac  12491  1arith  12508  ennnfonelemkh  12572  tgioo  14733  suplociccreex  14803  hoverb  14827  reeff1olem  14947  lgsvalmod  15176  gausslemma2dlem3  15220  lgsquadlem2  15235