Theorem rpge0d 11876

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

Step	Hyp	Ref	Expression
1		rpred.1	. 2 |- ( ph -> A e. RR+ )
2		rpge0 11845	. 2 |- ( A e. RR+ -> 0 <_ A )
3	1, 2	syl 17	1 |- ( ph -> 0 <_ A )

Syntax hints:   -> wi 4   e. wcel 1990   class class class wbr 4653   0cc0 9936   <_ cle 10075   RR+crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-rp 11833

This theorem is referenced by:  rprege0d  11879  sqrlem5  13987  isumrpcl  14575  isumltss  14580  harmonic  14591  expcnv  14596  prmreclem5  15624  prmreclem6  15625  4sqlem7  15648  nmoi2  22534  reperflem  22621  lebnumii  22765  nmoleub2lem3  22915  nmoleub3  22919  lmnn  23061  minveclem3  23200  pjthlem1  23208  ovoliunlem1  23270  vitalilem4  23380  vitali  23382  itg2const2  23508  itggt0  23608  lhop1lem  23776  plyeq0lem  23966  aalioulem4  24090  aaliou3lem2  24098  aaliou3lem3  24099  pserdvlem2  24182  abelthlem7  24192  pilem2  24206  pilem3  24207  divlogrlim  24381  logtayllem  24405  cxpge0  24429  divcxp  24433  cxpsqrtlem  24448  cxpsqrt  24449  abscxpbnd  24494  asinlem3  24598  leibpi  24669  birthdaylem3  24680  rlimcnp3  24694  cxplim  24698  rlimcxp  24700  cxp2limlem  24702  cxp2lim  24703  jensenlem2  24714  amgmlem  24716  emcllem2  24723  emcllem4  24725  emcllem6  24727  fsumharmonic  24738  zetacvg  24741  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem5  24759  lgamcvg2  24781  regamcl  24787  ftalem3  24801  ftalem5  24803  basellem6  24812  basellem8  24814  chtge0  24838  chtwordi  24882  chpval2  24943  chpchtsum  24944  chpub  24945  bposlem1  25009  bposlem2  25010  bposlem4  25012  bposlem5  25013  bposlem6  25014  bposlem7  25015  bposlem9  25017  lgsquadlem2  25106  chtppilimlem1  25162  chtppilimlem2  25163  chtppilim  25164  chpchtlim  25168  rplogsumlem1  25173  rplogsumlem2  25174  dchrisum0lem1a  25175  rpvmasumlem  25176  dchrisumlema  25177  2vmadivsumlem  25229  logdivbnd  25245  selberg3lem1  25246  selberg3lem2  25247  selberg4lem1  25249  pntrsumbnd2  25256  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6a  25271  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntibndlem2  25280  pntlemg  25287  pntlemk  25295  pntlem3  25298  pntleml  25300  ostth2lem1  25307  padicabv  25319  ostth2lem3  25324  ostth3  25327  ubthlem2  27727  minvecolem3  27732  minvecolem5  27737  pjhthlem1  28250  fsumub  29574  sqsscirc1  29954  omssubaddlem  30361  hgt750lemd  30726  logdivsqrle  30728  hgt750lem  30729  hgt750leme  30736  knoppndvlem18  32520  taupilemrplb  33166  poimirlem29  33438  itggt0cn  33482  geomcau  33555  cntotbnd  33595  rrndstprj2  33630  irrapxlem5  37390  pell1qrgaplem  37437  pell14qrgapw  37440  pellqrex  37443  rpexpmord  37513  rmxypos  37514  binomcxplemnotnn0  38555  recnnltrp  39593  rpgtrecnn  39597  stoweidlem3  40220  stoweidlem26  40243  wallispilem4  40285  wallispi  40287  wallispi2lem1  40288  stirlinglem1  40291  stirlinglem4  40294  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  fourierdlem39  40363  fourierdlem42  40366  fourierdlem87  40410  fourierdlem107  40430  rrndistlt  40510  sge0rpcpnf  40638  ovnsubaddlem1  40784  hoidmvlelem2  40810  hoidmvlelem4  40812  ovolval5lem1  40866  vonioolem1  40894