Theorem rpge0d 13005

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5109  0cc0 11074   ≤ cle 11215  ℝ⁺crp 12957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-resscn 11131  ax-1cn 11132  ax-addrcl 11135  ax-rnegex 11145  ax-cnre 11147  ax-pre-lttri 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11216  df-mnf 11217  df-xr 11218  df-ltxr 11219  df-le 11220  df-rp 12958

This theorem is referenced by:  rprege0d  13008  rpexpmord  14139  01sqrexlem5  15218  isumrpcl  15815  isumltss  15820  harmonic  15831  expcnv  15836  prmreclem5  16897  prmreclem6  16898  4sqlem7  16921  nmoi2  24624  reperflem  24713  lebnumii  24871  nmoleub2lem3  25021  nmoleub3  25025  lmnn  25169  minveclem3  25335  pjthlem1  25343  ovoliunlem1  25409  vitalilem4  25518  vitali  25520  itg2const2  25648  itggt0  25751  lhop1lem  25924  plyeq0lem  26121  aalioulem4  26249  aaliou3lem2  26257  aaliou3lem3  26258  pserdvlem2  26344  abelthlem7  26354  pilem2  26368  pilem3  26369  divlogrlim  26550  logtayllem  26574  cxpge0  26598  divcxp  26602  cxpsqrtlem  26617  cxpsqrt  26618  abscxpbnd  26669  asinlem3  26787  leibpi  26858  birthdaylem3  26869  rlimcnp3  26883  cxplim  26888  rlimcxp  26890  cxp2limlem  26892  cxp2lim  26893  jensenlem2  26904  amgmlem  26906  emcllem2  26913  emcllem4  26915  emcllem6  26917  fsumharmonic  26928  zetacvg  26931  lgamgulmlem2  26946  lgamgulmlem3  26947  lgamgulmlem5  26949  lgamcvg2  26971  regamcl  26977  ftalem3  26991  ftalem5  26993  basellem6  27002  basellem8  27004  chtge0  27028  chtwordi  27072  chpval2  27135  chpchtsum  27136  chpub  27137  bposlem1  27201  bposlem2  27202  bposlem4  27204  bposlem5  27205  bposlem6  27206  bposlem7  27207  bposlem9  27209  lgsquadlem2  27298  chtppilimlem1  27390  chtppilimlem2  27391  chtppilim  27392  chpchtlim  27396  rplogsumlem1  27401  rplogsumlem2  27402  dchrisum0lem1a  27403  rpvmasumlem  27404  dchrisumlema  27405  2vmadivsumlem  27457  logdivbnd  27473  selberg3lem1  27474  selberg3lem2  27475  selberg4lem1  27477  pntrsumbnd2  27484  pntrlog2bndlem1  27494  pntrlog2bndlem2  27495  pntrlog2bndlem3  27496  pntrlog2bndlem4  27497  pntrlog2bndlem5  27498  pntrlog2bndlem6a  27499  pntrlog2bndlem6  27500  pntrlog2bnd  27501  pntibndlem2  27508  pntlemg  27515  pntlemk  27523  pntlem3  27526  pntleml  27528  ostth2lem1  27535  padicabv  27547  ostth2lem3  27552  ostth3  27555  nrt2irr  30408  ubthlem2  30806  minvecolem3  30811  minvecolem5  30816  pjhthlem1  31326  fsumub  32759  constrsqrtcl  33775  sqsscirc1  33904  omssubaddlem  34296  hgt750lemd  34645  logdivsqrle  34647  hgt750lem  34648  hgt750leme  34655  knoppndvlem18  36512  taupilemrplb  37303  poimirlem29  37638  itggt0cn  37679  geomcau  37748  cntotbnd  37785  rrndstprj2  37820  aks4d1p1p7  42057  2ap1caineq  42128  fltnltalem  42643  irrapxlem5  42807  pell1qrgaplem  42854  pell14qrgapw  42857  pellqrex  42860  rmxypos  42929  binomcxplemnotnn0  44338  recnnltrp  45366  rpgtrecnn  45369  stoweidlem3  45994  stoweidlem26  46017  wallispilem4  46059  wallispi  46061  wallispi2lem1  46062  stirlinglem1  46065  stirlinglem4  46068  stirlinglem10  46074  stirlinglem11  46075  stirlinglem12  46076  fourierdlem39  46137  fourierdlem42  46140  fourierdlem87  46184  fourierdlem107  46204  rrndistlt  46281  sge0rpcpnf  46412  ovnsubaddlem1  46561  hoidmvlelem2  46587  hoidmvlelem4  46589  ovolval5lem1  46643  vonioolem1  46671