Theorem peano2re 8278

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6000  ℝcr 7994  1c1 7996   + caddc 7998

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

This theorem is referenced by:  lep1  8988  letrp1  8991  p1le  8992  ledivp1  9046  nnssre  9110  nn1suc  9125  nnge1  9129  div4p1lem1div2  9361  zltp1le  9497  suprzclex  9541  zeo  9548  peano2uz2  9550  uzind  9554  btwnapz  9573  numltc  9599  ge0p1rp  9877  fznatpl1  10268  ubmelm1fzo  10427  infssuzex  10448  qbtwnxr  10472  flhalf  10517  fldiv4p1lem1div2  10520  seq3split  10705  seq3f1olemqsumk  10729  seqf1oglem1  10736  seqf1oglem2  10737  bernneq3  10879  facwordi  10957  faclbnd  10958  expcnvap0  12008  cvgratnnlemfm  12035  cvgratnnlemrate  12036  cvgratz  12038  mertenslemi1  12041  fprodntrivap  12090  divalglemnqt  12426  nonsq  12724  eulerthlema  12747  pcfac  12868  1arith  12885  ennnfonelemkh  12978  tgioo  15222  suplociccreex  15292  hoverb  15316  reeff1olem  15439  lgsvalmod  15692  gausslemma2dlem3  15736  lgsquadlem2  15751