Theorem rpge0d 13059

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  0cc0 11095   ≤ cle 11239  ℝ⁺crp 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-addrcl 11156  ax-rnegex 11166  ax-cnre 11168  ax-pre-lttri 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-rp 13012

This theorem is referenced by:  rprege0d  13062  rpexpmord  14200  01sqrexlem5  15293  isumrpcl  15893  isumltss  15898  harmonic  15909  expcnv  15914  prmreclem5  16975  prmreclem6  16976  4sqlem7  16999  nmoi2  24887  reperflem  24976  lebnumii  25125  nmoleub2lem3  25274  nmoleub3  25278  lmnn  25422  minveclem3  25588  pjthlem1  25596  ovoliunlem1  25661  vitalilem4  25770  vitali  25772  itg2const2  25900  itggt0  26003  lhop1lem  26172  plyeq0lem  26367  aalioulem4  26498  aaliou3lem2  26506  aaliou3lem3  26507  pserdvlem2  26591  abelthlem7  26601  pilem2  26615  pilem3  26616  divlogrlim  26800  logtayllem  26824  cxpge0  26848  divcxp  26852  cxpsqrtlem  26867  cxpsqrt  26868  abscxpbnd  26918  asinlem3  27036  leibpi  27107  birthdaylem3  27118  rlimcnp3  27132  cxplim  27136  rlimcxp  27138  cxp2limlem  27140  cxp2lim  27141  jensenlem2  27152  amgmlem  27154  emcllem2  27161  emcllem4  27163  emcllem6  27165  fsumharmonic  27176  zetacvg  27179  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem5  27197  lgamcvg2  27219  regamcl  27225  ftalem3  27239  ftalem5  27241  basellem6  27250  basellem8  27252  chtge0  27276  chtwordi  27320  chpval2  27382  chpchtsum  27383  chpub  27384  bposlem1  27448  bposlem2  27449  bposlem4  27451  bposlem5  27452  bposlem6  27453  bposlem7  27454  bposlem9  27456  lgsquadlem2  27545  chtppilimlem1  27637  chtppilimlem2  27638  chtppilim  27639  chpchtlim  27643  rplogsumlem1  27648  rplogsumlem2  27649  dchrisum0lem1a  27650  rpvmasumlem  27651  dchrisumlema  27652  2vmadivsumlem  27704  logdivbnd  27720  selberg3lem1  27721  selberg3lem2  27722  selberg4lem1  27724  pntrsumbnd2  27731  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6a  27746  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntibndlem2  27755  pntlemg  27762  pntlemk  27770  pntlem3  27773  pntleml  27775  ostth2lem1  27782  padicabv  27794  ostth2lem3  27799  ostth3  27802  nrt2irr  30824  ubthlem2  31223  minvecolem3  31228  minvecolem5  31233  pjhthlem1  31743  fsumub  33172  constrsqrtcl  34169  sqsscirc1  34298  omssubaddlem  34689  hgt750lemd  35035  logdivsqrle  35037  hgt750lem  35038  hgt750leme  35045  knoppndvlem18  37118  taupilemrplb  37964  poimirlem29  38300  itggt0cn  38341  geomcau  38410  cntotbnd  38447  rrndstprj2  38482  aks4d1p1p7  42841  2ap1caineq  42912  fltnltalem  43394  irrapxlem5  43553  pell1qrgaplem  43600  pell14qrgapw  43603  pellqrex  43606  rmxypos  43674  binomcxplemnotnn0  45066  recnnltrp  46092  rpgtrecnn  46095  stoweidlem3  46717  stoweidlem26  46740  wallispilem4  46782  wallispi  46784  wallispi2lem1  46785  stirlinglem1  46788  stirlinglem4  46791  stirlinglem10  46797  stirlinglem11  46798  stirlinglem12  46799  fourierdlem39  46860  fourierdlem42  46863  fourierdlem87  46907  fourierdlem107  46927  rrndistlt  47004  sge0rpcpnf  47135  ovnsubaddlem1  47284  hoidmvlelem2  47310  hoidmvlelem4  47312  ovolval5lem1  47366  vonioolem1  47394