Theorem rpge0d 13063

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5113  0cc0 11099   ≤ cle 11243  ℝ⁺crp 13015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11156  ax-1cn 11157  ax-addrcl 11160  ax-rnegex 11170  ax-cnre 11172  ax-pre-lttri 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-rp 13016

This theorem is referenced by:  rprege0d  13066  rpexpmord  14203  01sqrexlem5  15296  isumrpcl  15896  isumltss  15901  harmonic  15912  expcnv  15917  prmreclem5  16979  prmreclem6  16980  4sqlem7  17003  nmoi2  24855  reperflem  24944  lebnumii  25093  nmoleub2lem3  25242  nmoleub3  25246  lmnn  25390  minveclem3  25556  pjthlem1  25564  ovoliunlem1  25629  vitalilem4  25738  vitali  25740  itg2const2  25868  itggt0  25971  lhop1lem  26140  plyeq0lem  26335  aalioulem4  26464  aaliou3lem2  26472  aaliou3lem3  26473  pserdvlem2  26556  abelthlem7  26566  pilem2  26580  pilem3  26581  divlogrlim  26765  logtayllem  26789  cxpge0  26813  divcxp  26817  cxpsqrtlem  26832  cxpsqrt  26833  abscxpbnd  26883  asinlem3  27001  leibpi  27072  birthdaylem3  27083  rlimcnp3  27097  cxplim  27101  rlimcxp  27103  cxp2limlem  27105  cxp2lim  27106  jensenlem2  27117  amgmlem  27119  emcllem2  27126  emcllem4  27128  emcllem6  27130  fsumharmonic  27141  zetacvg  27144  lgamgulmlem2  27159  lgamgulmlem3  27160  lgamgulmlem5  27162  lgamcvg2  27184  regamcl  27190  ftalem3  27204  ftalem5  27206  basellem6  27215  basellem8  27217  chtge0  27241  chtwordi  27285  chpval2  27347  chpchtsum  27348  chpub  27349  bposlem1  27413  bposlem2  27414  bposlem4  27416  bposlem5  27417  bposlem6  27418  bposlem7  27419  bposlem9  27421  lgsquadlem2  27510  chtppilimlem1  27602  chtppilimlem2  27603  chtppilim  27604  chpchtlim  27608  rplogsumlem1  27613  rplogsumlem2  27614  dchrisum0lem1a  27615  rpvmasumlem  27616  dchrisumlema  27617  2vmadivsumlem  27669  logdivbnd  27685  selberg3lem1  27686  selberg3lem2  27687  selberg4lem1  27689  pntrsumbnd2  27696  pntrlog2bndlem1  27706  pntrlog2bndlem2  27707  pntrlog2bndlem3  27708  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  pntrlog2bndlem6a  27711  pntrlog2bndlem6  27712  pntrlog2bnd  27713  pntibndlem2  27720  pntlemg  27727  pntlemk  27735  pntlem3  27738  pntleml  27740  ostth2lem1  27747  padicabv  27759  ostth2lem3  27764  ostth3  27767  nrt2irr  30764  ubthlem2  31163  minvecolem3  31168  minvecolem5  31173  pjhthlem1  31683  fsumub  33112  constrsqrtcl  34113  sqsscirc1  34242  omssubaddlem  34633  hgt750lemd  34979  logdivsqrle  34981  hgt750lem  34982  hgt750leme  34989  knoppndvlem18  37006  taupilemrplb  37851  poimirlem29  38187  itggt0cn  38228  geomcau  38297  cntotbnd  38334  rrndstprj2  38369  aks4d1p1p7  42730  2ap1caineq  42801  fltnltalem  43285  irrapxlem5  43444  pell1qrgaplem  43491  pell14qrgapw  43494  pellqrex  43497  rmxypos  43565  binomcxplemnotnn0  44957  recnnltrp  45983  rpgtrecnn  45986  stoweidlem3  46608  stoweidlem26  46631  wallispilem4  46673  wallispi  46675  wallispi2lem1  46676  stirlinglem1  46679  stirlinglem4  46682  stirlinglem10  46688  stirlinglem11  46689  stirlinglem12  46690  fourierdlem39  46751  fourierdlem42  46754  fourierdlem87  46798  fourierdlem107  46818  rrndistlt  46895  sge0rpcpnf  47026  ovnsubaddlem1  47175  hoidmvlelem2  47201  hoidmvlelem4  47203  ovolval5lem1  47257  vonioolem1  47285