Theorem rpge0d 12951

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5096  0cc0 11024   ≤ cle 11165  ℝ⁺crp 12903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-addrcl 11085  ax-rnegex 11095  ax-cnre 11097  ax-pre-lttri 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-rp 12904

This theorem is referenced by:  rprege0d  12954  rpexpmord  14089  01sqrexlem5  15167  isumrpcl  15764  isumltss  15769  harmonic  15780  expcnv  15785  prmreclem5  16846  prmreclem6  16847  4sqlem7  16870  nmoi2  24672  reperflem  24761  lebnumii  24919  nmoleub2lem3  25069  nmoleub3  25073  lmnn  25217  minveclem3  25383  pjthlem1  25391  ovoliunlem1  25457  vitalilem4  25566  vitali  25568  itg2const2  25696  itggt0  25799  lhop1lem  25972  plyeq0lem  26169  aalioulem4  26297  aaliou3lem2  26305  aaliou3lem3  26306  pserdvlem2  26392  abelthlem7  26402  pilem2  26416  pilem3  26417  divlogrlim  26598  logtayllem  26622  cxpge0  26646  divcxp  26650  cxpsqrtlem  26665  cxpsqrt  26666  abscxpbnd  26717  asinlem3  26835  leibpi  26906  birthdaylem3  26917  rlimcnp3  26931  cxplim  26936  rlimcxp  26938  cxp2limlem  26940  cxp2lim  26941  jensenlem2  26952  amgmlem  26954  emcllem2  26961  emcllem4  26963  emcllem6  26965  fsumharmonic  26976  zetacvg  26979  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamgulmlem5  26997  lgamcvg2  27019  regamcl  27025  ftalem3  27039  ftalem5  27041  basellem6  27050  basellem8  27052  chtge0  27076  chtwordi  27120  chpval2  27183  chpchtsum  27184  chpub  27185  bposlem1  27249  bposlem2  27250  bposlem4  27252  bposlem5  27253  bposlem6  27254  bposlem7  27255  bposlem9  27257  lgsquadlem2  27346  chtppilimlem1  27438  chtppilimlem2  27439  chtppilim  27440  chpchtlim  27444  rplogsumlem1  27449  rplogsumlem2  27450  dchrisum0lem1a  27451  rpvmasumlem  27452  dchrisumlema  27453  2vmadivsumlem  27505  logdivbnd  27521  selberg3lem1  27522  selberg3lem2  27523  selberg4lem1  27525  pntrsumbnd2  27532  pntrlog2bndlem1  27542  pntrlog2bndlem2  27543  pntrlog2bndlem3  27544  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntrlog2bndlem6a  27547  pntrlog2bndlem6  27548  pntrlog2bnd  27549  pntibndlem2  27556  pntlemg  27563  pntlemk  27571  pntlem3  27574  pntleml  27576  ostth2lem1  27583  padicabv  27595  ostth2lem3  27600  ostth3  27603  nrt2irr  30497  ubthlem2  30895  minvecolem3  30900  minvecolem5  30905  pjhthlem1  31415  fsumub  32858  constrsqrtcl  33885  sqsscirc1  34014  omssubaddlem  34405  hgt750lemd  34754  logdivsqrle  34756  hgt750lem  34757  hgt750leme  34764  knoppndvlem18  36672  taupilemrplb  37464  poimirlem29  37789  itggt0cn  37830  geomcau  37899  cntotbnd  37936  rrndstprj2  37971  aks4d1p1p7  42267  2ap1caineq  42338  fltnltalem  42847  irrapxlem5  43010  pell1qrgaplem  43057  pell14qrgapw  43060  pellqrex  43063  rmxypos  43131  binomcxplemnotnn0  44539  recnnltrp  45563  rpgtrecnn  45566  stoweidlem3  46189  stoweidlem26  46212  wallispilem4  46254  wallispi  46256  wallispi2lem1  46257  stirlinglem1  46260  stirlinglem4  46263  stirlinglem10  46269  stirlinglem11  46270  stirlinglem12  46271  fourierdlem39  46332  fourierdlem42  46335  fourierdlem87  46379  fourierdlem107  46399  rrndistlt  46476  sge0rpcpnf  46607  ovnsubaddlem1  46756  hoidmvlelem2  46782  hoidmvlelem4  46784  ovolval5lem1  46838  vonioolem1  46866