Theorem peano2re 8228

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2177  (class class class)co 5957  ℝcr 7944  1c1 7946   + caddc 7948

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

This theorem is referenced by:  lep1  8938  letrp1  8941  p1le  8942  ledivp1  8996  nnssre  9060  nn1suc  9075  nnge1  9079  div4p1lem1div2  9311  zltp1le  9447  suprzclex  9491  zeo  9498  peano2uz2  9500  uzind  9504  btwnapz  9523  numltc  9549  ge0p1rp  9827  fznatpl1  10218  ubmelm1fzo  10377  infssuzex  10398  qbtwnxr  10422  flhalf  10467  fldiv4p1lem1div2  10470  seq3split  10655  seq3f1olemqsumk  10679  seqf1oglem1  10686  seqf1oglem2  10687  bernneq3  10829  facwordi  10907  faclbnd  10908  expcnvap0  11888  cvgratnnlemfm  11915  cvgratnnlemrate  11916  cvgratz  11918  mertenslemi1  11921  fprodntrivap  11970  divalglemnqt  12306  nonsq  12604  eulerthlema  12627  pcfac  12748  1arith  12765  ennnfonelemkh  12858  tgioo  15101  suplociccreex  15171  hoverb  15195  reeff1olem  15318  lgsvalmod  15571  gausslemma2dlem3  15615  lgsquadlem2  15630