Theorem peano2re 11378

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11203	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11178	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 703	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  lep1  12051  letrp1  12054  p1le  12055  ledivp1  12112  sup2  12166  nnssre  12232  nnge1  12259  div4p1lem1div2  12494  zltp1le  12639  suprzcl  12671  zeo  12677  peano2uz2  12679  uzind  12683  numltc  12737  uzwo  12930  ge0p1rp  13044  qbtwnxr  13221  xrsupsslem  13328  supxrunb1  13340  fznatpl1  13602  fzp1disj  13607  fzneuz  13632  fzp1nel  13635  ubmelm1fzo  13788  fllep1  13830  flflp1  13836  flhalf  13859  ltdifltdiv  13863  fldiv4p1lem1div2  13864  dfceil2  13868  ceim1l  13876  uzsup  13892  modltm1p1mod  13955  addmodlteq  13978  fsequb  14007  seqf1olem1  14073  seqf1olem2  14074  bernneq3  14263  expnbnd  14264  expmulnbnd  14267  discr1  14271  discr  14272  facwordi  14321  faclbnd  14322  hashfun  14470  seqcoll2  14498  rexuzre  15400  caubnd  15406  rlim2lt  15544  lo1bddrp  15572  rlimo1  15664  o1rlimmul  15666  o1fsum  15861  harmonic  15909  expcnv  15914  geomulcvg  15926  mertenslem1  15934  bpoly4  16108  nonsq  16813  eulerthlem2  16836  pcprendvds  16895  pcmpt  16947  pcfac  16954  vdwlem6  17041  vdwlem11  17046  chnccat  18677  chfacffsupp  23013  chfacfscmul0  23015  chfacfpmmul0  23019  tgioo  24953  zcld  24971  iocopnst  25099  cnheibor  25114  bndth  25117  cncmet  25481  pjthlem1  25596  ovolicc2lem3  25678  ovolicopnf  25683  ioorcl2  25731  dyadf  25750  dyadovol  25752  dyadss  25753  dyaddisjlem  25754  dyadmaxlem  25756  opnmbllem  25760  volsup2  25764  vitalilem2  25768  itg2const2  25900  itg2cnlem1  25920  dvfsumle  26180  dvfsumabs  26182  dvfsumlem1  26185  dvfsumlem3  26187  dvfsumrlim  26190  fta1glem2  26326  fta1lem  26468  aalioulem3  26497  ulmbdd  26561  itgulm  26571  psercnlem1  26588  abelthlem2  26595  abelthlem7  26601  reeff1olem  26609  logtayl  26825  loglesqrt  26926  atanlogsublem  27080  leibpi  27107  efrlim  27134  harmonicubnd  27174  fsumharmonic  27176  ftalem5  27241  basellem2  27246  basellem3  27247  chtnprm  27318  chpp1  27319  ppip1le  27325  ppiub  27368  logfaclbnd  27386  logfacrlim  27388  perfectlem2  27394  bcmono  27441  lgsvalmod  27480  gausslemma2dlem3  27532  lgseisen  27543  lgsquadlem1  27544  lgsquadlem2  27545  chebbnd1lem2  27634  chtppilimlem1  27637  rplogsumlem2  27649  dchrisumlema  27652  dchrisumlem1  27653  dchrisumlem3  27655  dchrisum0lem1  27680  chpdifbndlem1  27717  logdivbnd  27720  pntrmax  27728  pntrsumo1  27729  pntpbnd1a  27749  pntpbnd1  27750  pntpbnd2  27751  pntibndlem2  27755  pntlemg  27762  pntlemr  27766  pntlemj  27767  pntlemk  27770  ostth2lem1  27782  qabvle  27789  ostth2lem3  27799  ostth2lem4  27800  axlowdimlem16  29307  wwlksnredwwlkn  30244  wwlksnextproplem3  30260  wwlksext2clwwlk  30408  wwlksubclwwlk  30409  eupth2lems  30589  smcnlem  31049  minvecolem4  31232  pjhthlem1  31743  zltp1ne  35601  cvmliftlem7  35783  dnibndlem13  37079  knoppndvlem19  37119  knoppndvlem21  37121  icoreunrn  38005  relowlssretop  38009  ltflcei  38259  poimirlem1  38272  poimirlem2  38273  poimirlem4  38275  poimirlem6  38277  poimirlem7  38278  poimirlem8  38279  opnmbllem0  38307  mblfinlem1  38308  mblfinlem2  38309  mblfinlem4  38311  itg2addnclem2  38323  itg2addnclem3  38324  incsequz  38399  isbnd3  38435  rrntotbnd  38487  sn-sup2  43265  3cubeslem1  43415  3cubeslem2  43416  irrapxlem4  43552  pellexlem5  43560  pell14qrgapw  43603  pellfundgt1  43610  jm3.1lem2  43745  expdiophlem1  43748  fzuntgd  44184  zltlesub  46004  suplesup  46055  supxrunb3  46114  xrpnf  46199  fmul01lt1lem1  46300  limsupre3lem  46446  xlimxrre  46545  xlimpnfv  46552  ioodvbdlimc1lem1  46645  dvnxpaek  46656  dvnmul  46657  fourierdlem4  46825  fourierdlem11  46832  fourierdlem25  46846  fourierdlem50  46870  fourierdlem64  46884  fourierdlem65  46885  fourierdlem77  46897  fourierdlem79  46899  iinhoiicclem  47387  smfresal  47502  natglobalincr  47593  fmtno4prmfac  48324  lighneallem4a  48360  evenltle  48482  perfectALTVlem2  48487  logbpw2m1  49347