Theorem peano2re 11412

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11239	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11216	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 690	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2099  (class class class)co 7415  ℝcr 11132  1c1 11134   + caddc 11136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-i2m1 11201  ax-1ne0 11202  ax-rrecex 11205  ax-cnre 11206

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5144  df-iota 6495  df-fv 6551  df-ov 7418

This theorem is referenced by:  lep1  12080  letrp1  12083  p1le  12084  ledivp1  12141  sup2  12195  nnssre  12241  nnge1  12265  div4p1lem1div2  12492  zltp1le  12637  suprzcl  12667  zeo  12673  peano2uz2  12675  uzind  12679  numltc  12728  uzwo  12920  ge0p1rp  13032  qbtwnxr  13206  xrsupsslem  13313  supxrunb1  13325  fznatpl1  13582  fzp1disj  13587  fzneuz  13609  fzp1nel  13612  ubmelm1fzo  13755  fllep1  13793  flflp1  13799  flhalf  13822  ltdifltdiv  13826  fldiv4p1lem1div2  13827  dfceil2  13831  ceim1l  13839  uzsup  13855  modltm1p1mod  13915  addmodlteq  13938  fsequb  13967  seqf1olem1  14033  seqf1olem2  14034  bernneq3  14220  expnbnd  14221  expmulnbnd  14224  discr1  14228  discr  14229  facwordi  14275  faclbnd  14276  hashfun  14423  seqcoll2  14453  rexuzre  15326  caubnd  15332  rlim2lt  15468  lo1bddrp  15496  rlimo1  15588  o1rlimmul  15590  o1fsum  15786  harmonic  15832  expcnv  15837  geomulcvg  15849  mertenslem1  15857  bpoly4  16030  nonsq  16725  eulerthlem2  16745  pcprendvds  16803  pcmpt  16855  pcfac  16862  vdwlem6  16949  vdwlem11  16954  chfacffsupp  22752  chfacfscmul0  22754  chfacfpmmul0  22758  tgioo  24706  zcld  24723  iocopnst  24858  cnheibor  24875  bndth  24878  cncmet  25244  pjthlem1  25359  ovolicc2lem3  25442  ovolicopnf  25447  ioorcl2  25495  dyadf  25514  dyadovol  25516  dyadss  25517  dyaddisjlem  25518  dyadmaxlem  25520  opnmbllem  25524  volsup2  25528  vitalilem2  25532  itg2const2  25665  itg2cnlem1  25685  dvfsumle  25948  dvfsumleOLD  25949  dvfsumabs  25951  dvfsumlem1  25954  dvfsumlem3  25957  dvfsumrlim  25960  fta1glem2  26097  fta1lem  26236  aalioulem3  26263  ulmbdd  26328  itgulm  26338  psercnlem1  26356  abelthlem2  26363  abelthlem7  26369  reeff1olem  26377  logtayl  26588  loglesqrt  26687  atanlogsublem  26841  leibpi  26868  efrlim  26895  efrlimOLD  26896  harmonicubnd  26936  fsumharmonic  26938  ftalem5  27003  basellem2  27008  basellem3  27009  chtnprm  27080  chpp1  27081  ppip1le  27087  ppiub  27131  logfaclbnd  27149  logfacrlim  27151  perfectlem2  27157  bcmono  27204  lgsvalmod  27243  gausslemma2dlem3  27295  lgseisen  27306  lgsquadlem1  27307  lgsquadlem2  27308  chebbnd1lem2  27397  chtppilimlem1  27400  rplogsumlem2  27412  dchrisumlema  27415  dchrisumlem1  27416  dchrisumlem3  27418  dchrisum0lem1  27443  chpdifbndlem1  27480  logdivbnd  27483  pntrmax  27491  pntrsumo1  27492  pntpbnd1a  27512  pntpbnd1  27513  pntpbnd2  27514  pntibndlem2  27518  pntlemg  27525  pntlemr  27529  pntlemj  27530  pntlemk  27533  ostth2lem1  27545  qabvle  27552  ostth2lem3  27562  ostth2lem4  27563  axlowdimlem16  28762  wwlksnredwwlkn  29700  wwlksnextproplem3  29716  wwlksext2clwwlk  29861  wwlksubclwwlk  29862  eupth2lems  30042  smcnlem  30501  minvecolem4  30684  pjhthlem1  31195  zltp1ne  34714  cvmliftlem7  34896  dnibndlem13  35960  knoppndvlem19  36000  knoppndvlem21  36002  icoreunrn  36833  relowlssretop  36837  ltflcei  37076  poimirlem1  37089  poimirlem2  37090  poimirlem4  37092  poimirlem6  37094  poimirlem7  37095  poimirlem8  37096  opnmbllem0  37124  mblfinlem1  37125  mblfinlem2  37126  mblfinlem4  37128  itg2addnclem2  37140  itg2addnclem3  37141  incsequz  37216  isbnd3  37252  rrntotbnd  37304  sn-sup2  42015  3cubeslem1  42095  3cubeslem2  42096  irrapxlem4  42236  pellexlem5  42244  pell14qrgapw  42287  pellfundgt1  42294  jm3.1lem2  42430  expdiophlem1  42433  fzuntgd  42879  zltlesub  44658  suplesup  44712  supxrunb3  44772  xrpnf  44859  fmul01lt1lem1  44963  limsupre3lem  45111  xlimxrre  45210  xlimpnfv  45217  ioodvbdlimc1lem1  45310  dvnxpaek  45321  dvnmul  45322  fourierdlem4  45490  fourierdlem11  45497  fourierdlem25  45511  fourierdlem50  45535  fourierdlem64  45549  fourierdlem65  45550  fourierdlem77  45562  fourierdlem79  45564  iinhoiicclem  46052  smfresal  46167  natglobalincr  46254  fmtno4prmfac  46903  lighneallem4a  46939  evenltle  47048  perfectALTVlem2  47053  logbpw2m1  47631