Theorem rpge0d 13064

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5125  0cc0 11138   ≤ cle 11279  ℝ⁺crp 13017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738  ax-resscn 11195  ax-1cn 11196  ax-addrcl 11199  ax-rnegex 11209  ax-cnre 11211  ax-pre-lttri 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-sbc 3773  df-csb 3882  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-mpt 5208  df-id 5560  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-er 8728  df-en 8969  df-dom 8970  df-sdom 8971  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-rp 13018

This theorem is referenced by:  rprege0d  13067  rpexpmord  14191  01sqrexlem5  15268  isumrpcl  15862  isumltss  15867  harmonic  15878  expcnv  15883  prmreclem5  16941  prmreclem6  16942  4sqlem7  16965  nmoi2  24706  reperflem  24795  lebnumii  24953  nmoleub2lem3  25103  nmoleub3  25107  lmnn  25252  minveclem3  25418  pjthlem1  25426  ovoliunlem1  25492  vitalilem4  25601  vitali  25603  itg2const2  25731  itggt0  25834  lhop1lem  26007  plyeq0lem  26204  aalioulem4  26332  aaliou3lem2  26340  aaliou3lem3  26341  pserdvlem2  26427  abelthlem7  26437  pilem2  26451  pilem3  26452  divlogrlim  26632  logtayllem  26656  cxpge0  26680  divcxp  26684  cxpsqrtlem  26699  cxpsqrt  26700  abscxpbnd  26751  asinlem3  26869  leibpi  26940  birthdaylem3  26951  rlimcnp3  26965  cxplim  26970  rlimcxp  26972  cxp2limlem  26974  cxp2lim  26975  jensenlem2  26986  amgmlem  26988  emcllem2  26995  emcllem4  26997  emcllem6  26999  fsumharmonic  27010  zetacvg  27013  lgamgulmlem2  27028  lgamgulmlem3  27029  lgamgulmlem5  27031  lgamcvg2  27053  regamcl  27059  ftalem3  27073  ftalem5  27075  basellem6  27084  basellem8  27086  chtge0  27110  chtwordi  27154  chpval2  27217  chpchtsum  27218  chpub  27219  bposlem1  27283  bposlem2  27284  bposlem4  27286  bposlem5  27287  bposlem6  27288  bposlem7  27289  bposlem9  27291  lgsquadlem2  27380  chtppilimlem1  27472  chtppilimlem2  27473  chtppilim  27474  chpchtlim  27478  rplogsumlem1  27483  rplogsumlem2  27484  dchrisum0lem1a  27485  rpvmasumlem  27486  dchrisumlema  27487  2vmadivsumlem  27539  logdivbnd  27555  selberg3lem1  27556  selberg3lem2  27557  selberg4lem1  27559  pntrsumbnd2  27566  pntrlog2bndlem1  27576  pntrlog2bndlem2  27577  pntrlog2bndlem3  27578  pntrlog2bndlem4  27579  pntrlog2bndlem5  27580  pntrlog2bndlem6a  27581  pntrlog2bndlem6  27582  pntrlog2bnd  27583  pntibndlem2  27590  pntlemg  27597  pntlemk  27605  pntlem3  27608  pntleml  27610  ostth2lem1  27617  padicabv  27629  ostth2lem3  27634  ostth3  27637  nrt2irr  30439  ubthlem2  30837  minvecolem3  30842  minvecolem5  30847  pjhthlem1  31357  fsumub  32777  sqsscirc1  33848  omssubaddlem  34242  hgt750lemd  34604  logdivsqrle  34606  hgt750lem  34607  hgt750leme  34614  knoppndvlem18  36471  taupilemrplb  37262  poimirlem29  37597  itggt0cn  37638  geomcau  37707  cntotbnd  37744  rrndstprj2  37779  aks4d1p1p7  42016  2ap1caineq  42087  fltnltalem  42617  irrapxlem5  42782  pell1qrgaplem  42829  pell14qrgapw  42832  pellqrex  42835  rmxypos  42904  binomcxplemnotnn0  44320  recnnltrp  45333  rpgtrecnn  45336  stoweidlem3  45963  stoweidlem26  45986  wallispilem4  46028  wallispi  46030  wallispi2lem1  46031  stirlinglem1  46034  stirlinglem4  46037  stirlinglem10  46043  stirlinglem11  46044  stirlinglem12  46045  fourierdlem39  46106  fourierdlem42  46109  fourierdlem87  46153  fourierdlem107  46173  rrndistlt  46250  sge0rpcpnf  46381  ovnsubaddlem1  46530  hoidmvlelem2  46556  hoidmvlelem4  46558  ovolval5lem1  46612  vonioolem1  46640