Theorem rpge0d 13041

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

Syntax hints:   → wi 4   ∈ wcel 2142   class class class wbr 5100  0cc0 11073   ≤ cle 11217  ℝ⁺crp 12993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-addrcl 11134  ax-rnegex 11144  ax-cnre 11146  ax-pre-lttri 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-rp 12994

This theorem is referenced by:  rprege0d  13044  rpexpmord  14181  01sqrexlem5  15273  isumrpcl  15873  isumltss  15878  harmonic  15889  expcnv  15894  prmreclem5  16956  prmreclem6  16957  4sqlem7  16980  nmoi2  24787  reperflem  24876  lebnumii  25025  nmoleub2lem3  25174  nmoleub3  25178  lmnn  25322  minveclem3  25488  pjthlem1  25496  ovoliunlem1  25561  vitalilem4  25670  vitali  25672  itg2const2  25800  itggt0  25903  lhop1lem  26072  plyeq0lem  26267  aalioulem4  26396  aaliou3lem2  26404  aaliou3lem3  26405  pserdvlem2  26488  abelthlem7  26498  pilem2  26512  pilem3  26513  divlogrlim  26697  logtayllem  26721  cxpge0  26745  divcxp  26749  cxpsqrtlem  26764  cxpsqrt  26765  abscxpbnd  26815  asinlem3  26933  leibpi  27004  birthdaylem3  27015  rlimcnp3  27029  cxplim  27033  rlimcxp  27035  cxp2limlem  27037  cxp2lim  27038  jensenlem2  27049  amgmlem  27051  emcllem2  27058  emcllem4  27060  emcllem6  27062  fsumharmonic  27073  zetacvg  27076  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem5  27094  lgamcvg2  27116  regamcl  27122  ftalem3  27136  ftalem5  27138  basellem6  27147  basellem8  27149  chtge0  27173  chtwordi  27217  chpval2  27279  chpchtsum  27280  chpub  27281  bposlem1  27345  bposlem2  27346  bposlem4  27348  bposlem5  27349  bposlem6  27350  bposlem7  27351  bposlem9  27353  lgsquadlem2  27442  chtppilimlem1  27534  chtppilimlem2  27535  chtppilim  27536  chpchtlim  27540  rplogsumlem1  27545  rplogsumlem2  27546  dchrisum0lem1a  27547  rpvmasumlem  27548  dchrisumlema  27549  2vmadivsumlem  27601  logdivbnd  27617  selberg3lem1  27618  selberg3lem2  27619  selberg4lem1  27621  pntrsumbnd2  27628  pntrlog2bndlem1  27638  pntrlog2bndlem2  27639  pntrlog2bndlem3  27640  pntrlog2bndlem4  27641  pntrlog2bndlem5  27642  pntrlog2bndlem6a  27643  pntrlog2bndlem6  27644  pntrlog2bnd  27645  pntibndlem2  27652  pntlemg  27659  pntlemk  27667  pntlem3  27670  pntleml  27672  ostth2lem1  27679  padicabv  27691  ostth2lem3  27696  ostth3  27699  nrt2irr  30672  ubthlem2  31071  minvecolem3  31076  minvecolem5  31081  pjhthlem1  31591  fsumub  33027  constrsqrtcl  34073  sqsscirc1  34202  omssubaddlem  34593  hgt750lemd  34939  logdivsqrle  34941  hgt750lem  34942  hgt750leme  34949  knoppndvlem18  36964  taupilemrplb  37809  poimirlem29  38145  itggt0cn  38186  geomcau  38255  cntotbnd  38292  rrndstprj2  38327  aks4d1p1p7  42688  2ap1caineq  42759  fltnltalem  43241  irrapxlem5  43400  pell1qrgaplem  43447  pell14qrgapw  43450  pellqrex  43453  rmxypos  43521  binomcxplemnotnn0  44929  recnnltrp  45949  rpgtrecnn  45952  stoweidlem3  46574  stoweidlem26  46597  wallispilem4  46639  wallispi  46641  wallispi2lem1  46642  stirlinglem1  46645  stirlinglem4  46648  stirlinglem10  46654  stirlinglem11  46655  stirlinglem12  46656  fourierdlem39  46717  fourierdlem42  46720  fourierdlem87  46764  fourierdlem107  46784  rrndistlt  46861  sge0rpcpnf  46992  ovnsubaddlem1  47141  hoidmvlelem2  47167  hoidmvlelem4  47169  ovolval5lem1  47223  vonioolem1  47251