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

Theorem rpge0d 10390
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 10362 . 2  |-  ( A  e.  RR+  ->  0  <_  A )
31, 2syl 17 1  |-  ( ph  ->  0  <_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1685   class class class wbr 4025   0cc0 8733    <_ cle 8864   RR+crp 10350
This theorem is referenced by:  rprege0d  10393  sqrlem5  11727  isumrpcl  12297  isumltss  12302  harmonic  12312  expcnv  12317  prmreclem5  12962  prmreclem6  12963  4sqlem7  12986  nmoi2  18234  reperflem  18318  lebnumii  18459  nmoleub2lem3  18591  nmoleub3  18595  lmnn  18684  minveclem3  18788  pjthlem1  18796  ovoliunlem1  18856  vitalilem4  18961  vitali  18963  itg2const2  19091  itggt0  19191  lhop1lem  19355  plyeq0lem  19587  aalioulem4  19710  aaliou3lem2  19718  aaliou3lem3  19719  pserdvlem2  19799  abelthlem7  19809  pilem2  19823  pilem3  19824  divlogrlim  19977  logtayllem  20001  cxpge0  20025  divcxp  20029  cxpsqrlem  20044  cxpsqr  20045  abscxpbnd  20088  asinlem3  20162  leibpi  20233  birthdaylem3  20243  rlimcnp3  20257  cxplim  20261  rlimcxp  20263  cxp2limlem  20265  cxp2lim  20266  jensenlem2  20277  amgmlem  20279  emcllem2  20285  emcllem4  20287  emcllem6  20289  fsumharmonic  20300  ftalem3  20307  ftalem5  20309  basellem6  20318  basellem8  20320  chtge0  20345  chtwordi  20389  chpval2  20452  chpchtsum  20453  chpub  20454  bposlem1  20518  bposlem2  20519  bposlem4  20521  bposlem5  20522  bposlem6  20523  bposlem7  20524  bposlem9  20526  lgsquadlem2  20589  chtppilimlem1  20617  chtppilimlem2  20618  chtppilim  20619  chpchtlim  20623  rplogsumlem1  20628  rplogsumlem2  20629  dchrisum0lem1a  20630  rpvmasumlem  20631  dchrisumlema  20632  2vmadivsumlem  20684  logdivbnd  20700  selberg3lem1  20701  selberg3lem2  20702  selberg4lem1  20704  pntrsumbnd2  20711  pntrlog2bndlem1  20721  pntrlog2bndlem2  20722  pntrlog2bndlem3  20723  pntrlog2bndlem4  20724  pntrlog2bndlem5  20725  pntrlog2bndlem6a  20726  pntrlog2bndlem6  20727  pntrlog2bnd  20728  pntibndlem2  20735  pntlemg  20742  pntlemk  20750  pntlem3  20753  pntleml  20755  ostth2lem1  20762  padicabv  20774  ostth2lem3  20779  ostth3  20782  ubthlem2  21443  minvecolem3  21448  minvecolem5  21453  pjhthlem1  21963  zetacvg  23094  geomcau  25875  cntotbnd  25920  rrndstprj2  25955  irrapxlem5  26311  pell1qrgaplem  26358  pell14qrgapw  26361  pellqrex  26364  rpexpmord  26433  rmxypos  26434  wallispilem4  27217  wallispi  27219  wallispi2lem1  27220  stirlinglem1  27223  stirlinglem4  27226  stirlinglem10  27232  stirlinglem11  27233  stirlinglem12  27234
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-resscn 8790  ax-1cn 8791  ax-icn 8792  ax-addcl 8793  ax-addrcl 8794  ax-mulcl 8795  ax-mulrcl 8796  ax-i2m1 8801  ax-1ne0 8802  ax-rnegex 8804  ax-rrecex 8805  ax-cnre 8806  ax-pre-lttri 8807
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fun 5224  df-fn 5225  df-f 5226  df-f1 5227  df-fo 5228  df-f1o 5229  df-fv 5230  df-ov 5823  df-er 6656  df-en 6860  df-dom 6861  df-sdom 6862  df-pnf 8865  df-mnf 8866  df-xr 8867  df-ltxr 8868  df-le 8869  df-rp 10351
  Copyright terms: Public domain W3C validator