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

Theorem rpge0d 11308
Description: A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1  |-  ( ph  ->  A  e.  RR+ )
Assertion
Ref Expression
rpge0d  |-  ( ph  ->  0  <_  A )

Proof of Theorem rpge0d
StepHypRef Expression
1 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
2 rpge0 11277 . 2  |-  ( A  e.  RR+  ->  0  <_  A )
31, 2syl 17 1  |-  ( ph  ->  0  <_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   class class class wbr 4395   0cc0 9522    <_ cle 9659   RR+crp 11265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-i2m1 9590  ax-1ne0 9591  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-ov 6281  df-er 7348  df-en 7555  df-dom 7556  df-sdom 7557  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-rp 11266
This theorem is referenced by:  rprege0d  11311  sqrlem5  13229  isumrpcl  13806  isumltss  13811  harmonic  13822  expcnv  13827  prmreclem5  14647  prmreclem6  14648  4sqlem7  14671  nmoi2  21529  reperflem  21615  lebnumii  21758  nmoleub2lem3  21890  nmoleub3  21894  lmnn  21994  minveclem3  22136  pjthlem1  22144  ovoliunlem1  22205  vitalilem4  22312  vitali  22314  itg2const2  22440  itggt0  22540  lhop1lem  22706  plyeq0lem  22899  aalioulem4  23023  aaliou3lem2  23031  aaliou3lem3  23032  pserdvlem2  23115  abelthlem7  23125  pilem2  23139  pilem3  23140  divlogrlim  23310  logtayllem  23334  cxpge0  23358  divcxp  23362  cxpsqrtlem  23377  cxpsqrt  23378  abscxpbnd  23423  asinlem3  23527  leibpi  23598  birthdaylem3  23609  rlimcnp3  23623  cxplim  23627  rlimcxp  23629  cxp2limlem  23631  cxp2lim  23632  jensenlem2  23643  amgmlem  23645  emcllem2  23652  emcllem4  23654  emcllem6  23656  fsumharmonic  23667  zetacvg  23670  lgamgulmlem2  23685  lgamgulmlem3  23686  lgamgulmlem5  23688  lgamcvg2  23710  regamcl  23716  ftalem3  23729  ftalem5  23731  basellem6  23740  basellem8  23742  chtge0  23767  chtwordi  23811  chpval2  23874  chpchtsum  23875  chpub  23876  bposlem1  23940  bposlem2  23941  bposlem4  23943  bposlem5  23944  bposlem6  23945  bposlem7  23946  bposlem9  23948  lgsquadlem2  24011  chtppilimlem1  24039  chtppilimlem2  24040  chtppilim  24041  chpchtlim  24045  rplogsumlem1  24050  rplogsumlem2  24051  dchrisum0lem1a  24052  rpvmasumlem  24053  dchrisumlema  24054  2vmadivsumlem  24106  logdivbnd  24122  selberg3lem1  24123  selberg3lem2  24124  selberg4lem1  24126  pntrsumbnd2  24133  pntrlog2bndlem1  24143  pntrlog2bndlem2  24144  pntrlog2bndlem3  24145  pntrlog2bndlem4  24146  pntrlog2bndlem5  24147  pntrlog2bndlem6a  24148  pntrlog2bndlem6  24149  pntrlog2bnd  24150  pntibndlem2  24157  pntlemg  24164  pntlemk  24172  pntlem3  24175  pntleml  24177  ostth2lem1  24184  padicabv  24196  ostth2lem3  24201  ostth3  24204  ubthlem2  26201  minvecolem3  26206  minvecolem5  26211  pjhthlem1  26723  sqsscirc1  28343  omssubaddlem  28747  taupilemrplb  31246  itggt0cn  31460  geomcau  31534  cntotbnd  31574  rrndstprj2  31609  irrapxlem5  35123  pell1qrgaplem  35170  pell14qrgapw  35173  pellqrex  35176  rpexpmord  35245  rmxypos  35246  binomcxplemnotnn0  36109  stoweidlem3  37153  stoweidlem26  37176  wallispilem4  37218  wallispi  37220  wallispi2lem1  37221  stirlinglem1  37224  stirlinglem4  37227  stirlinglem10  37233  stirlinglem11  37234  stirlinglem12  37235  fourierdlem39  37296  fourierdlem42  37299  fourierdlem87  37344  fourierdlem107  37364
  Copyright terms: Public domain W3C validator