Theorem rpge0d 13080

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5111  0cc0 11115   ≤ cle 11259  ℝ⁺crp 13032

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11172  ax-1cn 11173  ax-addrcl 11176  ax-rnegex 11186  ax-cnre 11188  ax-pre-lttri 11189

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-rp 13033

This theorem is used by:  rprege0d  13083  rpexpmord  14222  01sqrexlem5  15321  isumrpcl  15920  isumltss  15925  harmonic  15936  expcnv  15941  prmreclem5  17002  prmreclem6  17003  4sqlem7  17026  nmoi2  24938  reperflem  25027  lebnumii  25176  nmoleub2lem3  25325  nmoleub3  25329  lmnn  25473  minveclem3  25639  pjthlem1  25647  ovoliunlem1  25712  vitalilem4  25821  vitali  25823  itg2const2  25951  itggt0  26054  lhop1lem  26223  plyeq0lem  26418  aalioulem4  26549  aaliou3lem2  26557  aaliou3lem3  26558  pserdvlem2  26642  abelthlem7  26652  pilem2  26666  pilem3  26667  divlogrlim  26851  logtayllem  26875  cxpge0  26899  divcxp  26903  cxpsqrtlem  26918  cxpsqrt  26919  abscxpbnd  26969  asinlem3  27087  leibpi  27158  birthdaylem3  27169  rlimcnp3  27183  cxplim  27187  rlimcxp  27189  cxp2limlem  27191  cxp2lim  27192  jensenlem2  27203  amgmlem  27205  emcllem2  27212  emcllem4  27214  emcllem6  27216  fsumharmonic  27227  zetacvg  27230  lgamgulmlem2  27245  lgamgulmlem3  27246  lgamgulmlem5  27248  lgamcvg2  27270  regamcl  27276  ftalem3  27290  ftalem5  27292  basellem6  27301  basellem8  27303  chtge0  27327  chtwordi  27371  chpval2  27433  chpchtsum  27434  chpub  27435  bposlem1  27499  bposlem2  27500  bposlem4  27502  bposlem5  27503  bposlem6  27504  bposlem7  27505  bposlem9  27507  lgsquadlem2  27596  chtppilimlem1  27688  chtppilimlem2  27689  chtppilim  27690  chpchtlim  27694  rplogsumlem1  27699  rplogsumlem2  27700  dchrisum0lem1a  27701  rpvmasumlem  27702  dchrisumlema  27703  2vmadivsumlem  27755  logdivbnd  27771  selberg3lem1  27772  selberg3lem2  27773  selberg4lem1  27775  pntrsumbnd2  27782  pntrlog2bndlem1  27792  pntrlog2bndlem2  27793  pntrlog2bndlem3  27794  pntrlog2bndlem4  27795  pntrlog2bndlem5  27796  pntrlog2bndlem6a  27797  pntrlog2bndlem6  27798  pntrlog2bnd  27799  pntibndlem2  27806  pntlemg  27813  pntlemk  27821  pntlem3  27824  pntleml  27826  ostth2lem1  27833  padicabv  27845  ostth2lem3  27850  ostth3  27853  nrt2irr  30895  ubthlem2  31294  minvecolem3  31299  minvecolem5  31304  pjhthlem1  31814  fsumub  33242  constrsqrtcl  34233  sqsscirc1  34362  omssubaddlem  34754  hgt750lemd  35100  logdivsqrle  35102  hgt750lem  35103  hgt750leme  35110  knoppndvlem18  37175  taupilemrplb  38021  poimirlem29  38357  itggt0cn  38398  geomcau  38468  cntotbnd  38505  rrndstprj2  38540  aks4d1p1p7  42899  2ap1caineq  42970  fltnltalem  43452  irrapxlem5  43611  pell1qrgaplem  43658  pell14qrgapw  43661  pellqrex  43664  rmxypos  43732  binomcxplemnotnn0  45124  recnnltrp  46150  rpgtrecnn  46153  stoweidlem3  46775  stoweidlem26  46798  wallispilem4  46840  wallispi  46842  wallispi2lem1  46843  stirlinglem1  46846  stirlinglem4  46849  stirlinglem10  46855  stirlinglem11  46856  stirlinglem12  46857  fourierdlem39  46918  fourierdlem42  46921  fourierdlem87  46965  fourierdlem107  46985  rrndistlt  47062  sge0rpcpnf  47193  ovnsubaddlem1  47342  hoidmvlelem2  47368  hoidmvlelem4  47370  ovolval5lem1  47424  vonioolem1  47452