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

Theorem peano2re 9806
Description: A theorem for reals analogous the second Peano postulate peano2nn 10621. (Contributed by NM, 5-Jul-2005.)
Assertion
Ref Expression
peano2re  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )

Proof of Theorem peano2re
StepHypRef Expression
1 1re 9642 . 2  |-  1  e.  RR
2 readdcl 9622 . 2  |-  ( ( A  e.  RR  /\  1  e.  RR )  ->  ( A  +  1 )  e.  RR )
31, 2mpan2 675 1  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868  (class class class)co 6301   RRcr 9538   1c1 9540    + caddc 9542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-i2m1 9607  ax-1ne0 9608  ax-rrecex 9611  ax-cnre 9612
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-iota 5561  df-fv 5605  df-ov 6304
This theorem is referenced by:  lep1  10444  letrp1  10447  p1le  10448  ledivp1  10508  sup2  10565  nnssre  10613  nnge1  10635  zltp1le  10986  suprzcl  11015  zeo  11021  peano2uz2  11023  uzind  11027  numltc  11071  uzwo  11222  ge0p1rp  11331  qbtwnxr  11493  xrsupsslem  11592  supxrunb1  11605  fznatpl1  11850  fzp1disj  11854  fzneuz  11875  fzp1nel  11878  ubmelm1fzo  12006  fllep1  12036  flflp1  12042  flhalf  12061  ltdifltdiv  12065  dfceil2  12067  ceim1l  12073  uzsup  12089  modltm1p1mod  12141  fsequb  12187  seqf1olem1  12251  seqf1olem2  12252  bernneq3  12399  expnbnd  12400  expmulnbnd  12403  discr1  12407  discr  12408  facwordi  12473  faclbnd  12474  hashfun  12606  seqcoll2  12625  rexuzre  13401  caubnd  13407  rlim2lt  13546  lo1bddrp  13574  rlimo1  13665  o1rlimmul  13667  o1fsum  13858  harmonic  13902  expcnv  13907  geomulcvg  13917  mertenslem1  13925  bpoly4  14097  nonsq  14693  eulerthlem2  14715  pcprendvds  14775  pcmpt  14822  pcfac  14829  vdwlem6  14921  vdwlem11  14926  chfacffsupp  19864  chfacfscmul0  19866  chfacfpmmul0  19870  tgioo  21798  zcld  21815  iocopnst  21952  cnheibor  21967  bndth  21970  cncmet  22274  pjthlem1  22375  ovolicc2lem3  22456  ovolicopnf  22462  ioorcl2  22508  dyadf  22533  dyadovol  22535  dyadss  22536  dyaddisjlem  22537  dyadmaxlem  22539  opnmbllem  22543  volsup2  22547  vitalilem2  22551  itg2const2  22683  itg2cnlem1  22703  dvfsumle  22957  dvfsumabs  22959  dvfsumlem1  22962  dvfsumlem3  22964  dvfsumrlim  22967  fta1glem2  23101  fta1lem  23244  aalioulem3  23274  ulmbdd  23337  itgulm  23347  psercnlem1  23364  abelthlem2  23371  abelthlem7  23377  reeff1olem  23385  logtayl  23589  loglesqrt  23682  atanlogsublem  23825  leibpi  23852  efrlim  23879  harmonicubnd  23919  fsumharmonic  23921  ftalem5  23985  ftalem5OLD  23987  basellem2  23992  basellem3  23993  chtnprm  24065  chpp1  24066  ppip1le  24072  ppiub  24116  logfaclbnd  24134  logfacrlim  24136  perfectlem2  24142  bcmono  24189  lgsvalmod  24227  lgseisen  24265  lgsquadlem1  24266  lgsquadlem2  24267  chebbnd1lem2  24292  chtppilimlem1  24295  rplogsumlem2  24307  dchrisumlema  24310  dchrisumlem1  24311  dchrisumlem3  24313  dchrisum0lem1  24338  chpdifbndlem1  24375  logdivbnd  24378  pntrmax  24386  pntrsumo1  24387  pntpbnd1a  24407  pntpbnd1  24408  pntpbnd2  24409  pntibndlem2  24413  pntlemg  24420  pntlemr  24424  pntlemj  24425  pntlemk  24428  ostth2lem1  24440  qabvle  24447  ostth2lem3  24457  ostth2lem4  24458  axlowdimlem16  24971  wwlknredwwlkn  25437  wwlkextproplem1  25452  wwlkextproplem3  25454  wwlkext2clwwlk  25514  wwlksubclwwlk  25515  clwlkfclwwlk  25555  eupath2lem3  25690  eupath2  25691  extwwlkfablem2  25789  smcnlem  26316  minvecolem4  26505  minvecolem4OLD  26515  pjhthlem1  27027  cvmliftlem7  30007  icoreunrn  31700  relowlssretop  31704  ltflcei  31844  poimirlem1  31852  poimirlem2  31853  poimirlem4  31855  poimirlem6  31857  poimirlem7  31858  poimirlem8  31859  opnmbllem0  31887  mblfinlem1  31888  mblfinlem2  31889  mblfinlem4  31891  dvtanlemOLD  31902  itg2addnclem2  31905  itg2addnclem3  31906  incsequz  31988  isbnd3  32027  rrntotbnd  32079  irrapxlem4  35586  pellexlem5  35594  pell14qrgapw  35639  pellfundgt1  35648  jm3.1lem2  35790  expdiophlem1  35793  zltlesub  37334  suplesup  37401  fmul01lt1lem1  37479  ioodvbdlimc1lem1  37620  ioodvbdlimc1lem1OLD  37622  dvnxpaek  37634  dvnmul  37635  fourierdlem4  37790  fourierdlem11  37797  fourierdlem25  37811  fourierdlem50  37837  fourierdlem64  37851  fourierdlem65  37852  fourierdlem77  37864  fourierdlem79  37866  perfectALTVlem2  38553  logbpw2m1  39566
  Copyright terms: Public domain W3C validator