Theorem rpge0d 13093

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 13059	. 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 11127   ≤ cle 11271  ℝ⁺crp 13045

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 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11184  ax-1cn 11185  ax-addrcl 11188  ax-rnegex 11198  ax-cnre 11200  ax-pre-lttri 11201

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 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 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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-rp 13046

This theorem is used by:  rprege0d  13096  rpexpmord  14235  01sqrexlem5  15336  isumrpcl  15935  isumltss  15940  harmonic  15951  expcnv  15956  prmreclem5  17015  prmreclem6  17016  4sqlem7  17039  nmoi2  24959  reperflem  25048  lebnumii  25197  nmoleub2lem3  25346  nmoleub3  25350  lmnn  25494  minveclem3  25660  pjthlem1  25668  ovoliunlem1  25733  vitalilem4  25842  vitali  25844  itg2const2  25972  itggt0  26074  lhop1lem  26243  plyeq0lem  26439  aalioulem4  26574  aaliou3lem2  26582  aaliou3lem3  26583  pserdvlem2  26667  abelthlem7  26677  pilem2  26691  pilem3  26692  divlogrlim  26875  logtayllem  26899  cxpge0  26923  divcxp  26927  cxpsqrtlem  26942  cxpsqrt  26943  abscxpbnd  26993  asinlem3  27111  leibpi  27182  birthdaylem3  27193  rlimcnp3  27207  cxplim  27211  rlimcxp  27213  cxp2limlem  27215  cxp2lim  27216  jensenlem2  27227  amgmlem  27229  emcllem2  27236  emcllem4  27238  emcllem6  27240  fsumharmonic  27251  zetacvg  27254  lgamgulmlem2  27269  lgamgulmlem3  27270  lgamgulmlem5  27272  lgamcvg2  27294  regamcl  27300  ftalem3  27314  ftalem5  27316  basellem6  27325  basellem8  27327  chtge0  27351  chtwordi  27395  chpval2  27457  chpchtsum  27458  chpub  27459  bposlem1  27523  bposlem2  27524  bposlem4  27526  bposlem5  27527  bposlem6  27528  bposlem7  27529  bposlem9  27531  lgsquadlem2  27620  chtppilimlem1  27712  chtppilimlem2  27713  chtppilim  27714  chpchtlim  27718  rplogsumlem1  27723  rplogsumlem2  27724  dchrisum0lem1a  27725  rpvmasumlem  27726  dchrisumlema  27727  2vmadivsumlem  27779  logdivbnd  27795  selberg3lem1  27796  selberg3lem2  27797  selberg4lem1  27799  pntrsumbnd2  27806  pntrlog2bndlem1  27816  pntrlog2bndlem2  27817  pntrlog2bndlem3  27818  pntrlog2bndlem4  27819  pntrlog2bndlem5  27820  pntrlog2bndlem6a  27821  pntrlog2bndlem6  27822  pntrlog2bnd  27823  pntibndlem2  27830  pntlemg  27837  pntlemk  27845  pntlem3  27848  pntleml  27850  ostth2lem1  27857  padicabv  27869  ostth2lem3  27874  ostth3  27877  nrt2irr  30956  ubthlem2  31355  minvecolem3  31360  minvecolem5  31365  pjhthlem1  31875  fsumub  33301  constrsqrtcl  34292  sqsscirc1  34421  omssubaddlem  34813  hgt750lemd  35159  logdivsqrle  35161  hgt750lem  35162  hgt750leme  35169  knoppndvlem18  37229  taupilemrplb  38075  poimirlem29  38401  itggt0cn  38442  geomcau  38512  cntotbnd  38549  rrndstprj2  38584  aks4d1p1p7  42943  2ap1caineq  43014  fltnltalem  43511  irrapxlem5  43670  pell1qrgaplem  43717  pell14qrgapw  43720  pellqrex  43723  rmxypos  43791  binomcxplemnotnn0  45183  recnnltrp  46209  rpgtrecnn  46212  stoweidlem3  46834  stoweidlem26  46857  wallispilem4  46899  wallispi  46901  wallispi2lem1  46902  stirlinglem1  46905  stirlinglem4  46908  stirlinglem10  46914  stirlinglem11  46915  stirlinglem12  46916  fourierdlem39  46977  fourierdlem42  46980  fourierdlem87  47024  fourierdlem107  47044  rrndistlt  47121  sge0rpcpnf  47252  ovnsubaddlem1  47401  hoidmvlelem2  47427  hoidmvlelem4  47429  ovolval5lem1  47483  vonioolem1  47511