Theorem elrpd 13046

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 13008	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5119  ℝcr 11126  0cc0 11127   < clt 11267  ℝ⁺crp 13006

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-rp 13007

This theorem is referenced by:  mul2lt0rgt0  13110  mul2lt0bi  13113  xov1plusxeqvd  13513  zltaddlt1le  13520  sqn0rp  14143  ltexp2a  14182  expcan  14185  ltexp2  14186  leexp2a  14188  expnlbnd2  14250  discr  14256  01sqrexlem4  15262  01sqrexlem7  15265  rpsqrtcl  15281  absrpcl  15305  mulcn2  15610  fprodle  16010  rprisefaccl  16037  rpefcl  16120  eflt  16133  ef01bndlem  16200  stdbdmopn  24455  methaus  24457  nmrpcl  24557  nlmvscnlem1  24623  metnrmlem1a  24796  icopnfcnv  24889  evth  24907  lebnumlem1  24909  nmoleub2lem3  25064  ipcnlem1  25195  minveclem4  25382  pjthlem1  25387  vitalilem4  25562  mbfmulc2lem  25598  itg2gt0  25711  dveflem  25933  dvferm1lem  25938  dvferm2  25941  aaliou3lem3  26302  psercnlem1  26385  pserdvlem1  26387  pserdv  26389  reeff1olem  26406  pilem2  26412  pilem3  26413  tanrpcl  26463  cosordlem  26489  rplogcl  26563  logdivlti  26579  logdivlt  26580  logdivle  26581  recxpcl  26634  rpcxpcl  26635  mulcxp  26644  cxple2  26656  cxpsqrt  26662  cxpcn3  26708  loglesqrt  26721  atanlogaddlem  26873  atantan  26883  atanbnd  26886  rlimcnp  26925  rlimcnp2  26926  efrlim  26929  efrlimOLD  26930  cxp2limlem  26936  cxp2lim  26937  cxploglim2  26939  jensen  26949  harmonicubnd  26970  fsumharmonic  26972  lgamgulmlem2  26990  ftalem2  27034  basellem3  27043  basellem8  27048  chtrpcl  27135  fsumvma2  27175  chpval2  27179  chpchtsum  27180  chpub  27181  efexple  27242  chebbnd1lem2  27431  chebbnd1lem3  27432  chebbnd1  27433  chtppilimlem1  27434  chtppilimlem2  27435  chtppilim  27436  chebbnd2  27438  chto1lb  27439  chpchtlim  27440  chpo1ub  27441  rplogsumlem2  27446  dchrisumlema  27449  dchrisumlem3  27452  dchrvmasumlem2  27459  dchrvmasumiflem1  27462  dchrisum0lema  27475  chpdifbndlem1  27514  chpdifbndlem2  27515  chpdifbnd  27516  selberg3lem1  27518  pntrsumo1  27526  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntpbnd  27549  pntibndlem2  27552  pntibndlem3  27553  pntibnd  27554  pntlemd  27555  pntlem3  27570  pntleml  27572  pnt2  27574  pnt  27575  abvcxp  27576  ostth2lem1  27579  padicabv  27591  ostth2lem3  27596  ostth2lem4  27597  ostth2  27598  ostth3  27599  ttgcontlem1  28810  blocnilem  30731  minvecolem4  30807  minvecolem5  30808  pjhthlem1  31318  eigposi  31763  2sqr3minply  33760  xrge0iifhom  33914  cndprobprob  34416  hgt750lem  34629  unblimceq0lem  36470  unblimceq0  36471  knoppndvlem14  36489  knoppndvlem18  36493  knoppndvlem20  36495  tan2h  37582  mblfinlem3  37629  mblfinlem4  37630  itg2addnclem  37641  itg2gt0cn  37645  ftc1anclem7  37669  ftc1anc  37671  dvasin  37674  areacirclem1  37678  areacirclem4  37681  areacirc  37683  geomcau  37729  blbnd  37757  prdsbnd2  37765  rrnequiv  37805  relogbcld  41932  logblebd  41935  3lexlogpow5ineq2  42014  3lexlogpow2ineq1  42017  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks6d1c7lem1  42139  metakunt29  42192  explt1d  42319  expeq1d  42320  pell14qrrp  42830  pellfundex  42856  pellfundrp  42858  rmspecfund  42879  rmspecpos  42887  areaquad  43187  wwlemuld  44127  radcnvrat  44286  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  supxrgere  45308  supxrgelem  45312  xralrple2  45329  xralrple3  45349  sqrlearg  45530  sinaover2ne0  45845  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnmul  45920  stoweidlem25  46002  stoweidlem28  46005  stoweidlem42  46019  stoweidlem49  46026  wallispilem3  46044  wallispilem4  46045  wallispi  46047  wallispi2lem1  46048  stirlinglem5  46055  stirlinglem10  46060  fourierdlem4  46088  fourierdlem6  46090  fourierdlem7  46091  fourierdlem19  46103  fourierdlem24  46108  fourierdlem26  46110  fourierdlem30  46114  fourierdlem42  46126  fourierdlem51  46134  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem73  46156  fourierdlem75  46158  fourierdlem79  46162  fourierdlem92  46175  fourierdlem109  46192  fouriersw  46208  etransclem35  46246  qndenserrnbllem  46271  ioorrnopnlem  46281  hoiqssbllem1  46599  hoiqssbllem2  46600  iunhoiioolem  46652  pimrecltpos  46685  smfrec  46766  smfmullem1  46768  smfmullem2  46769  smfmullem3  46770  m1mod0mod1  47331  rege1logbrege0  48486  fldivexpfllog2  48493  fllog2  48496  resum2sqrp  48636  eenglngeehlnmlem2  48666  itschlc0xyqsol1  48694  inlinecirc02plem  48714  amgmwlem  49614