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

Theorem peano2re 9774
Description: A theorem for reals analogous the second Peano postulate peano2nn 10573. (Contributed by NM, 5-Jul-2005.)
Assertion
Ref Expression
peano2re

Proof of Theorem peano2re
StepHypRef Expression
1 1re 9616 . 2
2 readdcl 9596 . 2
31, 2mpan2 671 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  (class class class)co 6296   cr 9512  1c1 9514   caddc 9516
This theorem is referenced by:  lep1  10406  letrp1  10409  p1le  10410  ledivp1  10472  sup2  10524  nnssre  10565  nnge1  10587  zltp1le  10938  suprzcl  10967  zeo  10973  peano2uz2  10975  uzind  10979  numltc  11024  uzwo  11173  uzwoOLD  11174  ge0p1rp  11277  qbtwnxr  11428  xrsupsslem  11527  supxrunb1  11540  fznatpl1  11763  fzp1disj  11767  fzneuz  11788  fzp1nel  11791  ubmelm1fzo  11908  fllep1  11938  flflp1  11944  flhalf  11962  ltdifltdiv  11966  dfceil2  11968  ceim1l  11974  uzsup  11990  modltm1p1mod  12039  fsequb  12085  seqf1olem1  12146  seqf1olem2  12147  bernneq3  12294  expnbnd  12295  expmulnbnd  12298  discr1  12302  discr  12303  facwordi  12367  faclbnd  12368  hashfun  12495  seqcoll2  12513  rexuzre  13185  caubnd  13191  rlim2lt  13320  lo1bddrp  13348  rlimo1  13439  o1rlimmul  13441  o1fsum  13627  harmonic  13670  expcnv  13675  geomulcvg  13685  mertenslem1  13693  nonsq  14292  eulerthlem2  14312  pcprendvds  14364  pcmpt  14411  pcfac  14418  vdwlem6  14504  vdwlem11  14509  chfacffsupp  19357  chfacfscmul0  19359  chfacfpmmul0  19363  tgioo  21301  zcld  21318  iocopnst  21440  cnheibor  21455  bndth  21458  cncmet  21761  pjthlem1  21852  ovolicc2lem3  21930  ovolicopnf  21935  ioorcl2  21981  dyadf  22000  dyadovol  22002  dyadss  22003  dyaddisjlem  22004  dyadmaxlem  22006  opnmbllem  22010  volsup2  22014  vitalilem2  22018  itg2const2  22148  itg2cnlem1  22168  dvfsumle  22422  dvfsumabs  22424  dvfsumlem1  22427  dvfsumlem3  22429  dvfsumrlim  22432  fta1glem2  22567  fta1lem  22703  aalioulem3  22730  ulmbdd  22793  itgulm  22803  psercnlem1  22820  abelthlem2  22827  abelthlem7  22833  reeff1olem  22841  logtayl  23041  loglesqrt  23132  atanlogsublem  23246  leibpi  23273  efrlim  23299  harmonicubnd  23339  fsumharmonic  23341  ftalem5  23350  basellem2  23355  basellem3  23356  chtnprm  23428  chpp1  23429  ppip1le  23435  ppiub  23479  logfaclbnd  23497  logfacrlim  23499  perfectlem2  23505  bcmono  23552  lgsvalmod  23590  lgseisen  23628  lgsquadlem1  23629  lgsquadlem2  23630  chebbnd1lem2  23655  chtppilimlem1  23658  rplogsumlem2  23670  dchrisumlema  23673  dchrisumlem1  23674  dchrisumlem3  23676  dchrisum0lem1  23701  chpdifbndlem1  23738  logdivbnd  23741  pntrmax  23749  pntrsumo1  23750  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntibndlem2  23776  pntlemg  23783  pntlemr  23787  pntlemj  23788  pntlemk  23791  ostth2lem1  23803  qabvle  23810  ostth2lem3  23820  ostth2lem4  23821  axlowdimlem16  24260  wwlknredwwlkn  24726  wwlkextproplem1  24741  wwlkextproplem3  24743  wwlkext2clwwlk  24803  wwlksubclwwlk  24804  clwlkfclwwlk  24844  eupath2lem3  24979  eupath2  24980  extwwlkfablem2  25078  smcnlem  25607  minvecolem4  25796  pjhthlem1  26309  cvmliftlem7  28736  bpoly4  29821  ltflcei  30043  opnmbllem0  30050  mblfinlem1  30051  mblfinlem2  30052  mblfinlem4  30054  dvtanlem  30064  itg2addnclem2  30067  itg2addnclem3  30068  incsequz  30241  isbnd3  30280  rrntotbnd  30332  irrapxlem4  30761  pellexlem5  30769  pell14qrgapw  30812  pellfundgt1  30819  jm3.1lem2  30960  expdiophlem1  30963  zltlesub  31468  fmul01lt1lem1  31578  ioodvbdlimc1lem1  31728  dvnxpaek  31739  dvnmul  31740  fourierdlem4  31893  fourierdlem11  31900  fourierdlem25  31914  fourierdlem50  31939  fourierdlem64  31953  fourierdlem65  31954  fourierdlem77  31966  fourierdlem79  31968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator