Theorem rpge0d 12970

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5110  0cc0 11060   ≤ cle 11199  ℝ⁺crp 12924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-resscn 11117  ax-1cn 11118  ax-addrcl 11121  ax-rnegex 11131  ax-cnre 11133  ax-pre-lttri 11134

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-rp 12925

This theorem is referenced by:  rprege0d  12973  rpexpmord  14083  01sqrexlem5  15143  isumrpcl  15739  isumltss  15744  harmonic  15755  expcnv  15760  prmreclem5  16803  prmreclem6  16804  4sqlem7  16827  nmoi2  24131  reperflem  24218  lebnumii  24366  nmoleub2lem3  24515  nmoleub3  24519  lmnn  24664  minveclem3  24830  pjthlem1  24838  ovoliunlem1  24903  vitalilem4  25012  vitali  25014  itg2const2  25143  itggt0  25245  lhop1lem  25414  plyeq0lem  25608  aalioulem4  25732  aaliou3lem2  25740  aaliou3lem3  25741  pserdvlem2  25824  abelthlem7  25834  pilem2  25848  pilem3  25849  divlogrlim  26027  logtayllem  26051  cxpge0  26075  divcxp  26079  cxpsqrtlem  26094  cxpsqrt  26095  abscxpbnd  26143  asinlem3  26258  leibpi  26329  birthdaylem3  26340  rlimcnp3  26354  cxplim  26358  rlimcxp  26360  cxp2limlem  26362  cxp2lim  26363  jensenlem2  26374  amgmlem  26376  emcllem2  26383  emcllem4  26385  emcllem6  26387  fsumharmonic  26398  zetacvg  26401  lgamgulmlem2  26416  lgamgulmlem3  26417  lgamgulmlem5  26419  lgamcvg2  26441  regamcl  26447  ftalem3  26461  ftalem5  26463  basellem6  26472  basellem8  26474  chtge0  26498  chtwordi  26542  chpval2  26603  chpchtsum  26604  chpub  26605  bposlem1  26669  bposlem2  26670  bposlem4  26672  bposlem5  26673  bposlem6  26674  bposlem7  26675  bposlem9  26677  lgsquadlem2  26766  chtppilimlem1  26858  chtppilimlem2  26859  chtppilim  26860  chpchtlim  26864  rplogsumlem1  26869  rplogsumlem2  26870  dchrisum0lem1a  26871  rpvmasumlem  26872  dchrisumlema  26873  2vmadivsumlem  26925  logdivbnd  26941  selberg3lem1  26942  selberg3lem2  26943  selberg4lem1  26945  pntrsumbnd2  26952  pntrlog2bndlem1  26962  pntrlog2bndlem2  26963  pntrlog2bndlem3  26964  pntrlog2bndlem4  26965  pntrlog2bndlem5  26966  pntrlog2bndlem6a  26967  pntrlog2bndlem6  26968  pntrlog2bnd  26969  pntibndlem2  26976  pntlemg  26983  pntlemk  26991  pntlem3  26994  pntleml  26996  ostth2lem1  27003  padicabv  27015  ostth2lem3  27020  ostth3  27023  ubthlem2  29876  minvecolem3  29881  minvecolem5  29886  pjhthlem1  30396  fsumub  31794  sqsscirc1  32578  omssubaddlem  32988  hgt750lemd  33350  logdivsqrle  33352  hgt750lem  33353  hgt750leme  33360  knoppndvlem18  35068  taupilemrplb  35864  poimirlem29  36180  itggt0cn  36221  geomcau  36291  cntotbnd  36328  rrndstprj2  36363  aks4d1p1p7  40604  2ap1caineq  40626  fltnltalem  41058  irrapxlem5  41207  pell1qrgaplem  41254  pell14qrgapw  41257  pellqrex  41260  rmxypos  41329  binomcxplemnotnn0  42758  recnnltrp  43732  rpgtrecnn  43735  stoweidlem3  44364  stoweidlem26  44387  wallispilem4  44429  wallispi  44431  wallispi2lem1  44432  stirlinglem1  44435  stirlinglem4  44438  stirlinglem10  44444  stirlinglem11  44445  stirlinglem12  44446  fourierdlem39  44507  fourierdlem42  44510  fourierdlem87  44554  fourierdlem107  44574  rrndistlt  44651  sge0rpcpnf  44782  ovnsubaddlem1  44931  hoidmvlelem2  44957  hoidmvlelem4  44959  ovolval5lem1  45013  vonioolem1  45041