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

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

Proof of Theorem peano2re
StepHypRef Expression
1 1re 11162 . 2 1 ∈ ℝ
2 readdcl 11141 . 2 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
31, 2mpan2 690 1 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  (class class class)co 7362  cr 11057  1c1 11059   + caddc 11061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-i2m1 11126  ax-1ne0 11127  ax-rrecex 11130  ax-cnre 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365
This theorem is referenced by:  lep1  12003  letrp1  12006  p1le  12007  ledivp1  12064  sup2  12118  nnssre  12164  nnge1  12188  div4p1lem1div2  12415  zltp1le  12560  suprzcl  12590  zeo  12596  peano2uz2  12598  uzind  12602  numltc  12651  uzwo  12843  ge0p1rp  12953  qbtwnxr  13126  xrsupsslem  13233  supxrunb1  13245  fznatpl1  13502  fzp1disj  13507  fzneuz  13529  fzp1nel  13532  ubmelm1fzo  13675  fllep1  13713  flflp1  13719  flhalf  13742  ltdifltdiv  13746  fldiv4p1lem1div2  13747  dfceil2  13751  ceim1l  13759  uzsup  13775  modltm1p1mod  13835  addmodlteq  13858  fsequb  13887  seqf1olem1  13954  seqf1olem2  13955  bernneq3  14141  expnbnd  14142  expmulnbnd  14145  discr1  14149  discr  14150  facwordi  14196  faclbnd  14197  hashfun  14344  seqcoll2  14371  rexuzre  15244  caubnd  15250  rlim2lt  15386  lo1bddrp  15414  rlimo1  15506  o1rlimmul  15508  o1fsum  15705  harmonic  15751  expcnv  15756  geomulcvg  15768  mertenslem1  15776  bpoly4  15949  nonsq  16641  eulerthlem2  16661  pcprendvds  16719  pcmpt  16771  pcfac  16778  vdwlem6  16865  vdwlem11  16870  chfacffsupp  22221  chfacfscmul0  22223  chfacfpmmul0  22227  tgioo  24175  zcld  24192  iocopnst  24319  cnheibor  24334  bndth  24337  cncmet  24702  pjthlem1  24817  ovolicc2lem3  24899  ovolicopnf  24904  ioorcl2  24952  dyadf  24971  dyadovol  24973  dyadss  24974  dyaddisjlem  24975  dyadmaxlem  24977  opnmbllem  24981  volsup2  24985  vitalilem2  24989  itg2const2  25122  itg2cnlem1  25142  dvfsumle  25401  dvfsumabs  25403  dvfsumlem1  25406  dvfsumlem3  25408  dvfsumrlim  25411  fta1glem2  25547  fta1lem  25683  aalioulem3  25710  ulmbdd  25773  itgulm  25783  psercnlem1  25800  abelthlem2  25807  abelthlem7  25813  reeff1olem  25821  logtayl  26031  loglesqrt  26127  atanlogsublem  26281  leibpi  26308  efrlim  26335  harmonicubnd  26375  fsumharmonic  26377  ftalem5  26442  basellem2  26447  basellem3  26448  chtnprm  26519  chpp1  26520  ppip1le  26526  ppiub  26568  logfaclbnd  26586  logfacrlim  26588  perfectlem2  26594  bcmono  26641  lgsvalmod  26680  gausslemma2dlem3  26732  lgseisen  26743  lgsquadlem1  26744  lgsquadlem2  26745  chebbnd1lem2  26834  chtppilimlem1  26837  rplogsumlem2  26849  dchrisumlema  26852  dchrisumlem1  26853  dchrisumlem3  26855  dchrisum0lem1  26880  chpdifbndlem1  26917  logdivbnd  26920  pntrmax  26928  pntrsumo1  26929  pntpbnd1a  26949  pntpbnd1  26950  pntpbnd2  26951  pntibndlem2  26955  pntlemg  26962  pntlemr  26966  pntlemj  26967  pntlemk  26970  ostth2lem1  26982  qabvle  26989  ostth2lem3  26999  ostth2lem4  27000  axlowdimlem16  27948  wwlksnredwwlkn  28882  wwlksnextproplem3  28898  wwlksext2clwwlk  29043  wwlksubclwwlk  29044  eupth2lems  29224  smcnlem  29681  minvecolem4  29864  pjhthlem1  30375  zltp1ne  33740  cvmliftlem7  33925  dnibndlem13  34982  knoppndvlem19  35022  knoppndvlem21  35024  icoreunrn  35859  relowlssretop  35863  ltflcei  36095  poimirlem1  36108  poimirlem2  36109  poimirlem4  36111  poimirlem6  36113  poimirlem7  36114  poimirlem8  36115  opnmbllem0  36143  mblfinlem1  36144  mblfinlem2  36145  mblfinlem4  36147  itg2addnclem2  36159  itg2addnclem3  36160  incsequz  36236  isbnd3  36272  rrntotbnd  36324  sn-sup2  40967  3cubeslem1  41036  3cubeslem2  41037  irrapxlem4  41177  pellexlem5  41185  pell14qrgapw  41228  pellfundgt1  41235  jm3.1lem2  41371  expdiophlem1  41374  fzuntgd  41804  zltlesub  43593  suplesup  43647  supxrunb3  43708  xrpnf  43795  fmul01lt1lem1  43899  limsupre3lem  44047  xlimxrre  44146  xlimpnfv  44153  ioodvbdlimc1lem1  44246  dvnxpaek  44257  dvnmul  44258  fourierdlem4  44426  fourierdlem11  44433  fourierdlem25  44447  fourierdlem50  44471  fourierdlem64  44485  fourierdlem65  44486  fourierdlem77  44498  fourierdlem79  44500  iinhoiicclem  44988  smfresal  45103  natglobalincr  45190  fmtno4prmfac  45838  lighneallem4a  45874  evenltle  45983  perfectALTVlem2  45988  logbpw2m1  46727
  Copyright terms: Public domain W3C validator