Theorem rpge0d 12705

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5070  0cc0 10802   ≤ cle 10941  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-addrcl 10863  ax-rnegex 10873  ax-cnre 10875  ax-pre-lttri 10876

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-rp 12660

This theorem is referenced by:  rprege0d  12708  rpexpmord  13814  sqrlem5  14886  isumrpcl  15483  isumltss  15488  harmonic  15499  expcnv  15504  prmreclem5  16549  prmreclem6  16550  4sqlem7  16573  nmoi2  23800  reperflem  23887  lebnumii  24035  nmoleub2lem3  24184  nmoleub3  24188  lmnn  24332  minveclem3  24498  pjthlem1  24506  ovoliunlem1  24571  vitalilem4  24680  vitali  24682  itg2const2  24811  itggt0  24913  lhop1lem  25082  plyeq0lem  25276  aalioulem4  25400  aaliou3lem2  25408  aaliou3lem3  25409  pserdvlem2  25492  abelthlem7  25502  pilem2  25516  pilem3  25517  divlogrlim  25695  logtayllem  25719  cxpge0  25743  divcxp  25747  cxpsqrtlem  25762  cxpsqrt  25763  abscxpbnd  25811  asinlem3  25926  leibpi  25997  birthdaylem3  26008  rlimcnp3  26022  cxplim  26026  rlimcxp  26028  cxp2limlem  26030  cxp2lim  26031  jensenlem2  26042  amgmlem  26044  emcllem2  26051  emcllem4  26053  emcllem6  26055  fsumharmonic  26066  zetacvg  26069  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem5  26087  lgamcvg2  26109  regamcl  26115  ftalem3  26129  ftalem5  26131  basellem6  26140  basellem8  26142  chtge0  26166  chtwordi  26210  chpval2  26271  chpchtsum  26272  chpub  26273  bposlem1  26337  bposlem2  26338  bposlem4  26340  bposlem5  26341  bposlem6  26342  bposlem7  26343  bposlem9  26345  lgsquadlem2  26434  chtppilimlem1  26526  chtppilimlem2  26527  chtppilim  26528  chpchtlim  26532  rplogsumlem1  26537  rplogsumlem2  26538  dchrisum0lem1a  26539  rpvmasumlem  26540  dchrisumlema  26541  2vmadivsumlem  26593  logdivbnd  26609  selberg3lem1  26610  selberg3lem2  26611  selberg4lem1  26613  pntrsumbnd2  26620  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6a  26635  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntibndlem2  26644  pntlemg  26651  pntlemk  26659  pntlem3  26662  pntleml  26664  ostth2lem1  26671  padicabv  26683  ostth2lem3  26688  ostth3  26691  ubthlem2  29134  minvecolem3  29139  minvecolem5  29144  pjhthlem1  29654  fsumub  31044  sqsscirc1  31760  omssubaddlem  32166  hgt750lemd  32528  logdivsqrle  32530  hgt750lem  32531  hgt750leme  32538  knoppndvlem18  34636  taupilemrplb  35418  poimirlem29  35733  itggt0cn  35774  geomcau  35844  cntotbnd  35881  rrndstprj2  35916  aks4d1p1p7  40010  2ap1caineq  40029  fltnltalem  40415  irrapxlem5  40564  pell1qrgaplem  40611  pell14qrgapw  40614  pellqrex  40617  rmxypos  40685  binomcxplemnotnn0  41863  recnnltrp  42806  rpgtrecnn  42809  stoweidlem3  43434  stoweidlem26  43457  wallispilem4  43499  wallispi  43501  wallispi2lem1  43502  stirlinglem1  43505  stirlinglem4  43508  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  fourierdlem39  43577  fourierdlem42  43580  fourierdlem87  43624  fourierdlem107  43644  rrndistlt  43721  sge0rpcpnf  43849  ovnsubaddlem1  43998  hoidmvlelem2  44024  hoidmvlelem4  44026  ovolval5lem1  44080  vonioolem1  44108