Theorem peano2re 11408

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11233	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11208	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 704	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7414  ℝcr 11124  1c1 11126   + caddc 11128

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-i2m1 11193  ax-1ne0 11194  ax-rrecex 11197  ax-cnre 11198

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417

This theorem is used by:  lep1  12081  letrp1  12084  p1le  12085  ledivp1  12142  sup2  12196  nnssre  12262  nnge1  12289  div4p1lem1div2  12524  zltp1le  12669  suprzcl  12702  zeo  12708  peano2uz2  12710  uzind  12714  numltc  12768  uzwo  12961  ge0p1rp  13076  qbtwnxr  13253  xrsupsslem  13360  supxrunb1  13372  fznatpl1  13634  fzp1disj  13639  fzneuz  13664  fzp1nel  13667  ubmelm1fzo  13820  fllep1  13863  flflp1  13869  flhalf  13892  ltdifltdiv  13896  fldiv4p1lem1div2  13897  dfceil2  13901  ceim1l  13909  uzsup  13925  modltm1p1mod  13988  addmodlteq  14011  fsequb  14040  seqf1olem1  14106  seqf1olem2  14107  bernneq3  14296  expnbnd  14297  expmulnbnd  14300  discr1  14304  discr  14305  facwordi  14354  faclbnd  14355  hashfun  14503  seqcoll2  14531  rexuzre  15441  caubnd  15447  rlim2lt  15585  lo1bddrp  15613  rlimo1  15705  o1rlimmul  15707  o1fsum  15901  harmonic  15949  expcnv  15954  geomulcvg  15966  mertenslem1  15974  bpoly4  16146  nonsq  16851  eulerthlem2  16874  pcprendvds  16933  pcmpt  16985  pcfac  16992  vdwlem6  17079  vdwlem11  17084  chnccat  18715  chfacffsupp  23082  chfacfscmul0  23084  chfacfpmmul0  23088  tgioo  25023  zcld  25041  iocopnst  25169  cnheibor  25184  bndth  25187  cncmet  25551  pjthlem1  25666  ovolicc2lem3  25748  ovolicopnf  25753  ioorcl2  25801  dyadf  25820  dyadovol  25822  dyadss  25823  dyaddisjlem  25824  dyadmaxlem  25826  opnmbllem  25830  volsup2  25834  vitalilem2  25838  itg2const2  25970  itg2cnlem1  25990  dvfsumle  26249  dvfsumabs  26251  dvfsumlem1  26254  dvfsumlem3  26256  dvfsumrlim  26259  fta1glem2  26395  fta1lem  26538  aalioulem3  26571  ulmbdd  26635  itgulm  26645  psercnlem1  26662  abelthlem2  26669  abelthlem7  26675  reeff1olem  26683  logtayl  26898  loglesqrt  26999  atanlogsublem  27153  leibpi  27180  efrlim  27207  harmonicubnd  27247  fsumharmonic  27249  ftalem5  27314  basellem2  27319  basellem3  27320  chtnprm  27391  chpp1  27392  ppip1le  27398  ppiub  27441  logfaclbnd  27459  logfacrlim  27461  perfectlem2  27467  bcmono  27514  lgsvalmod  27553  gausslemma2dlem3  27605  lgseisen  27616  lgsquadlem1  27617  lgsquadlem2  27618  chebbnd1lem2  27707  chtppilimlem1  27710  rplogsumlem2  27722  dchrisumlema  27725  dchrisumlem1  27726  dchrisumlem3  27728  dchrisum0lem1  27753  chpdifbndlem1  27790  logdivbnd  27793  pntrmax  27801  pntrsumo1  27802  pntpbnd1a  27822  pntpbnd1  27823  pntpbnd2  27824  pntibndlem2  27828  pntlemg  27835  pntlemr  27839  pntlemj  27840  pntlemk  27843  ostth2lem1  27855  qabvle  27862  ostth2lem3  27872  ostth2lem4  27873  axlowdimlem16  29415  wwlksnredwwlkn  30364  wwlksnextproplem3  30380  wwlksext2clwwlk  30528  wwlksubclwwlk  30529  eupth2lems  30719  smcnlem  31179  minvecolem4  31362  pjhthlem1  31873  zltp1ne  35715  cvmliftlem7  35871  dnibndlem13  37188  knoppndvlem19  37228  knoppndvlem21  37230  icoreunrn  38114  relowlssretop  38118  ltflcei  38363  poimirlem1  38371  poimirlem2  38372  poimirlem4  38374  poimirlem6  38376  poimirlem7  38377  poimirlem8  38378  opnmbllem0  38406  mblfinlem1  38407  mblfinlem2  38408  mblfinlem4  38410  itg2addnclem2  38422  itg2addnclem3  38423  incsequz  38499  isbnd3  38535  rrntotbnd  38587  sn-sup2  43380  3cubeslem1  43530  3cubeslem2  43531  irrapxlem4  43667  pellexlem5  43675  pell14qrgapw  43718  pellfundgt1  43725  jm3.1lem2  43860  expdiophlem1  43863  fzuntgd  44299  zltlesub  46119  suplesup  46170  supxrunb3  46229  xrpnf  46314  fmul01lt1lem1  46415  limsupre3lem  46561  xlimxrre  46660  xlimpnfv  46667  ioodvbdlimc1lem1  46760  dvnxpaek  46771  dvnmul  46772  fourierdlem4  46940  fourierdlem11  46947  fourierdlem25  46961  fourierdlem50  46985  fourierdlem64  46999  fourierdlem65  47000  fourierdlem77  47012  fourierdlem79  47014  iinhoiicclem  47502  smfresal  47617  fmtno4prmfac  48476  lighneallem4a  48512  evenltle  48634  perfectALTVlem2  48639  logbpw2m1  49498