Theorem elrpd 13029

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

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5099  ℝcr 11067  0cc0 11068   < clt 11211  ℝ⁺crp 12988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-rp 12989

This theorem is referenced by:  mul2lt0rgt0  13093  mul2lt0bi  13096  xov1plusxeqvd  13497  zltaddlt1le  13504  sqn0rp  14135  ltexp2a  14174  expcan  14177  ltexp2  14178  leexp2a  14180  expnlbnd2  14242  discr  14248  01sqrexlem4  15253  01sqrexlem7  15256  rpsqrtcl  15272  absrpcl  15296  mulcn2  15604  fprodle  16007  rprisefaccl  16034  rpefcl  16117  eflt  16130  ef01bndlem  16197  stdbdmopn  24556  methaus  24558  nmrpcl  24658  nlmvscnlem1  24724  metnrmlem1a  24897  icopnfcnv  24982  evth  24999  lebnumlem1  25001  nmoleub2lem3  25155  ipcnlem1  25285  minveclem4  25472  pjthlem1  25477  vitalilem4  25651  mbfmulc2lem  25687  itg2gt0  25800  dveflem  26019  dvferm1lem  26024  dvferm2  26027  aaliou3lem3  26383  psercnlem1  26463  pserdvlem1  26465  pserdv  26467  reeff1olem  26484  pilem2  26490  pilem3  26491  tanrpcl  26544  cosordlem  26570  rplogcl  26644  logdivlti  26660  logdivlt  26661  logdivle  26662  recxpcl  26715  rpcxpcl  26716  mulcxp  26725  cxple2  26737  cxpsqrt  26743  cxpcn3  26788  loglesqrt  26801  atanlogaddlem  26953  atantan  26963  atanbnd  26966  rlimcnp  27005  rlimcnp2  27006  efrlim  27009  cxp2limlem  27015  cxp2lim  27016  cxploglim2  27018  jensen  27028  harmonicubnd  27049  fsumharmonic  27051  lgamgulmlem2  27069  ftalem2  27113  basellem3  27122  basellem8  27127  chtrpcl  27214  fsumvma2  27253  chpval2  27257  chpchtsum  27258  chpub  27259  efexple  27320  chebbnd1lem2  27509  chebbnd1lem3  27510  chebbnd1  27511  chtppilimlem1  27512  chtppilimlem2  27513  chtppilim  27514  chebbnd2  27516  chto1lb  27517  chpchtlim  27518  chpo1ub  27519  rplogsumlem2  27524  dchrisumlema  27527  dchrisumlem3  27530  dchrvmasumlem2  27537  dchrvmasumiflem1  27540  dchrisum0lema  27553  chpdifbndlem1  27592  chpdifbndlem2  27593  chpdifbnd  27594  selberg3lem1  27596  pntrsumo1  27604  pntpbnd1a  27624  pntpbnd1  27625  pntpbnd2  27626  pntpbnd  27627  pntibndlem2  27630  pntibndlem3  27631  pntibnd  27632  pntlemd  27633  pntlem3  27648  pntleml  27650  pnt2  27652  pnt  27653  abvcxp  27654  ostth2lem1  27657  padicabv  27669  ostth2lem3  27674  ostth2lem4  27675  ostth2  27676  ostth3  27677  ttgcontlem1  29029  blocnilem  30951  minvecolem4  31027  minvecolem5  31028  pjhthlem1  31538  eigposi  31983  2sqr3minply  34036  xrge0iifhom  34193  cndprobprob  34694  hgt750lem  34907  unblimceq0lem  36897  unblimceq0  36898  knoppndvlem14  36916  knoppndvlem18  36920  knoppndvlem20  36922  tan2h  38064  mblfinlem3  38111  mblfinlem4  38112  itg2addnclem  38123  itg2gt0cn  38127  ftc1anclem7  38151  ftc1anc  38153  dvasin  38156  areacirclem1  38160  areacirclem4  38163  areacirc  38165  geomcau  38211  blbnd  38239  prdsbnd2  38247  rrnequiv  38287  relogbcld  42544  logblebd  42547  3lexlogpow5ineq2  42625  3lexlogpow2ineq1  42628  3lexlogpow2ineq2  42629  3lexlogpow5ineq5  42630  aks4d1p1p3  42639  aks4d1p1p2  42640  aks4d1p1p4  42641  aks4d1p1p6  42643  aks4d1p1p7  42644  aks4d1p1p5  42645  aks4d1p1  42646  aks6d1c7lem1  42750  explt1d  42885  expeq1d  42886  pell14qrrp  43390  pellfundex  43416  pellfundrp  43418  rmspecfund  43439  rmspecpos  43446  areaquad  43746  wwlemuld  44685  radcnvrat  44843  binomcxplemdvbinom  44882  binomcxplemnotnn0  44885  supxrgere  45862  supxrgelem  45866  xralrple2  45883  xralrple3  45902  sqrlearg  46082  sinaover2ne0  46395  ioodvbdlimc1lem1  46458  ioodvbdlimc1lem2  46459  ioodvbdlimc2lem  46461  dvnmul  46470  stoweidlem25  46552  stoweidlem28  46555  stoweidlem42  46569  stoweidlem49  46576  wallispilem3  46594  wallispilem4  46595  wallispi  46597  wallispi2lem1  46598  stirlinglem5  46605  stirlinglem10  46610  fourierdlem4  46638  fourierdlem6  46640  fourierdlem7  46641  fourierdlem19  46653  fourierdlem24  46658  fourierdlem26  46660  fourierdlem30  46664  fourierdlem42  46676  fourierdlem51  46684  fourierdlem63  46696  fourierdlem64  46697  fourierdlem65  46698  fourierdlem73  46706  fourierdlem75  46708  fourierdlem79  46712  fourierdlem92  46725  fourierdlem109  46742  fouriersw  46758  etransclem35  46796  qndenserrnbllem  46821  ioorrnopnlem  46831  hoiqssbllem1  47149  hoiqssbllem2  47150  iunhoiioolem  47202  pimrecltpos  47235  smfrec  47316  smfmullem1  47318  smfmullem2  47319  smfmullem3  47320  m1mod0mod1  47907  rege1logbrege0  49133  fldivexpfllog2  49140  fllog2  49143  resum2sqrp  49283  eenglngeehlnmlem2  49313  itschlc0xyqsol1  49341  inlinecirc02plem  49361  amgmwlem  50376