Theorem peano2re 8155

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

Assertion

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

Proof of Theorem peano2re

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

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

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

This theorem is referenced by:  lep1  8864  letrp1  8867  p1le  8868  ledivp1  8922  nnssre  8986  nn1suc  9001  nnge1  9005  div4p1lem1div2  9236  zltp1le  9371  suprzclex  9415  zeo  9422  peano2uz2  9424  uzind  9428  btwnapz  9447  numltc  9473  ge0p1rp  9751  fznatpl1  10142  ubmelm1fzo  10293  qbtwnxr  10326  flhalf  10371  fldiv4p1lem1div2  10374  seq3split  10559  seq3f1olemqsumk  10583  seqf1oglem1  10590  seqf1oglem2  10591  bernneq3  10733  facwordi  10811  faclbnd  10812  expcnvap0  11645  cvgratnnlemfm  11672  cvgratnnlemrate  11673  cvgratz  11675  mertenslemi1  11678  fprodntrivap  11727  divalglemnqt  12061  infssuzex  12086  nonsq  12345  eulerthlema  12368  pcfac  12488  1arith  12505  ennnfonelemkh  12569  tgioo  14714  suplociccreex  14778  hoverb  14802  reeff1olem  14906  lgsvalmod  15135  gausslemma2dlem3  15179