MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  peano2re Structured version   Visualization version   GIF version

Theorem peano2re 10463
Description: A theorem for reals analogous the second Peano postulate peano2nn 11288. (Contributed by NM, 5-Jul-2005.)
Assertion
Ref Expression
peano2re (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Proof of Theorem peano2re
StepHypRef Expression
1 1re 10293 . 2 1 ∈ ℝ
2 readdcl 10272 . 2 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
31, 2mpan2 682 1 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  (class class class)co 6842  cr 10188  1c1 10190   + caddc 10192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-i2m1 10257  ax-1ne0 10258  ax-rrecex 10261  ax-cnre 10262
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-iota 6031  df-fv 6076  df-ov 6845
This theorem is referenced by:  lep1  11116  letrp1  11119  p1le  11120  ledivp1  11179  sup2  11233  nnssre  11278  nnge1  11303  div4p1lem1div2  11533  zltp1le  11674  suprzcl  11704  zeo  11710  peano2uz2  11712  uzind  11716  numltc  11767  uzwo  11952  ge0p1rp  12060  qbtwnxr  12233  xrsupsslem  12339  supxrunb1  12351  fznatpl1  12602  fzp1disj  12606  fzneuz  12628  fzp1nel  12631  ubmelm1fzo  12772  fllep1  12810  flflp1  12816  flhalf  12839  ltdifltdiv  12843  fldiv4p1lem1div2  12844  dfceil2  12848  ceim1l  12854  uzsup  12870  modltm1p1mod  12930  addmodlteq  12953  fsequb  12982  seqf1olem1  13047  seqf1olem2  13048  bernneq3  13199  expnbnd  13200  expmulnbnd  13203  discr1  13207  discr  13208  facwordi  13280  faclbnd  13281  hashfun  13425  seqcoll2  13450  rexuzre  14379  caubnd  14385  rlim2lt  14515  lo1bddrp  14543  rlimo1  14634  o1rlimmul  14636  o1fsum  14831  harmonic  14877  expcnv  14882  geomulcvg  14893  mertenslem1  14901  bpoly4  15074  nonsq  15748  eulerthlem2  15768  pcprendvds  15826  pcmpt  15877  pcfac  15884  vdwlem6  15971  vdwlem11  15976  chfacffsupp  20940  chfacfscmul0  20942  chfacfpmmul0  20946  tgioo  22878  zcld  22895  iocopnst  23018  cnheibor  23033  bndth  23036  cncmet  23399  pjthlem1  23497  ovolicc2lem3  23577  ovolicopnf  23582  ioorcl2  23630  dyadf  23649  dyadovol  23651  dyadss  23652  dyaddisjlem  23653  dyadmaxlem  23655  opnmbllem  23659  volsup2  23663  vitalilem2  23667  itg2const2  23799  itg2cnlem1  23819  dvfsumle  24075  dvfsumabs  24077  dvfsumlem1  24080  dvfsumlem3  24082  dvfsumrlim  24085  fta1glem2  24217  fta1lem  24353  aalioulem3  24380  ulmbdd  24443  itgulm  24453  psercnlem1  24470  abelthlem2  24477  abelthlem7  24483  reeff1olem  24491  logtayl  24697  loglesqrt  24790  atanlogsublem  24933  leibpi  24960  efrlim  24987  harmonicubnd  25027  fsumharmonic  25029  ftalem5  25094  basellem2  25099  basellem3  25100  chtnprm  25171  chpp1  25172  ppip1le  25178  ppiub  25220  logfaclbnd  25238  logfacrlim  25240  perfectlem2  25246  bcmono  25293  lgsvalmod  25332  gausslemma2dlem3  25384  lgseisen  25395  lgsquadlem1  25396  lgsquadlem2  25397  chebbnd1lem2  25450  chtppilimlem1  25453  rplogsumlem2  25465  dchrisumlema  25468  dchrisumlem1  25469  dchrisumlem3  25471  dchrisum0lem1  25496  chpdifbndlem1  25533  logdivbnd  25536  pntrmax  25544  pntrsumo1  25545  pntpbnd1a  25565  pntpbnd1  25566  pntpbnd2  25567  pntibndlem2  25571  pntlemg  25578  pntlemr  25582  pntlemj  25583  pntlemk  25586  ostth2lem1  25598  qabvle  25605  ostth2lem3  25615  ostth2lem4  25616  axlowdimlem16  26128  wwlksnredwwlkn  27095  wwlksnextproplem3  27112  wwlksext2clwwlk  27270  wwlksext2clwwlkOLD  27271  wwlksubclwwlk  27272  clwlksfclwwlkOLD  27299  eupth2lems  27474  smcnlem  27943  minvecolem4  28127  pjhthlem1  28641  cvmliftlem7  31653  dnibndlem13  32851  knoppndvlem19  32892  knoppndvlem21  32894  icoreunrn  33572  relowlssretop  33576  ltflcei  33753  poimirlem1  33766  poimirlem2  33767  poimirlem4  33769  poimirlem6  33771  poimirlem7  33772  poimirlem8  33773  opnmbllem0  33801  mblfinlem1  33802  mblfinlem2  33803  mblfinlem4  33805  itg2addnclem2  33817  itg2addnclem3  33818  incsequz  33898  isbnd3  33937  rrntotbnd  33989  irrapxlem4  37999  pellexlem5  38007  pell14qrgapw  38050  pellfundgt1  38057  jm3.1lem2  38194  expdiophlem1  38197  zltlesub  40069  suplesup  40125  supxrunb3  40192  xrpnf  40285  fmul01lt1lem1  40386  limsupre3lem  40534  xlimxrre  40627  xlimpnfv  40634  ioodvbdlimc1lem1  40716  dvnxpaek  40727  dvnmul  40728  fourierdlem4  40897  fourierdlem11  40904  fourierdlem25  40918  fourierdlem50  40942  fourierdlem64  40956  fourierdlem65  40957  fourierdlem77  40969  fourierdlem79  40971  iinhoiicclem  41459  smfresal  41567  fmtno4prmfac  42092  lighneallem4a  42133  evenltle  42234  perfectALTVlem2  42239  logbpw2m1  42962
  Copyright terms: Public domain W3C validator