Theorem rpge0d 12775

Description: A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpge0d	⊢ (𝜑 → 0 ≤ 𝐴)

Proof of Theorem rpge0d

Step	Hyp	Ref	Expression
1		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpge0 12742	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2110   class class class wbr 5079  0cc0 10872   ≤ cle 11011  ℝ⁺crp 12729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-resscn 10929  ax-1cn 10930  ax-addrcl 10933  ax-rnegex 10943  ax-cnre 10945  ax-pre-lttri 10946

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-nel 3052  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-er 8481  df-en 8717  df-dom 8718  df-sdom 8719  df-pnf 11012  df-mnf 11013  df-xr 11014  df-ltxr 11015  df-le 11016  df-rp 12730

This theorem is referenced by:  rprege0d  12778  rpexpmord  13884  sqrlem5  14956  isumrpcl  15553  isumltss  15558  harmonic  15569  expcnv  15574  prmreclem5  16619  prmreclem6  16620  4sqlem7  16643  nmoi2  23892  reperflem  23979  lebnumii  24127  nmoleub2lem3  24276  nmoleub3  24280  lmnn  24425  minveclem3  24591  pjthlem1  24599  ovoliunlem1  24664  vitalilem4  24773  vitali  24775  itg2const2  24904  itggt0  25006  lhop1lem  25175  plyeq0lem  25369  aalioulem4  25493  aaliou3lem2  25501  aaliou3lem3  25502  pserdvlem2  25585  abelthlem7  25595  pilem2  25609  pilem3  25610  divlogrlim  25788  logtayllem  25812  cxpge0  25836  divcxp  25840  cxpsqrtlem  25855  cxpsqrt  25856  abscxpbnd  25904  asinlem3  26019  leibpi  26090  birthdaylem3  26101  rlimcnp3  26115  cxplim  26119  rlimcxp  26121  cxp2limlem  26123  cxp2lim  26124  jensenlem2  26135  amgmlem  26137  emcllem2  26144  emcllem4  26146  emcllem6  26148  fsumharmonic  26159  zetacvg  26162  lgamgulmlem2  26177  lgamgulmlem3  26178  lgamgulmlem5  26180  lgamcvg2  26202  regamcl  26208  ftalem3  26222  ftalem5  26224  basellem6  26233  basellem8  26235  chtge0  26259  chtwordi  26303  chpval2  26364  chpchtsum  26365  chpub  26366  bposlem1  26430  bposlem2  26431  bposlem4  26433  bposlem5  26434  bposlem6  26435  bposlem7  26436  bposlem9  26438  lgsquadlem2  26527  chtppilimlem1  26619  chtppilimlem2  26620  chtppilim  26621  chpchtlim  26625  rplogsumlem1  26630  rplogsumlem2  26631  dchrisum0lem1a  26632  rpvmasumlem  26633  dchrisumlema  26634  2vmadivsumlem  26686  logdivbnd  26702  selberg3lem1  26703  selberg3lem2  26704  selberg4lem1  26706  pntrsumbnd2  26713  pntrlog2bndlem1  26723  pntrlog2bndlem2  26724  pntrlog2bndlem3  26725  pntrlog2bndlem4  26726  pntrlog2bndlem5  26727  pntrlog2bndlem6a  26728  pntrlog2bndlem6  26729  pntrlog2bnd  26730  pntibndlem2  26737  pntlemg  26744  pntlemk  26752  pntlem3  26755  pntleml  26757  ostth2lem1  26764  padicabv  26776  ostth2lem3  26781  ostth3  26784  ubthlem2  29229  minvecolem3  29234  minvecolem5  29239  pjhthlem1  29749  fsumub  31138  sqsscirc1  31854  omssubaddlem  32262  hgt750lemd  32624  logdivsqrle  32626  hgt750lem  32627  hgt750leme  32634  knoppndvlem18  34705  taupilemrplb  35487  poimirlem29  35802  itggt0cn  35843  geomcau  35913  cntotbnd  35950  rrndstprj2  35985  aks4d1p1p7  40079  2ap1caineq  40098  fltnltalem  40496  irrapxlem5  40645  pell1qrgaplem  40692  pell14qrgapw  40695  pellqrex  40698  rmxypos  40766  binomcxplemnotnn0  41944  recnnltrp  42887  rpgtrecnn  42890  stoweidlem3  43515  stoweidlem26  43538  wallispilem4  43580  wallispi  43582  wallispi2lem1  43583  stirlinglem1  43586  stirlinglem4  43589  stirlinglem10  43595  stirlinglem11  43596  stirlinglem12  43597  fourierdlem39  43658  fourierdlem42  43661  fourierdlem87  43705  fourierdlem107  43725  rrndistlt  43802  sge0rpcpnf  43930  ovnsubaddlem1  44079  hoidmvlelem2  44105  hoidmvlelem4  44107  ovolval5lem1  44161  vonioolem1  44189