Theorem rpge0d 12160

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

Syntax hints:   → wi 4   ∈ wcel 2166   class class class wbr 4873  0cc0 10252   ≤ cle 10392  ℝ⁺crp 12112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-resscn 10309  ax-1cn 10310  ax-addrcl 10313  ax-rnegex 10323  ax-cnre 10325  ax-pre-lttri 10326

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-er 8009  df-en 8223  df-dom 8224  df-sdom 8225  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-rp 12113

This theorem is referenced by:  rprege0d  12163  sqrlem5  14364  isumrpcl  14949  isumltss  14954  harmonic  14965  expcnv  14970  prmreclem5  15995  prmreclem6  15996  4sqlem7  16019  nmoi2  22904  reperflem  22991  lebnumii  23135  nmoleub2lem3  23284  nmoleub3  23288  lmnn  23431  minveclem3  23597  pjthlem1  23605  ovoliunlem1  23668  vitalilem4  23777  vitali  23779  itg2const2  23907  itggt0  24007  lhop1lem  24175  plyeq0lem  24365  aalioulem4  24489  aaliou3lem2  24497  aaliou3lem3  24498  pserdvlem2  24581  abelthlem7  24591  pilem2  24605  pilem3  24606  pilem3OLD  24607  divlogrlim  24780  logtayllem  24804  cxpge0  24828  divcxp  24832  cxpsqrtlem  24847  cxpsqrt  24848  abscxpbnd  24896  asinlem3  25011  leibpi  25082  birthdaylem3  25093  rlimcnp3  25107  cxplim  25111  rlimcxp  25113  cxp2limlem  25115  cxp2lim  25116  jensenlem2  25127  amgmlem  25129  emcllem2  25136  emcllem4  25138  emcllem6  25140  fsumharmonic  25151  zetacvg  25154  lgamgulmlem2  25169  lgamgulmlem3  25170  lgamgulmlem5  25172  lgamcvg2  25194  regamcl  25200  ftalem3  25214  ftalem5  25216  basellem6  25225  basellem8  25227  chtge0  25251  chtwordi  25295  chpval2  25356  chpchtsum  25357  chpub  25358  bposlem1  25422  bposlem2  25423  bposlem4  25425  bposlem5  25426  bposlem6  25427  bposlem7  25428  bposlem9  25430  lgsquadlem2  25519  chtppilimlem1  25575  chtppilimlem2  25576  chtppilim  25577  chpchtlim  25581  rplogsumlem1  25586  rplogsumlem2  25587  dchrisum0lem1a  25588  rpvmasumlem  25589  dchrisumlema  25590  2vmadivsumlem  25642  logdivbnd  25658  selberg3lem1  25659  selberg3lem2  25660  selberg4lem1  25662  pntrsumbnd2  25669  pntrlog2bndlem1  25679  pntrlog2bndlem2  25680  pntrlog2bndlem3  25681  pntrlog2bndlem4  25682  pntrlog2bndlem5  25683  pntrlog2bndlem6a  25684  pntrlog2bndlem6  25685  pntrlog2bnd  25686  pntibndlem2  25693  pntlemg  25700  pntlemk  25708  pntlem3  25711  pntleml  25713  ostth2lem1  25720  padicabv  25732  ostth2lem3  25737  ostth3  25740  ubthlem2  28282  minvecolem3  28287  minvecolem5  28292  pjhthlem1  28805  fsumub  30121  sqsscirc1  30499  omssubaddlem  30906  hgt750lemd  31275  logdivsqrle  31277  hgt750lem  31278  hgt750leme  31285  knoppndvlem18  33052  taupilemrplb  33712  poimirlem29  33982  itggt0cn  34025  geomcau  34097  cntotbnd  34137  rrndstprj2  34172  irrapxlem5  38234  pell1qrgaplem  38281  pell14qrgapw  38284  pellqrex  38287  rpexpmord  38356  rmxypos  38357  binomcxplemnotnn0  39395  recnnltrp  40390  rpgtrecnn  40394  stoweidlem3  41014  stoweidlem26  41037  wallispilem4  41079  wallispi  41081  wallispi2lem1  41082  stirlinglem1  41085  stirlinglem4  41088  stirlinglem10  41094  stirlinglem11  41095  stirlinglem12  41096  fourierdlem39  41157  fourierdlem42  41160  fourierdlem87  41204  fourierdlem107  41224  rrndistlt  41301  sge0rpcpnf  41429  ovnsubaddlem1  41578  hoidmvlelem2  41604  hoidmvlelem4  41606  ovolval5lem1  41660  vonioolem1  41688