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

Theorem rpge0d 11023
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 10995 . 2  |-  ( A  e.  RR+  ->  0  <_  A )
31, 2syl 16 1  |-  ( ph  ->  0  <_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   class class class wbr 4287   0cc0 9274    <_ cle 9411   RR+crp 10983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-rp 10984
This theorem is referenced by:  rprege0d  11026  sqrlem5  12728  isumrpcl  13298  isumltss  13303  harmonic  13313  expcnv  13318  prmreclem5  13973  prmreclem6  13974  4sqlem7  13997  nmoi2  20289  reperflem  20375  lebnumii  20518  nmoleub2lem3  20650  nmoleub3  20654  lmnn  20754  minveclem3  20896  pjthlem1  20904  ovoliunlem1  20965  vitalilem4  21071  vitali  21073  itg2const2  21199  itggt0  21299  lhop1lem  21465  plyeq0lem  21658  aalioulem4  21781  aaliou3lem2  21789  aaliou3lem3  21790  pserdvlem2  21873  abelthlem7  21883  pilem2  21897  pilem3  21898  divlogrlim  22060  logtayllem  22084  cxpge0  22108  divcxp  22112  cxpsqrlem  22127  cxpsqr  22128  abscxpbnd  22171  asinlem3  22246  leibpi  22317  birthdaylem3  22327  rlimcnp3  22341  cxplim  22345  rlimcxp  22347  cxp2limlem  22349  cxp2lim  22350  jensenlem2  22361  amgmlem  22363  emcllem2  22370  emcllem4  22372  emcllem6  22374  fsumharmonic  22385  ftalem3  22392  ftalem5  22394  basellem6  22403  basellem8  22405  chtge0  22430  chtwordi  22474  chpval2  22537  chpchtsum  22538  chpub  22539  bposlem1  22603  bposlem2  22604  bposlem4  22606  bposlem5  22607  bposlem6  22608  bposlem7  22609  bposlem9  22611  lgsquadlem2  22674  chtppilimlem1  22702  chtppilimlem2  22703  chtppilim  22704  chpchtlim  22708  rplogsumlem1  22713  rplogsumlem2  22714  dchrisum0lem1a  22715  rpvmasumlem  22716  dchrisumlema  22717  2vmadivsumlem  22769  logdivbnd  22785  selberg3lem1  22786  selberg3lem2  22787  selberg4lem1  22789  pntrsumbnd2  22796  pntrlog2bndlem1  22806  pntrlog2bndlem2  22807  pntrlog2bndlem3  22808  pntrlog2bndlem4  22809  pntrlog2bndlem5  22810  pntrlog2bndlem6a  22811  pntrlog2bndlem6  22812  pntrlog2bnd  22813  pntibndlem2  22820  pntlemg  22827  pntlemk  22835  pntlem3  22838  pntleml  22840  ostth2lem1  22847  padicabv  22859  ostth2lem3  22864  ostth3  22867  ubthlem2  24240  minvecolem3  24245  minvecolem5  24250  pjhthlem1  24762  sqsscirc1  26307  zetacvg  26970  lgamgulmlem2  26985  lgamgulmlem3  26986  lgamgulmlem5  26988  lgamcvg2  27010  regamcl  27016  itggt0cn  28435  geomcau  28626  cntotbnd  28666  rrndstprj2  28701  irrapxlem5  29138  pell1qrgaplem  29185  pell14qrgapw  29188  pellqrex  29191  rpexpmord  29260  rmxypos  29261  stoweidlem3  29769  stoweidlem26  29792  wallispilem4  29834  wallispi  29836  wallispi2lem1  29837  stirlinglem1  29840  stirlinglem4  29843  stirlinglem10  29849  stirlinglem11  29850  stirlinglem12  29851  taupilemrplb  35507
  Copyright terms: Public domain W3C validator