Theorem elrpd 12778

Description: Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
elrpd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
elrpd.2	⊢ (𝜑 → 0 < 𝐴)

Assertion

Ref	Expression
elrpd	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Proof of Theorem elrpd

Step	Hyp	Ref	Expression
1		elrpd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		elrpd.2	. 2 ⊢ (𝜑 → 0 < 𝐴)
3		elrp 12741	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5075  ℝcr 10879  0cc0 10880   < clt 11018  ℝ⁺crp 12739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-rp 12740

This theorem is referenced by:  mul2lt0rgt0  12842  mul2lt0bi  12845  xov1plusxeqvd  13239  zltaddlt1le  13246  sqn0rp  13855  ltexp2a  13893  expcan  13896  ltexp2  13897  leexp2a  13899  expnlbnd2  13958  discr  13964  sqrlem4  14966  sqrlem7  14969  rpsqrtcl  14985  absrpcl  15009  mulcn2  15314  fprodle  15715  rprisefaccl  15742  rpefcl  15822  eflt  15835  ef01bndlem  15902  stdbdmopn  23683  methaus  23685  nmrpcl  23785  nlmvscnlem1  23859  metnrmlem1a  24030  icopnfcnv  24114  evth  24131  lebnumlem1  24133  nmoleub2lem3  24287  ipcnlem1  24418  minveclem4  24605  pjthlem1  24610  vitalilem4  24784  mbfmulc2lem  24820  itg2gt0  24934  dveflem  25152  dvferm1lem  25157  dvferm2  25160  aaliou3lem3  25513  psercnlem1  25593  pserdvlem1  25595  pserdv  25597  reeff1olem  25614  pilem2  25620  pilem3  25621  tanrpcl  25670  cosordlem  25695  rplogcl  25768  logdivlti  25784  logdivlt  25785  logdivle  25786  recxpcl  25839  rpcxpcl  25840  mulcxp  25849  cxple2  25861  cxpsqrt  25867  cxpcn3  25910  loglesqrt  25920  atanlogaddlem  26072  atantan  26082  atanbnd  26085  rlimcnp  26124  rlimcnp2  26125  efrlim  26128  cxp2limlem  26134  cxp2lim  26135  cxploglim2  26137  jensen  26147  harmonicubnd  26168  fsumharmonic  26170  lgamgulmlem2  26188  ftalem2  26232  basellem3  26241  basellem8  26246  chtrpcl  26333  fsumvma2  26371  chpval2  26375  chpchtsum  26376  chpub  26377  efexple  26438  chebbnd1lem2  26627  chebbnd1lem3  26628  chebbnd1  26629  chtppilimlem1  26630  chtppilimlem2  26631  chtppilim  26632  chebbnd2  26634  chto1lb  26635  chpchtlim  26636  chpo1ub  26637  rplogsumlem2  26642  dchrisumlema  26645  dchrisumlem3  26648  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  dchrisum0lema  26671  chpdifbndlem1  26710  chpdifbndlem2  26711  chpdifbnd  26712  selberg3lem1  26714  pntrsumo1  26722  pntpbnd1a  26742  pntpbnd1  26743  pntpbnd2  26744  pntpbnd  26745  pntibndlem2  26748  pntibndlem3  26749  pntibnd  26750  pntlemd  26751  pntlem3  26766  pntleml  26768  pnt2  26770  pnt  26771  abvcxp  26772  ostth2lem1  26775  padicabv  26787  ostth2lem3  26792  ostth2lem4  26793  ostth2  26794  ostth3  26795  ttgcontlem1  27261  blocnilem  29175  minvecolem4  29251  minvecolem5  29252  pjhthlem1  29762  eigposi  30207  xrge0iifhom  31896  cndprobprob  32414  hgt750lem  32640  unblimceq0lem  34695  unblimceq0  34696  knoppndvlem14  34714  knoppndvlem18  34718  knoppndvlem20  34720  tan2h  35778  mblfinlem3  35825  mblfinlem4  35826  itg2addnclem  35837  itg2gt0cn  35841  ftc1anclem7  35865  ftc1anc  35867  dvasin  35870  areacirclem1  35874  areacirclem4  35877  areacirc  35879  geomcau  35926  blbnd  35954  prdsbnd2  35962  rrnequiv  36002  relogbcld  39988  logblebd  39991  3lexlogpow5ineq2  40070  3lexlogpow2ineq1  40073  3lexlogpow2ineq2  40074  3lexlogpow5ineq5  40075  aks4d1p1p3  40084  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p1  40091  metakunt29  40160  pell14qrrp  40689  pellfundex  40715  pellfundrp  40717  rmspecfund  40738  rmspecpos  40745  areaquad  41054  wwlemuld  41773  radcnvrat  41939  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  supxrgere  42879  supxrgelem  42883  xralrple2  42900  xralrple3  42920  sqrlearg  43098  sinaover2ne0  43416  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnmul  43491  stoweidlem25  43573  stoweidlem28  43576  stoweidlem42  43590  stoweidlem49  43597  wallispilem3  43615  wallispilem4  43616  wallispi  43618  wallispi2lem1  43619  stirlinglem5  43626  stirlinglem10  43631  fourierdlem4  43659  fourierdlem6  43661  fourierdlem7  43662  fourierdlem19  43674  fourierdlem24  43679  fourierdlem26  43681  fourierdlem30  43685  fourierdlem42  43697  fourierdlem51  43705  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem73  43727  fourierdlem75  43729  fourierdlem79  43733  fourierdlem92  43746  fourierdlem109  43763  fouriersw  43779  etransclem35  43817  qndenserrnbllem  43842  ioorrnopnlem  43852  hoiqssbllem1  44167  hoiqssbllem2  44168  iunhoiioolem  44220  pimrecltpos  44253  smfrec  44334  smfmullem1  44336  smfmullem2  44337  smfmullem3  44338  m1mod0mod1  44832  rege1logbrege0  45915  fldivexpfllog2  45922  fllog2  45925  resum2sqrp  46065  eenglngeehlnmlem2  46095  itschlc0xyqsol1  46123  inlinecirc02plem  46143  amgmwlem  46517