Theorem rpge0d 13069

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

Syntax hints:   → wi 4   ∈ wcel 2098   class class class wbr 5152  0cc0 11154   ≤ cle 11295  ℝ⁺crp 13023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-resscn 11211  ax-1cn 11212  ax-addrcl 11215  ax-rnegex 11225  ax-cnre 11227  ax-pre-lttri 11228

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5579  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-er 8733  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-rp 13024

This theorem is referenced by:  rprege0d  13072  rpexpmord  14182  01sqrexlem5  15246  isumrpcl  15842  isumltss  15847  harmonic  15858  expcnv  15863  prmreclem5  16917  prmreclem6  16918  4sqlem7  16941  nmoi2  24730  reperflem  24817  lebnumii  24975  nmoleub2lem3  25125  nmoleub3  25129  lmnn  25274  minveclem3  25440  pjthlem1  25448  ovoliunlem1  25514  vitalilem4  25623  vitali  25625  itg2const2  25754  itggt0  25856  lhop1lem  26029  plyeq0lem  26229  aalioulem4  26355  aaliou3lem2  26363  aaliou3lem3  26364  pserdvlem2  26450  abelthlem7  26460  pilem2  26474  pilem3  26475  divlogrlim  26654  logtayllem  26678  cxpge0  26702  divcxp  26706  cxpsqrtlem  26721  cxpsqrt  26722  abscxpbnd  26773  asinlem3  26891  leibpi  26962  birthdaylem3  26973  rlimcnp3  26987  cxplim  26992  rlimcxp  26994  cxp2limlem  26996  cxp2lim  26997  jensenlem2  27008  amgmlem  27010  emcllem2  27017  emcllem4  27019  emcllem6  27021  fsumharmonic  27032  zetacvg  27035  lgamgulmlem2  27050  lgamgulmlem3  27051  lgamgulmlem5  27053  lgamcvg2  27075  regamcl  27081  ftalem3  27095  ftalem5  27097  basellem6  27106  basellem8  27108  chtge0  27132  chtwordi  27176  chpval2  27239  chpchtsum  27240  chpub  27241  bposlem1  27305  bposlem2  27306  bposlem4  27308  bposlem5  27309  bposlem6  27310  bposlem7  27311  bposlem9  27313  lgsquadlem2  27402  chtppilimlem1  27494  chtppilimlem2  27495  chtppilim  27496  chpchtlim  27500  rplogsumlem1  27505  rplogsumlem2  27506  dchrisum0lem1a  27507  rpvmasumlem  27508  dchrisumlema  27509  2vmadivsumlem  27561  logdivbnd  27577  selberg3lem1  27578  selberg3lem2  27579  selberg4lem1  27581  pntrsumbnd2  27588  pntrlog2bndlem1  27598  pntrlog2bndlem2  27599  pntrlog2bndlem3  27600  pntrlog2bndlem4  27601  pntrlog2bndlem5  27602  pntrlog2bndlem6a  27603  pntrlog2bndlem6  27604  pntrlog2bnd  27605  pntibndlem2  27612  pntlemg  27619  pntlemk  27627  pntlem3  27630  pntleml  27632  ostth2lem1  27639  padicabv  27651  ostth2lem3  27656  ostth3  27659  nrt2irr  30398  ubthlem2  30796  minvecolem3  30801  minvecolem5  30806  pjhthlem1  31316  fsumub  32718  sqsscirc1  33679  omssubaddlem  34089  hgt750lemd  34450  logdivsqrle  34452  hgt750lem  34453  hgt750leme  34460  knoppndvlem18  36180  taupilemrplb  36975  poimirlem29  37298  itggt0cn  37339  geomcau  37408  cntotbnd  37445  rrndstprj2  37480  aks4d1p1p7  41721  2ap1caineq  41791  fltnltalem  42253  irrapxlem5  42420  pell1qrgaplem  42467  pell14qrgapw  42470  pellqrex  42473  rmxypos  42542  binomcxplemnotnn0  43967  recnnltrp  44929  rpgtrecnn  44932  stoweidlem3  45561  stoweidlem26  45584  wallispilem4  45626  wallispi  45628  wallispi2lem1  45629  stirlinglem1  45632  stirlinglem4  45635  stirlinglem10  45641  stirlinglem11  45642  stirlinglem12  45643  fourierdlem39  45704  fourierdlem42  45707  fourierdlem87  45751  fourierdlem107  45771  rrndistlt  45848  sge0rpcpnf  45979  ovnsubaddlem1  46128  hoidmvlelem2  46154  hoidmvlelem4  46156  ovolval5lem1  46210  vonioolem1  46238