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

Theorem rpge0d 11019
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 10991 . 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 1755   class class class wbr 4280   0cc0 9270    <_ cle 9407   RR+crp 10979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-i2m1 9338  ax-1ne0 9339  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-rp 10980
This theorem is referenced by:  rprege0d  11022  sqrlem5  12720  isumrpcl  13289  isumltss  13294  harmonic  13304  expcnv  13309  prmreclem5  13964  prmreclem6  13965  4sqlem7  13988  nmoi2  20151  reperflem  20237  lebnumii  20380  nmoleub2lem3  20512  nmoleub3  20516  lmnn  20616  minveclem3  20758  pjthlem1  20766  ovoliunlem1  20827  vitalilem4  20933  vitali  20935  itg2const2  21061  itggt0  21161  lhop1lem  21327  plyeq0lem  21563  aalioulem4  21686  aaliou3lem2  21694  aaliou3lem3  21695  pserdvlem2  21778  abelthlem7  21788  pilem2  21802  pilem3  21803  divlogrlim  21965  logtayllem  21989  cxpge0  22013  divcxp  22017  cxpsqrlem  22032  cxpsqr  22033  abscxpbnd  22076  asinlem3  22151  leibpi  22222  birthdaylem3  22232  rlimcnp3  22246  cxplim  22250  rlimcxp  22252  cxp2limlem  22254  cxp2lim  22255  jensenlem2  22266  amgmlem  22268  emcllem2  22275  emcllem4  22277  emcllem6  22279  fsumharmonic  22290  ftalem3  22297  ftalem5  22299  basellem6  22308  basellem8  22310  chtge0  22335  chtwordi  22379  chpval2  22442  chpchtsum  22443  chpub  22444  bposlem1  22508  bposlem2  22509  bposlem4  22511  bposlem5  22512  bposlem6  22513  bposlem7  22514  bposlem9  22516  lgsquadlem2  22579  chtppilimlem1  22607  chtppilimlem2  22608  chtppilim  22609  chpchtlim  22613  rplogsumlem1  22618  rplogsumlem2  22619  dchrisum0lem1a  22620  rpvmasumlem  22621  dchrisumlema  22622  2vmadivsumlem  22674  logdivbnd  22690  selberg3lem1  22691  selberg3lem2  22692  selberg4lem1  22694  pntrsumbnd2  22701  pntrlog2bndlem1  22711  pntrlog2bndlem2  22712  pntrlog2bndlem3  22713  pntrlog2bndlem4  22714  pntrlog2bndlem5  22715  pntrlog2bndlem6a  22716  pntrlog2bndlem6  22717  pntrlog2bnd  22718  pntibndlem2  22725  pntlemg  22732  pntlemk  22740  pntlem3  22743  pntleml  22745  ostth2lem1  22752  padicabv  22764  ostth2lem3  22769  ostth3  22772  ubthlem2  24095  minvecolem3  24100  minvecolem5  24105  pjhthlem1  24617  sqsscirc1  26192  zetacvg  26849  lgamgulmlem2  26864  lgamgulmlem3  26865  lgamgulmlem5  26867  lgamcvg2  26889  regamcl  26895  itggt0cn  28308  geomcau  28499  cntotbnd  28539  rrndstprj2  28574  irrapxlem5  29012  pell1qrgaplem  29059  pell14qrgapw  29062  pellqrex  29065  rpexpmord  29134  rmxypos  29135  stoweidlem3  29644  stoweidlem26  29667  wallispilem4  29709  wallispi  29711  wallispi2lem1  29712  stirlinglem1  29715  stirlinglem4  29718  stirlinglem10  29724  stirlinglem11  29725  stirlinglem12  29726  taupilemrplb  35208
  Copyright terms: Public domain W3C validator