Theorem rpge0d 12938

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5089  0cc0 11006   ≤ cle 11147  ℝ⁺crp 12890

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-addrcl 11067  ax-rnegex 11077  ax-cnre 11079  ax-pre-lttri 11080

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-rp 12891

This theorem is referenced by:  rprege0d  12941  rpexpmord  14075  01sqrexlem5  15153  isumrpcl  15750  isumltss  15755  harmonic  15766  expcnv  15771  prmreclem5  16832  prmreclem6  16833  4sqlem7  16856  nmoi2  24645  reperflem  24734  lebnumii  24892  nmoleub2lem3  25042  nmoleub3  25046  lmnn  25190  minveclem3  25356  pjthlem1  25364  ovoliunlem1  25430  vitalilem4  25539  vitali  25541  itg2const2  25669  itggt0  25772  lhop1lem  25945  plyeq0lem  26142  aalioulem4  26270  aaliou3lem2  26278  aaliou3lem3  26279  pserdvlem2  26365  abelthlem7  26375  pilem2  26389  pilem3  26390  divlogrlim  26571  logtayllem  26595  cxpge0  26619  divcxp  26623  cxpsqrtlem  26638  cxpsqrt  26639  abscxpbnd  26690  asinlem3  26808  leibpi  26879  birthdaylem3  26890  rlimcnp3  26904  cxplim  26909  rlimcxp  26911  cxp2limlem  26913  cxp2lim  26914  jensenlem2  26925  amgmlem  26927  emcllem2  26934  emcllem4  26936  emcllem6  26938  fsumharmonic  26949  zetacvg  26952  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamgulmlem5  26970  lgamcvg2  26992  regamcl  26998  ftalem3  27012  ftalem5  27014  basellem6  27023  basellem8  27025  chtge0  27049  chtwordi  27093  chpval2  27156  chpchtsum  27157  chpub  27158  bposlem1  27222  bposlem2  27223  bposlem4  27225  bposlem5  27226  bposlem6  27227  bposlem7  27228  bposlem9  27230  lgsquadlem2  27319  chtppilimlem1  27411  chtppilimlem2  27412  chtppilim  27413  chpchtlim  27417  rplogsumlem1  27422  rplogsumlem2  27423  dchrisum0lem1a  27424  rpvmasumlem  27425  dchrisumlema  27426  2vmadivsumlem  27478  logdivbnd  27494  selberg3lem1  27495  selberg3lem2  27496  selberg4lem1  27498  pntrsumbnd2  27505  pntrlog2bndlem1  27515  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6a  27520  pntrlog2bndlem6  27521  pntrlog2bnd  27522  pntibndlem2  27529  pntlemg  27536  pntlemk  27544  pntlem3  27547  pntleml  27549  ostth2lem1  27556  padicabv  27568  ostth2lem3  27573  ostth3  27576  nrt2irr  30453  ubthlem2  30851  minvecolem3  30856  minvecolem5  30861  pjhthlem1  31371  fsumub  32811  constrsqrtcl  33792  sqsscirc1  33921  omssubaddlem  34312  hgt750lemd  34661  logdivsqrle  34663  hgt750lem  34664  hgt750leme  34671  knoppndvlem18  36571  taupilemrplb  37362  poimirlem29  37697  itggt0cn  37738  geomcau  37807  cntotbnd  37844  rrndstprj2  37879  aks4d1p1p7  42115  2ap1caineq  42186  fltnltalem  42703  irrapxlem5  42867  pell1qrgaplem  42914  pell14qrgapw  42917  pellqrex  42920  rmxypos  42988  binomcxplemnotnn0  44397  recnnltrp  45423  rpgtrecnn  45426  stoweidlem3  46049  stoweidlem26  46072  wallispilem4  46114  wallispi  46116  wallispi2lem1  46117  stirlinglem1  46120  stirlinglem4  46123  stirlinglem10  46129  stirlinglem11  46130  stirlinglem12  46131  fourierdlem39  46192  fourierdlem42  46195  fourierdlem87  46239  fourierdlem107  46259  rrndistlt  46336  sge0rpcpnf  46467  ovnsubaddlem1  46616  hoidmvlelem2  46642  hoidmvlelem4  46644  ovolval5lem1  46698  vonioolem1  46726