Theorem rpge0d 13079

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 13046	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5148  0cc0 11153   ≤ cle 11294  ℝ⁺crp 13032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-1cn 11211  ax-addrcl 11214  ax-rnegex 11224  ax-cnre 11226  ax-pre-lttri 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-rp 13033

This theorem is referenced by:  rprege0d  13082  rpexpmord  14205  01sqrexlem5  15282  isumrpcl  15876  isumltss  15881  harmonic  15892  expcnv  15897  prmreclem5  16954  prmreclem6  16955  4sqlem7  16978  nmoi2  24767  reperflem  24854  lebnumii  25012  nmoleub2lem3  25162  nmoleub3  25166  lmnn  25311  minveclem3  25477  pjthlem1  25485  ovoliunlem1  25551  vitalilem4  25660  vitali  25662  itg2const2  25791  itggt0  25894  lhop1lem  26067  plyeq0lem  26264  aalioulem4  26392  aaliou3lem2  26400  aaliou3lem3  26401  pserdvlem2  26487  abelthlem7  26497  pilem2  26511  pilem3  26512  divlogrlim  26692  logtayllem  26716  cxpge0  26740  divcxp  26744  cxpsqrtlem  26759  cxpsqrt  26760  abscxpbnd  26811  asinlem3  26929  leibpi  27000  birthdaylem3  27011  rlimcnp3  27025  cxplim  27030  rlimcxp  27032  cxp2limlem  27034  cxp2lim  27035  jensenlem2  27046  amgmlem  27048  emcllem2  27055  emcllem4  27057  emcllem6  27059  fsumharmonic  27070  zetacvg  27073  lgamgulmlem2  27088  lgamgulmlem3  27089  lgamgulmlem5  27091  lgamcvg2  27113  regamcl  27119  ftalem3  27133  ftalem5  27135  basellem6  27144  basellem8  27146  chtge0  27170  chtwordi  27214  chpval2  27277  chpchtsum  27278  chpub  27279  bposlem1  27343  bposlem2  27344  bposlem4  27346  bposlem5  27347  bposlem6  27348  bposlem7  27349  bposlem9  27351  lgsquadlem2  27440  chtppilimlem1  27532  chtppilimlem2  27533  chtppilim  27534  chpchtlim  27538  rplogsumlem1  27543  rplogsumlem2  27544  dchrisum0lem1a  27545  rpvmasumlem  27546  dchrisumlema  27547  2vmadivsumlem  27599  logdivbnd  27615  selberg3lem1  27616  selberg3lem2  27617  selberg4lem1  27619  pntrsumbnd2  27626  pntrlog2bndlem1  27636  pntrlog2bndlem2  27637  pntrlog2bndlem3  27638  pntrlog2bndlem4  27639  pntrlog2bndlem5  27640  pntrlog2bndlem6a  27641  pntrlog2bndlem6  27642  pntrlog2bnd  27643  pntibndlem2  27650  pntlemg  27657  pntlemk  27665  pntlem3  27668  pntleml  27670  ostth2lem1  27677  padicabv  27689  ostth2lem3  27694  ostth3  27697  nrt2irr  30502  ubthlem2  30900  minvecolem3  30905  minvecolem5  30910  pjhthlem1  31420  fsumub  32835  sqsscirc1  33869  omssubaddlem  34281  hgt750lemd  34642  logdivsqrle  34644  hgt750lem  34645  hgt750leme  34652  knoppndvlem18  36512  taupilemrplb  37303  poimirlem29  37636  itggt0cn  37677  geomcau  37746  cntotbnd  37783  rrndstprj2  37818  aks4d1p1p7  42056  2ap1caineq  42127  fltnltalem  42649  irrapxlem5  42814  pell1qrgaplem  42861  pell14qrgapw  42864  pellqrex  42867  rmxypos  42936  binomcxplemnotnn0  44352  recnnltrp  45327  rpgtrecnn  45330  stoweidlem3  45959  stoweidlem26  45982  wallispilem4  46024  wallispi  46026  wallispi2lem1  46027  stirlinglem1  46030  stirlinglem4  46033  stirlinglem10  46039  stirlinglem11  46040  stirlinglem12  46041  fourierdlem39  46102  fourierdlem42  46105  fourierdlem87  46149  fourierdlem107  46169  rrndistlt  46246  sge0rpcpnf  46377  ovnsubaddlem1  46526  hoidmvlelem2  46552  hoidmvlelem4  46554  ovolval5lem1  46608  vonioolem1  46636