Theorem rpge0d 13161

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  0cc0 11193   ≤ cle 11337  ℝ⁺crp 13113

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-addrcl 11254  ax-rnegex 11264  ax-cnre 11266  ax-pre-lttri 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  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 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-rp 13114

This theorem is used by:  rprege0d  13164  rpexpmord  14304  01sqrexlem5  15406  isumrpcl  16005  isumltss  16010  harmonic  16021  expcnv  16026  prmreclem5  17091  prmreclem6  17092  4sqlem7  17115  nmoi2  25042  reperflem  25131  lebnumii  25280  nmoleub2lem3  25429  nmoleub3  25433  lmnn  25577  minveclem3  25743  pjthlem1  25751  ovoliunlem1  25816  vitalilem4  25925  vitali  25927  itg2const2  26055  itggt0  26157  lhop1lem  26326  plyeq0lem  26522  aalioulem4  26655  aaliou3lem2  26663  aaliou3lem3  26664  pserdvlem2  26748  abelthlem7  26758  pilem2  26772  pilem3  26773  divlogrlim  26956  logtayllem  26980  cxpge0  27004  divcxp  27008  cxpsqrtlem  27023  cxpsqrt  27024  abscxpbnd  27074  asinlem3  27192  leibpi  27263  birthdaylem3  27274  rlimcnp3  27288  cxplim  27292  rlimcxp  27294  cxp2limlem  27296  cxp2lim  27297  jensenlem2  27308  amgmlem  27310  emcllem2  27317  emcllem4  27319  emcllem6  27321  fsumharmonic  27332  zetacvg  27335  lgamgulmlem2  27350  lgamgulmlem3  27351  lgamgulmlem5  27353  lgamcvg2  27375  regamcl  27381  ftalem3  27395  ftalem5  27397  basellem6  27406  basellem8  27408  chtge0  27432  chtwordi  27476  chpval2  27538  chpchtsum  27539  chpub  27540  bposlem1  27604  bposlem2  27605  bposlem4  27607  bposlem5  27608  bposlem6  27609  bposlem7  27610  bposlem9  27612  lgsquadlem2  27701  chtppilimlem1  27793  chtppilimlem2  27794  chtppilim  27795  chpchtlim  27799  rplogsumlem1  27804  rplogsumlem2  27805  dchrisum0lem1a  27806  rpvmasumlem  27807  dchrisumlema  27808  2vmadivsumlem  27860  logdivbnd  27876  selberg3lem1  27877  selberg3lem2  27878  selberg4lem1  27880  pntrsumbnd2  27887  pntrlog2bndlem1  27897  pntrlog2bndlem2  27898  pntrlog2bndlem3  27899  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntrlog2bndlem6a  27902  pntrlog2bndlem6  27903  pntrlog2bnd  27904  pntibndlem2  27911  pntlemg  27918  pntlemk  27926  pntlem3  27929  pntleml  27931  ostth2lem1  27938  padicabv  27950  ostth2lem3  27955  ostth3  27958  nrt2irr  31067  ubthlem2  31466  minvecolem3  31471  minvecolem5  31476  pjhthlem1  31986  fsumub  33412  constrsqrtcl  34404  sqsscirc1  34533  omssubaddlem  34924  hgt750lemd  35270  logdivsqrle  35272  hgt750lem  35273  hgt750leme  35280  knoppndvlem18  37375  taupilemrplb  38221  poimirlem29  38547  itggt0cn  38588  geomcau  38673  cntotbnd  38710  rrndstprj2  38745  aks4d1p1p7  43104  2ap1caineq  43175  fltnltalem  43653  irrapxlem5  43812  pell1qrgaplem  43859  pell14qrgapw  43862  pellqrex  43865  rmxypos  43933  binomcxplemnotnn0  45325  recnnltrp  46357  rpgtrecnn  46360  stoweidlem3  46982  stoweidlem26  47005  wallispilem4  47047  wallispi  47049  wallispi2lem1  47050  stirlinglem1  47053  stirlinglem4  47056  stirlinglem10  47062  stirlinglem11  47063  stirlinglem12  47064  fourierdlem39  47125  fourierdlem42  47128  fourierdlem87  47172  fourierdlem107  47192  rrndistlt  47269  sge0rpcpnf  47400  ovnsubaddlem1  47549  hoidmvlelem2  47575  hoidmvlelem4  47577  ovolval5lem1  47631  vonioolem1  47659