Theorem rpge0d 13175

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  0cc0 11207   ≤ cle 11351  ℝ⁺crp 13127

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-resscn 11264  ax-1cn 11265  ax-addrcl 11268  ax-rnegex 11278  ax-cnre 11280  ax-pre-lttri 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  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 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8724  df-en 8981  df-dom 8982  df-sdom 8983  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-rp 13128

This theorem is used by:  rprege0d  13178  rpexpmord  14318  01sqrexlem5  15422  isumrpcl  16021  isumltss  16026  harmonic  16037  expcnv  16042  prmreclem5  17107  prmreclem6  17108  4sqlem7  17131  nmoi2  25058  reperflem  25147  lebnumii  25296  nmoleub2lem3  25445  nmoleub3  25449  lmnn  25593  minveclem3  25759  pjthlem1  25767  ovoliunlem1  25832  vitalilem4  25941  vitali  25943  itg2const2  26071  itggt0  26173  lhop1lem  26342  plyeq0lem  26538  aalioulem4  26671  aaliou3lem2  26679  aaliou3lem3  26680  pserdvlem2  26764  abelthlem7  26774  pilem2  26788  pilem3  26789  divlogrlim  26972  logtayllem  26996  cxpge0  27020  divcxp  27024  cxpsqrtlem  27039  cxpsqrt  27040  abscxpbnd  27090  asinlem3  27208  leibpi  27279  birthdaylem3  27290  rlimcnp3  27304  cxplim  27308  rlimcxp  27310  cxp2limlem  27312  cxp2lim  27313  jensenlem2  27324  amgmlem  27326  emcllem2  27333  emcllem4  27335  emcllem6  27337  fsumharmonic  27348  zetacvg  27351  lgamgulmlem2  27366  lgamgulmlem3  27367  lgamgulmlem5  27369  lgamcvg2  27391  regamcl  27397  ftalem3  27411  ftalem5  27413  basellem6  27422  basellem8  27424  chtge0  27448  chtwordi  27492  chpval2  27554  chpchtsum  27555  chpub  27556  bposlem1  27620  bposlem2  27621  bposlem4  27623  bposlem5  27624  bposlem6  27625  bposlem7  27626  bposlem9  27628  lgsquadlem2  27717  chtppilimlem1  27809  chtppilimlem2  27810  chtppilim  27811  chpchtlim  27815  rplogsumlem1  27820  rplogsumlem2  27821  dchrisum0lem1a  27822  rpvmasumlem  27823  dchrisumlema  27824  2vmadivsumlem  27876  logdivbnd  27892  selberg3lem1  27893  selberg3lem2  27894  selberg4lem1  27896  pntrsumbnd2  27903  pntrlog2bndlem1  27913  pntrlog2bndlem2  27914  pntrlog2bndlem3  27915  pntrlog2bndlem4  27916  pntrlog2bndlem5  27917  pntrlog2bndlem6a  27918  pntrlog2bndlem6  27919  pntrlog2bnd  27920  pntibndlem2  27927  pntlemg  27934  pntlemk  27942  pntlem3  27945  pntleml  27947  ostth2lem1  27954  padicabv  27966  ostth2lem3  27971  ostth3  27974  nrt2irr  31083  ubthlem2  31482  minvecolem3  31487  minvecolem5  31492  pjhthlem1  32002  fsumub  33469  constrsqrtcl  34461  sqsscirc1  34590  omssubaddlem  34981  hgt750lemd  35327  logdivsqrle  35329  hgt750lem  35330  hgt750leme  35337  knoppndvlem18  37491  taupilemrplb  38350  poimirlem29  38676  itggt0cn  38717  geomcau  38802  cntotbnd  38839  rrndstprj2  38874  aks4d1p1p7  43233  2ap1caineq  43304  fltnltalem  43782  irrapxlem5  43942  pell1qrgaplem  43989  pell14qrgapw  43992  pellqrex  43995  rmxypos  44063  binomcxplemnotnn0  45449  recnnltrp  46496  rpgtrecnn  46499  stoweidlem3  47121  stoweidlem26  47144  wallispilem4  47186  wallispi  47188  wallispi2lem1  47189  stirlinglem1  47192  stirlinglem4  47195  stirlinglem10  47201  stirlinglem11  47202  stirlinglem12  47203  fourierdlem39  47264  fourierdlem42  47267  fourierdlem87  47311  fourierdlem107  47331  rrndistlt  47408  sge0rpcpnf  47539  ovnsubaddlem1  47688  hoidmvlelem2  47714  hoidmvlelem4  47716  ovolval5lem1  47770  vonioolem1  47798