Theorem peano2re 8293

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6007  ℝcr 8009  1c1 8011   + caddc 8013

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

This theorem is referenced by:  lep1  9003  letrp1  9006  p1le  9007  ledivp1  9061  nnssre  9125  nn1suc  9140  nnge1  9144  div4p1lem1div2  9376  zltp1le  9512  suprzclex  9556  zeo  9563  peano2uz2  9565  uzind  9569  btwnapz  9588  numltc  9614  ge0p1rp  9893  fznatpl1  10284  ubmelm1fzo  10444  infssuzex  10465  qbtwnxr  10489  flhalf  10534  fldiv4p1lem1div2  10537  seq3split  10722  seq3f1olemqsumk  10746  seqf1oglem1  10753  seqf1oglem2  10754  bernneq3  10896  facwordi  10974  faclbnd  10975  expcnvap0  12028  cvgratnnlemfm  12055  cvgratnnlemrate  12056  cvgratz  12058  mertenslemi1  12061  fprodntrivap  12110  divalglemnqt  12446  nonsq  12744  eulerthlema  12767  pcfac  12888  1arith  12905  ennnfonelemkh  12998  tgioo  15243  suplociccreex  15313  hoverb  15337  reeff1olem  15460  lgsvalmod  15713  gausslemma2dlem3  15757  lgsquadlem2  15772