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

Theorem rpge0d 11132
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 11104 . 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 1758   class class class wbr 4390   0cc0 9383    <_ cle 9520   RR+crp 11092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-i2m1 9451  ax-1ne0 9452  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-ov 6193  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-rp 11093
This theorem is referenced by:  rprege0d  11135  sqrlem5  12838  isumrpcl  13408  isumltss  13413  harmonic  13423  expcnv  13428  prmreclem5  14083  prmreclem6  14084  4sqlem7  14107  nmoi2  20425  reperflem  20511  lebnumii  20654  nmoleub2lem3  20786  nmoleub3  20790  lmnn  20890  minveclem3  21032  pjthlem1  21040  ovoliunlem1  21101  vitalilem4  21207  vitali  21209  itg2const2  21335  itggt0  21435  lhop1lem  21601  plyeq0lem  21794  aalioulem4  21917  aaliou3lem2  21925  aaliou3lem3  21926  pserdvlem2  22009  abelthlem7  22019  pilem2  22033  pilem3  22034  divlogrlim  22196  logtayllem  22220  cxpge0  22244  divcxp  22248  cxpsqrlem  22263  cxpsqr  22264  abscxpbnd  22307  asinlem3  22382  leibpi  22453  birthdaylem3  22463  rlimcnp3  22477  cxplim  22481  rlimcxp  22483  cxp2limlem  22485  cxp2lim  22486  jensenlem2  22497  amgmlem  22499  emcllem2  22506  emcllem4  22508  emcllem6  22510  fsumharmonic  22521  ftalem3  22528  ftalem5  22530  basellem6  22539  basellem8  22541  chtge0  22566  chtwordi  22610  chpval2  22673  chpchtsum  22674  chpub  22675  bposlem1  22739  bposlem2  22740  bposlem4  22742  bposlem5  22743  bposlem6  22744  bposlem7  22745  bposlem9  22747  lgsquadlem2  22810  chtppilimlem1  22838  chtppilimlem2  22839  chtppilim  22840  chpchtlim  22844  rplogsumlem1  22849  rplogsumlem2  22850  dchrisum0lem1a  22851  rpvmasumlem  22852  dchrisumlema  22853  2vmadivsumlem  22905  logdivbnd  22921  selberg3lem1  22922  selberg3lem2  22923  selberg4lem1  22925  pntrsumbnd2  22932  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bndlem6a  22947  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntibndlem2  22956  pntlemg  22963  pntlemk  22971  pntlem3  22974  pntleml  22976  ostth2lem1  22983  padicabv  22995  ostth2lem3  23000  ostth3  23003  ubthlem2  24407  minvecolem3  24412  minvecolem5  24417  pjhthlem1  24929  sqsscirc1  26472  zetacvg  27135  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem5  27153  lgamcvg2  27175  regamcl  27181  itggt0cn  28602  geomcau  28793  cntotbnd  28833  rrndstprj2  28868  irrapxlem5  29305  pell1qrgaplem  29352  pell14qrgapw  29355  pellqrex  29358  rpexpmord  29427  rmxypos  29428  stoweidlem3  29936  stoweidlem26  29959  wallispilem4  30001  wallispi  30003  wallispi2lem1  30004  stirlinglem1  30007  stirlinglem4  30010  stirlinglem10  30016  stirlinglem11  30017  stirlinglem12  30018  taupilemrplb  35920
  Copyright terms: Public domain W3C validator