Theorem rpge0d 12981

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  0cc0 11029   ≤ cle 11171  ℝ⁺crp 12933

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102  ax-pre-lttri 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-rp 12934

This theorem is referenced by:  rprege0d  12984  rpexpmord  14121  01sqrexlem5  15199  isumrpcl  15799  isumltss  15804  harmonic  15815  expcnv  15820  prmreclem5  16882  prmreclem6  16883  4sqlem7  16906  nmoi2  24705  reperflem  24794  lebnumii  24943  nmoleub2lem3  25092  nmoleub3  25096  lmnn  25240  minveclem3  25406  pjthlem1  25414  ovoliunlem1  25479  vitalilem4  25588  vitali  25590  itg2const2  25718  itggt0  25821  lhop1lem  25990  plyeq0lem  26185  aalioulem4  26312  aaliou3lem2  26320  aaliou3lem3  26321  pserdvlem2  26406  abelthlem7  26416  pilem2  26430  pilem3  26431  divlogrlim  26612  logtayllem  26636  cxpge0  26660  divcxp  26664  cxpsqrtlem  26679  cxpsqrt  26680  abscxpbnd  26730  asinlem3  26848  leibpi  26919  birthdaylem3  26930  rlimcnp3  26944  cxplim  26949  rlimcxp  26951  cxp2limlem  26953  cxp2lim  26954  jensenlem2  26965  amgmlem  26967  emcllem2  26974  emcllem4  26976  emcllem6  26978  fsumharmonic  26989  zetacvg  26992  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem5  27010  lgamcvg2  27032  regamcl  27038  ftalem3  27052  ftalem5  27054  basellem6  27063  basellem8  27065  chtge0  27089  chtwordi  27133  chpval2  27195  chpchtsum  27196  chpub  27197  bposlem1  27261  bposlem2  27262  bposlem4  27264  bposlem5  27265  bposlem6  27266  bposlem7  27267  bposlem9  27269  lgsquadlem2  27358  chtppilimlem1  27450  chtppilimlem2  27451  chtppilim  27452  chpchtlim  27456  rplogsumlem1  27461  rplogsumlem2  27462  dchrisum0lem1a  27463  rpvmasumlem  27464  dchrisumlema  27465  2vmadivsumlem  27517  logdivbnd  27533  selberg3lem1  27534  selberg3lem2  27535  selberg4lem1  27537  pntrsumbnd2  27544  pntrlog2bndlem1  27554  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntrlog2bndlem6a  27559  pntrlog2bndlem6  27560  pntrlog2bnd  27561  pntibndlem2  27568  pntlemg  27575  pntlemk  27583  pntlem3  27586  pntleml  27588  ostth2lem1  27595  padicabv  27607  ostth2lem3  27612  ostth3  27615  nrt2irr  30558  ubthlem2  30957  minvecolem3  30962  minvecolem5  30967  pjhthlem1  31477  fsumub  32916  constrsqrtcl  33939  sqsscirc1  34068  omssubaddlem  34459  hgt750lemd  34808  logdivsqrle  34810  hgt750lem  34811  hgt750leme  34818  knoppndvlem18  36805  taupilemrplb  37650  poimirlem29  37984  itggt0cn  38025  geomcau  38094  cntotbnd  38131  rrndstprj2  38166  aks4d1p1p7  42527  2ap1caineq  42598  fltnltalem  43109  irrapxlem5  43272  pell1qrgaplem  43319  pell14qrgapw  43322  pellqrex  43325  rmxypos  43393  binomcxplemnotnn0  44801  recnnltrp  45824  rpgtrecnn  45827  stoweidlem3  46449  stoweidlem26  46472  wallispilem4  46514  wallispi  46516  wallispi2lem1  46517  stirlinglem1  46520  stirlinglem4  46523  stirlinglem10  46529  stirlinglem11  46530  stirlinglem12  46531  fourierdlem39  46592  fourierdlem42  46595  fourierdlem87  46639  fourierdlem107  46659  rrndistlt  46736  sge0rpcpnf  46867  ovnsubaddlem1  47016  hoidmvlelem2  47042  hoidmvlelem4  47044  ovolval5lem1  47098  vonioolem1  47126