Theorem peano2re 10209

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 10039	. 2 ⊢ 1 ∈ ℝ
2		readdcl 10019	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 707	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1990  (class class class)co 6650  ℝcr 9935  1c1 9937   + caddc 9939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  lep1  10862  letrp1  10865  p1le  10866  ledivp1  10925  sup2  10979  nnssre  11024  nnge1  11046  div4p1lem1div2  11287  zltp1le  11427  suprzcl  11457  zeo  11463  peano2uz2  11465  uzind  11469  numltc  11528  uzwo  11751  ge0p1rp  11862  qbtwnxr  12031  xrsupsslem  12137  supxrunb1  12149  fznatpl1  12395  fzp1disj  12399  fzneuz  12421  fzp1nel  12424  ubmelm1fzo  12564  fllep1  12602  flflp1  12608  flhalf  12631  ltdifltdiv  12635  fldiv4p1lem1div2  12636  dfceil2  12640  ceim1l  12646  uzsup  12662  modltm1p1mod  12722  addmodlteq  12745  fsequb  12774  seqf1olem1  12840  seqf1olem2  12841  bernneq3  12992  expnbnd  12993  expmulnbnd  12996  discr1  13000  discr  13001  facwordi  13076  faclbnd  13077  hashfun  13224  seqcoll2  13249  rexuzre  14092  caubnd  14098  rlim2lt  14228  lo1bddrp  14256  rlimo1  14347  o1rlimmul  14349  o1fsum  14545  harmonic  14591  expcnv  14596  geomulcvg  14607  mertenslem1  14616  bpoly4  14790  nonsq  15467  eulerthlem2  15487  pcprendvds  15545  pcmpt  15596  pcfac  15603  vdwlem6  15690  vdwlem11  15695  chfacffsupp  20661  chfacfscmul0  20663  chfacfpmmul0  20667  tgioo  22599  zcld  22616  iocopnst  22739  cnheibor  22754  bndth  22757  cncmet  23119  pjthlem1  23208  ovolicc2lem3  23287  ovolicopnf  23292  ioorcl2  23340  dyadf  23359  dyadovol  23361  dyadss  23362  dyaddisjlem  23363  dyadmaxlem  23365  opnmbllem  23369  volsup2  23373  vitalilem2  23378  itg2const2  23508  itg2cnlem1  23528  dvfsumle  23784  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem3  23791  dvfsumrlim  23794  fta1glem2  23926  fta1lem  24062  aalioulem3  24089  ulmbdd  24152  itgulm  24162  psercnlem1  24179  abelthlem2  24186  abelthlem7  24192  reeff1olem  24200  logtayl  24406  loglesqrt  24499  atanlogsublem  24642  leibpi  24669  efrlim  24696  harmonicubnd  24736  fsumharmonic  24738  ftalem5  24803  basellem2  24808  basellem3  24809  chtnprm  24880  chpp1  24881  ppip1le  24887  ppiub  24929  logfaclbnd  24947  logfacrlim  24949  perfectlem2  24955  bcmono  25002  lgsvalmod  25041  gausslemma2dlem3  25093  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  chebbnd1lem2  25159  chtppilimlem1  25162  rplogsumlem2  25174  dchrisumlema  25177  dchrisumlem1  25178  dchrisumlem3  25180  dchrisum0lem1  25205  chpdifbndlem1  25242  logdivbnd  25245  pntrmax  25253  pntrsumo1  25254  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem2  25280  pntlemg  25287  pntlemr  25291  pntlemj  25292  pntlemk  25295  ostth2lem1  25307  qabvle  25314  ostth2lem3  25324  ostth2lem4  25325  axlowdimlem16  25837  wwlksnredwwlkn  26790  wwlksnextproplem3  26806  wwlksext2clwwlk  26924  wwlksubclwwlks  26925  clwlksfclwwlk  26962  eupth2lems  27098  smcnlem  27552  minvecolem4  27736  pjhthlem1  28250  cvmliftlem7  31273  dnibndlem13  32480  knoppndvlem19  32521  knoppndvlem21  32523  icoreunrn  33207  relowlssretop  33211  ltflcei  33397  poimirlem1  33410  poimirlem2  33411  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  opnmbllem0  33445  mblfinlem1  33446  mblfinlem2  33447  mblfinlem4  33449  itg2addnclem2  33462  itg2addnclem3  33463  incsequz  33544  isbnd3  33583  rrntotbnd  33635  irrapxlem4  37389  pellexlem5  37397  pell14qrgapw  37440  pellfundgt1  37447  jm3.1lem2  37585  expdiophlem1  37588  zltlesub  39497  suplesup  39555  supxrunb3  39623  fmul01lt1lem1  39816  limsupre3lem  39964  xlimxrre  40057  xlimpnfv  40064  ioodvbdlimc1lem1  40146  dvnxpaek  40157  dvnmul  40158  fourierdlem4  40328  fourierdlem11  40335  fourierdlem25  40349  fourierdlem50  40373  fourierdlem64  40387  fourierdlem65  40388  fourierdlem77  40400  fourierdlem79  40402  iinhoiicclem  40887  smfresal  40995  fmtno4prmfac  41484  lighneallem4a  41525  evenltle  41626  perfectALTVlem2  41631  logbpw2m1  42361