Theorem rpge0d 12776

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5074  0cc0 10871   ≤ cle 11010  ℝ⁺crp 12730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-addrcl 10932  ax-rnegex 10942  ax-cnre 10944  ax-pre-lttri 10945

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-rp 12731

This theorem is referenced by:  rprege0d  12779  rpexpmord  13886  sqrlem5  14958  isumrpcl  15555  isumltss  15560  harmonic  15571  expcnv  15576  prmreclem5  16621  prmreclem6  16622  4sqlem7  16645  nmoi2  23894  reperflem  23981  lebnumii  24129  nmoleub2lem3  24278  nmoleub3  24282  lmnn  24427  minveclem3  24593  pjthlem1  24601  ovoliunlem1  24666  vitalilem4  24775  vitali  24777  itg2const2  24906  itggt0  25008  lhop1lem  25177  plyeq0lem  25371  aalioulem4  25495  aaliou3lem2  25503  aaliou3lem3  25504  pserdvlem2  25587  abelthlem7  25597  pilem2  25611  pilem3  25612  divlogrlim  25790  logtayllem  25814  cxpge0  25838  divcxp  25842  cxpsqrtlem  25857  cxpsqrt  25858  abscxpbnd  25906  asinlem3  26021  leibpi  26092  birthdaylem3  26103  rlimcnp3  26117  cxplim  26121  rlimcxp  26123  cxp2limlem  26125  cxp2lim  26126  jensenlem2  26137  amgmlem  26139  emcllem2  26146  emcllem4  26148  emcllem6  26150  fsumharmonic  26161  zetacvg  26164  lgamgulmlem2  26179  lgamgulmlem3  26180  lgamgulmlem5  26182  lgamcvg2  26204  regamcl  26210  ftalem3  26224  ftalem5  26226  basellem6  26235  basellem8  26237  chtge0  26261  chtwordi  26305  chpval2  26366  chpchtsum  26367  chpub  26368  bposlem1  26432  bposlem2  26433  bposlem4  26435  bposlem5  26436  bposlem6  26437  bposlem7  26438  bposlem9  26440  lgsquadlem2  26529  chtppilimlem1  26621  chtppilimlem2  26622  chtppilim  26623  chpchtlim  26627  rplogsumlem1  26632  rplogsumlem2  26633  dchrisum0lem1a  26634  rpvmasumlem  26635  dchrisumlema  26636  2vmadivsumlem  26688  logdivbnd  26704  selberg3lem1  26705  selberg3lem2  26706  selberg4lem1  26708  pntrsumbnd2  26715  pntrlog2bndlem1  26725  pntrlog2bndlem2  26726  pntrlog2bndlem3  26727  pntrlog2bndlem4  26728  pntrlog2bndlem5  26729  pntrlog2bndlem6a  26730  pntrlog2bndlem6  26731  pntrlog2bnd  26732  pntibndlem2  26739  pntlemg  26746  pntlemk  26754  pntlem3  26757  pntleml  26759  ostth2lem1  26766  padicabv  26778  ostth2lem3  26783  ostth3  26786  ubthlem2  29233  minvecolem3  29238  minvecolem5  29243  pjhthlem1  29753  fsumub  31142  sqsscirc1  31858  omssubaddlem  32266  hgt750lemd  32628  logdivsqrle  32630  hgt750lem  32631  hgt750leme  32638  knoppndvlem18  34709  taupilemrplb  35491  poimirlem29  35806  itggt0cn  35847  geomcau  35917  cntotbnd  35954  rrndstprj2  35989  aks4d1p1p7  40082  2ap1caineq  40101  fltnltalem  40499  irrapxlem5  40648  pell1qrgaplem  40695  pell14qrgapw  40698  pellqrex  40701  rmxypos  40769  binomcxplemnotnn0  41974  recnnltrp  42916  rpgtrecnn  42919  stoweidlem3  43544  stoweidlem26  43567  wallispilem4  43609  wallispi  43611  wallispi2lem1  43612  stirlinglem1  43615  stirlinglem4  43618  stirlinglem10  43624  stirlinglem11  43625  stirlinglem12  43626  fourierdlem39  43687  fourierdlem42  43690  fourierdlem87  43734  fourierdlem107  43754  rrndistlt  43831  sge0rpcpnf  43959  ovnsubaddlem1  44108  hoidmvlelem2  44134  hoidmvlelem4  44136  ovolval5lem1  44190  vonioolem1  44218