Theorem peano2re 11417

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11244	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11221	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 691	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7414  ℝcr 11137  1c1 11139   + caddc 11141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-i2m1 11206  ax-1ne0 11207  ax-rrecex 11210  ax-cnre 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-iota 6495  df-fv 6550  df-ov 7417

This theorem is referenced by:  lep1  12091  letrp1  12094  p1le  12095  ledivp1  12153  sup2  12207  nnssre  12253  nnge1  12277  div4p1lem1div2  12505  zltp1le  12651  suprzcl  12682  zeo  12688  peano2uz2  12690  uzind  12694  numltc  12743  uzwo  12936  ge0p1rp  13049  qbtwnxr  13225  xrsupsslem  13332  supxrunb1  13344  fznatpl1  13601  fzp1disj  13606  fzneuz  13631  fzp1nel  13634  ubmelm1fzo  13785  fllep1  13824  flflp1  13830  flhalf  13853  ltdifltdiv  13857  fldiv4p1lem1div2  13858  dfceil2  13862  ceim1l  13870  uzsup  13886  modltm1p1mod  13947  addmodlteq  13970  fsequb  13999  seqf1olem1  14065  seqf1olem2  14066  bernneq3  14253  expnbnd  14254  expmulnbnd  14257  discr1  14261  discr  14262  facwordi  14311  faclbnd  14312  hashfun  14459  seqcoll2  14487  rexuzre  15374  caubnd  15380  rlim2lt  15516  lo1bddrp  15544  rlimo1  15636  o1rlimmul  15638  o1fsum  15832  harmonic  15878  expcnv  15883  geomulcvg  15895  mertenslem1  15903  bpoly4  16078  nonsq  16779  eulerthlem2  16802  pcprendvds  16861  pcmpt  16913  pcfac  16920  vdwlem6  17007  vdwlem11  17012  chfacffsupp  22829  chfacfscmul0  22831  chfacfpmmul0  22835  tgioo  24772  zcld  24790  iocopnst  24925  cnheibor  24942  bndth  24945  cncmet  25311  pjthlem1  25426  ovolicc2lem3  25509  ovolicopnf  25514  ioorcl2  25562  dyadf  25581  dyadovol  25583  dyadss  25584  dyaddisjlem  25585  dyadmaxlem  25587  opnmbllem  25591  volsup2  25595  vitalilem2  25599  itg2const2  25731  itg2cnlem1  25751  dvfsumle  26015  dvfsumleOLD  26016  dvfsumabs  26018  dvfsumlem1  26021  dvfsumlem3  26024  dvfsumrlim  26027  fta1glem2  26163  fta1lem  26304  aalioulem3  26331  ulmbdd  26396  itgulm  26406  psercnlem1  26424  abelthlem2  26431  abelthlem7  26437  reeff1olem  26445  logtayl  26657  loglesqrt  26759  atanlogsublem  26913  leibpi  26940  efrlim  26967  efrlimOLD  26968  harmonicubnd  27008  fsumharmonic  27010  ftalem5  27075  basellem2  27080  basellem3  27081  chtnprm  27152  chpp1  27153  ppip1le  27159  ppiub  27203  logfaclbnd  27221  logfacrlim  27223  perfectlem2  27229  bcmono  27276  lgsvalmod  27315  gausslemma2dlem3  27367  lgseisen  27378  lgsquadlem1  27379  lgsquadlem2  27380  chebbnd1lem2  27469  chtppilimlem1  27472  rplogsumlem2  27484  dchrisumlema  27487  dchrisumlem1  27488  dchrisumlem3  27490  dchrisum0lem1  27515  chpdifbndlem1  27552  logdivbnd  27555  pntrmax  27563  pntrsumo1  27564  pntpbnd1a  27584  pntpbnd1  27585  pntpbnd2  27586  pntibndlem2  27590  pntlemg  27597  pntlemr  27601  pntlemj  27602  pntlemk  27605  ostth2lem1  27617  qabvle  27624  ostth2lem3  27634  ostth2lem4  27635  axlowdimlem16  28921  wwlksnredwwlkn  29862  wwlksnextproplem3  29878  wwlksext2clwwlk  30023  wwlksubclwwlk  30024  eupth2lems  30204  smcnlem  30663  minvecolem4  30846  pjhthlem1  31357  zltp1ne  35056  cvmliftlem7  35237  dnibndlem13  36432  knoppndvlem19  36472  knoppndvlem21  36474  icoreunrn  37301  relowlssretop  37305  ltflcei  37556  poimirlem1  37569  poimirlem2  37570  poimirlem4  37572  poimirlem6  37574  poimirlem7  37575  poimirlem8  37576  opnmbllem0  37604  mblfinlem1  37605  mblfinlem2  37606  mblfinlem4  37608  itg2addnclem2  37620  itg2addnclem3  37621  incsequz  37696  isbnd3  37732  rrntotbnd  37784  sn-sup2  42446  3cubeslem1  42640  3cubeslem2  42641  irrapxlem4  42781  pellexlem5  42789  pell14qrgapw  42832  pellfundgt1  42839  jm3.1lem2  42975  expdiophlem1  42978  fzuntgd  43416  zltlesub  45242  suplesup  45295  supxrunb3  45355  xrpnf  45441  fmul01lt1lem1  45544  limsupre3lem  45692  xlimxrre  45791  xlimpnfv  45798  ioodvbdlimc1lem1  45891  dvnxpaek  45902  dvnmul  45903  fourierdlem4  46071  fourierdlem11  46078  fourierdlem25  46092  fourierdlem50  46116  fourierdlem64  46130  fourierdlem65  46131  fourierdlem77  46143  fourierdlem79  46145  iinhoiicclem  46633  smfresal  46748  natglobalincr  46837  fmtno4prmfac  47505  lighneallem4a  47541  evenltle  47650  perfectALTVlem2  47655  logbpw2m1  48434