Theorem rpge0d 12423

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5030  0cc0 10526   ≤ cle 10665  ℝ⁺crp 12377

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-1cn 10584  ax-addrcl 10587  ax-rnegex 10597  ax-cnre 10599  ax-pre-lttri 10600

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-rp 12378

This theorem is referenced by:  rprege0d  12426  rpexpmord  13528  sqrlem5  14598  isumrpcl  15190  isumltss  15195  harmonic  15206  expcnv  15211  prmreclem5  16246  prmreclem6  16247  4sqlem7  16270  nmoi2  23336  reperflem  23423  lebnumii  23571  nmoleub2lem3  23720  nmoleub3  23724  lmnn  23867  minveclem3  24033  pjthlem1  24041  ovoliunlem1  24106  vitalilem4  24215  vitali  24217  itg2const2  24345  itggt0  24447  lhop1lem  24616  plyeq0lem  24807  aalioulem4  24931  aaliou3lem2  24939  aaliou3lem3  24940  pserdvlem2  25023  abelthlem7  25033  pilem2  25047  pilem3  25048  divlogrlim  25226  logtayllem  25250  cxpge0  25274  divcxp  25278  cxpsqrtlem  25293  cxpsqrt  25294  abscxpbnd  25342  asinlem3  25457  leibpi  25528  birthdaylem3  25539  rlimcnp3  25553  cxplim  25557  rlimcxp  25559  cxp2limlem  25561  cxp2lim  25562  jensenlem2  25573  amgmlem  25575  emcllem2  25582  emcllem4  25584  emcllem6  25586  fsumharmonic  25597  zetacvg  25600  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem5  25618  lgamcvg2  25640  regamcl  25646  ftalem3  25660  ftalem5  25662  basellem6  25671  basellem8  25673  chtge0  25697  chtwordi  25741  chpval2  25802  chpchtsum  25803  chpub  25804  bposlem1  25868  bposlem2  25869  bposlem4  25871  bposlem5  25872  bposlem6  25873  bposlem7  25874  bposlem9  25876  lgsquadlem2  25965  chtppilimlem1  26057  chtppilimlem2  26058  chtppilim  26059  chpchtlim  26063  rplogsumlem1  26068  rplogsumlem2  26069  dchrisum0lem1a  26070  rpvmasumlem  26071  dchrisumlema  26072  2vmadivsumlem  26124  logdivbnd  26140  selberg3lem1  26141  selberg3lem2  26142  selberg4lem1  26144  pntrsumbnd2  26151  pntrlog2bndlem1  26161  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntrlog2bndlem6a  26166  pntrlog2bndlem6  26167  pntrlog2bnd  26168  pntibndlem2  26175  pntlemg  26182  pntlemk  26190  pntlem3  26193  pntleml  26195  ostth2lem1  26202  padicabv  26214  ostth2lem3  26219  ostth3  26222  ubthlem2  28654  minvecolem3  28659  minvecolem5  28664  pjhthlem1  29174  fsumub  30570  sqsscirc1  31261  omssubaddlem  31667  hgt750lemd  32029  logdivsqrle  32031  hgt750lem  32032  hgt750leme  32039  knoppndvlem18  33981  taupilemrplb  34734  poimirlem29  35086  itggt0cn  35127  geomcau  35197  cntotbnd  35234  rrndstprj2  35269  2ap1caineq  39349  fltnltalem  39618  irrapxlem5  39767  pell1qrgaplem  39814  pell14qrgapw  39817  pellqrex  39820  rmxypos  39888  binomcxplemnotnn0  41060  recnnltrp  42009  rpgtrecnn  42013  stoweidlem3  42645  stoweidlem26  42668  wallispilem4  42710  wallispi  42712  wallispi2lem1  42713  stirlinglem1  42716  stirlinglem4  42719  stirlinglem10  42725  stirlinglem11  42726  stirlinglem12  42727  fourierdlem39  42788  fourierdlem42  42791  fourierdlem87  42835  fourierdlem107  42855  rrndistlt  42932  sge0rpcpnf  43060  ovnsubaddlem1  43209  hoidmvlelem2  43235  hoidmvlelem4  43237  ovolval5lem1  43291  vonioolem1  43319