Theorem elrpd 11745

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

Syntax hints:   → wi 4   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814  0cc0 9815   < clt 9953  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-rp 11709

This theorem is referenced by:  mul2lt0rgt0  11809  mul2lt0bi  11812  xov1plusxeqvd  12189  zltaddlt1le  12195  ltexp2a  12774  expcan  12775  ltexp2  12776  leexp2a  12778  expnlbnd2  12857  discr  12863  sqrlem4  13834  sqrlem7  13837  rpsqrtcl  13853  absrpcl  13876  rlimrege0  14158  mulcn2  14174  fprodle  14566  rprisefaccl  14593  rpefcl  14673  eflt  14686  ef01bndlem  14753  stdbdmopn  22133  methaus  22135  nmrpcl  22234  nlmvscnlem1  22300  metnrmlem1a  22469  icopnfcnv  22549  evth  22566  lebnumlem1  22568  nmoleub2lem3  22723  ipcnlem1  22852  minveclem4  23011  vitalilem4  23186  mbfmulc2lem  23220  itg2gt0  23333  dveflem  23546  dvferm1lem  23551  dvferm2  23554  aaliou3lem3  23903  psercnlem1  23983  pserdvlem1  23985  pserdv  23987  reeff1olem  24004  pilem2  24010  pilem3  24011  tanrpcl  24060  cosordlem  24081  rplogcl  24154  logdivlti  24170  logdivlt  24171  logdivle  24172  dvloglem  24194  recxpcl  24221  rpcxpcl  24222  mulcxp  24231  cxple2  24243  cxpsqrt  24249  cxpcn3  24289  loglesqrt  24299  atanlogaddlem  24440  atantan  24450  atanbnd  24453  rlimcnp  24492  rlimcnp2  24493  efrlim  24496  cxp2limlem  24502  cxp2lim  24503  cxploglim2  24505  jensen  24515  harmonicubnd  24536  fsumharmonic  24538  lgamgulmlem2  24556  ftalem2  24600  basellem3  24609  basellem8  24614  chtrpcl  24701  fsumvma2  24739  chpval2  24743  chpchtsum  24744  chpub  24745  efexple  24806  chebbnd1lem2  24959  chebbnd1lem3  24960  chebbnd1  24961  chtppilimlem1  24962  chtppilimlem2  24963  chtppilim  24964  chebbnd2  24966  chto1lb  24967  chpchtlim  24968  chpo1ub  24969  rplogsumlem2  24974  dchrisumlema  24977  dchrisumlem3  24980  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  dchrisum0lema  25003  chpdifbndlem1  25042  chpdifbndlem2  25043  chpdifbnd  25044  selberg3lem1  25046  pntrsumo1  25054  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntpbnd  25077  pntibndlem2  25080  pntibndlem3  25081  pntibnd  25082  pntlemd  25083  pntlem3  25098  pntleml  25100  pnt2  25102  pnt  25103  abvcxp  25104  ostth2lem1  25107  padicabv  25119  ostth2lem3  25124  ostth2lem4  25125  ostth2  25126  ostth3  25127  ttgcontlem1  25565  blocnilem  27043  minvecolem4  27120  minvecolem5  27121  xrge0iifhom  29311  cndprobprob  29827  unblimceq0lem  31667  unblimceq0  31668  knoppndvlem14  31686  knoppndvlem18  31690  knoppndvlem20  31692  tan2h  32571  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem  32631  itg2gt0cn  32635  ftc1anclem7  32661  ftc1anc  32663  dvasin  32666  areacirclem1  32670  areacirclem4  32673  areacirc  32675  geomcau  32725  blbnd  32756  prdsbnd2  32764  rrnequiv  32804  pell14qrrp  36442  pellfundex  36468  pellfundrp  36470  rmspecfund  36492  rmspecpos  36499  areaquad  36821  wwlemuld  37474  radcnvrat  37535  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  supxrgere  38490  supxrgelem  38494  xralrple2  38511  xralrple3  38531  sqrlearg  38627  sinaover2ne0  38751  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmul  38833  stoweidlem25  38918  stoweidlem28  38921  stoweidlem42  38935  stoweidlem49  38942  wallispilem3  38960  wallispilem4  38961  wallispi  38963  wallispi2lem1  38964  stirlinglem5  38971  stirlinglem10  38976  fourierdlem4  39004  fourierdlem6  39006  fourierdlem7  39007  fourierdlem19  39019  fourierdlem24  39024  fourierdlem26  39026  fourierdlem30  39030  fourierdlem42  39042  fourierdlem51  39050  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem73  39072  fourierdlem75  39074  fourierdlem79  39078  fourierdlem92  39091  fourierdlem109  39108  fouriersw  39124  etransclem35  39162  qndenserrnbllem  39190  ioorrnopnlem  39200  hoiqssbllem1  39512  hoiqssbllem2  39513  iunhoiioolem  39566  pimrecltpos  39596  smfrec  39674  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  m1mod0mod1  39949  rege1logbrege0  42150  fldivexpfllog2  42157  fllog2  42160  amgmwlem  42357