Theorem elrpd 12974

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

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5072  ℝcr 11028  0cc0 11029   < clt 11170  ℝ⁺crp 12933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-rp 12934

This theorem is referenced by:  mul2lt0rgt0  13038  mul2lt0bi  13041  xov1plusxeqvd  13442  zltaddlt1le  13449  sqn0rp  14080  ltexp2a  14119  expcan  14122  ltexp2  14123  leexp2a  14125  expnlbnd2  14187  discr  14193  01sqrexlem4  15198  01sqrexlem7  15201  rpsqrtcl  15217  absrpcl  15241  mulcn2  15549  fprodle  15952  rprisefaccl  15979  rpefcl  16062  eflt  16075  ef01bndlem  16142  stdbdmopn  24501  methaus  24503  nmrpcl  24603  nlmvscnlem1  24669  metnrmlem1a  24842  icopnfcnv  24927  evth  24944  lebnumlem1  24946  nmoleub2lem3  25100  ipcnlem1  25230  minveclem4  25417  pjthlem1  25422  vitalilem4  25596  mbfmulc2lem  25632  itg2gt0  25745  dveflem  25964  dvferm1lem  25969  dvferm2  25972  aaliou3lem3  26328  psercnlem1  26408  pserdvlem1  26410  pserdv  26412  reeff1olem  26429  pilem2  26435  pilem3  26436  tanrpcl  26486  cosordlem  26512  rplogcl  26586  logdivlti  26602  logdivlt  26603  logdivle  26604  recxpcl  26657  rpcxpcl  26658  mulcxp  26667  cxple2  26679  cxpsqrt  26685  cxpcn3  26730  loglesqrt  26743  atanlogaddlem  26895  atantan  26905  atanbnd  26908  rlimcnp  26947  rlimcnp2  26948  efrlim  26951  cxp2limlem  26957  cxp2lim  26958  cxploglim2  26960  jensen  26970  harmonicubnd  26991  fsumharmonic  26993  lgamgulmlem2  27011  ftalem2  27055  basellem3  27064  basellem8  27069  chtrpcl  27156  fsumvma2  27195  chpval2  27199  chpchtsum  27200  chpub  27201  efexple  27262  chebbnd1lem2  27451  chebbnd1lem3  27452  chebbnd1  27453  chtppilimlem1  27454  chtppilimlem2  27455  chtppilim  27456  chebbnd2  27458  chto1lb  27459  chpchtlim  27460  chpo1ub  27461  rplogsumlem2  27466  dchrisumlema  27469  dchrisumlem3  27472  dchrvmasumlem2  27479  dchrvmasumiflem1  27482  dchrisum0lema  27495  chpdifbndlem1  27534  chpdifbndlem2  27535  chpdifbnd  27536  selberg3lem1  27538  pntrsumo1  27546  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  pntpbnd  27569  pntibndlem2  27572  pntibndlem3  27573  pntibnd  27574  pntlemd  27575  pntlem3  27590  pntleml  27592  pnt2  27594  pnt  27595  abvcxp  27596  ostth2lem1  27599  padicabv  27611  ostth2lem3  27616  ostth2lem4  27617  ostth2  27618  ostth3  27619  ttgcontlem1  28971  blocnilem  30893  minvecolem4  30969  minvecolem5  30970  pjhthlem1  31480  eigposi  31925  2sqr3minply  33964  xrge0iifhom  34121  cndprobprob  34622  hgt750lem  34835  unblimceq0lem  36812  unblimceq0  36813  knoppndvlem14  36831  knoppndvlem18  36835  knoppndvlem20  36837  tan2h  37979  mblfinlem3  38026  mblfinlem4  38027  itg2addnclem  38038  itg2gt0cn  38042  ftc1anclem7  38066  ftc1anc  38068  dvasin  38071  areacirclem1  38075  areacirclem4  38078  areacirc  38080  geomcau  38126  blbnd  38154  prdsbnd2  38162  rrnequiv  38202  relogbcld  42459  logblebd  42462  3lexlogpow5ineq2  42540  3lexlogpow2ineq1  42543  3lexlogpow2ineq2  42544  3lexlogpow5ineq5  42545  aks4d1p1p3  42554  aks4d1p1p2  42555  aks4d1p1p4  42556  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p1  42561  aks6d1c7lem1  42665  explt1d  42800  expeq1d  42801  pell14qrrp  43305  pellfundex  43331  pellfundrp  43333  rmspecfund  43354  rmspecpos  43361  areaquad  43661  wwlemuld  44600  radcnvrat  44758  binomcxplemdvbinom  44797  binomcxplemnotnn0  44800  supxrgere  45778  supxrgelem  45782  xralrple2  45799  xralrple3  45818  sqrlearg  45998  sinaover2ne0  46311  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnmul  46386  stoweidlem25  46468  stoweidlem28  46471  stoweidlem42  46485  stoweidlem49  46492  wallispilem3  46510  wallispilem4  46511  wallispi  46513  wallispi2lem1  46514  stirlinglem5  46521  stirlinglem10  46526  fourierdlem4  46554  fourierdlem6  46556  fourierdlem7  46557  fourierdlem19  46569  fourierdlem24  46574  fourierdlem26  46576  fourierdlem30  46580  fourierdlem42  46592  fourierdlem51  46600  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem73  46622  fourierdlem75  46624  fourierdlem79  46628  fourierdlem92  46641  fourierdlem109  46658  fouriersw  46674  etransclem35  46712  qndenserrnbllem  46737  ioorrnopnlem  46747  hoiqssbllem1  47065  hoiqssbllem2  47066  iunhoiioolem  47118  pimrecltpos  47151  smfrec  47232  smfmullem1  47234  smfmullem2  47235  smfmullem3  47236  m1mod0mod1  47823  rege1logbrege0  49049  fldivexpfllog2  49056  fllog2  49059  resum2sqrp  49199  eenglngeehlnmlem2  49229  itschlc0xyqsol1  49257  inlinecirc02plem  49277  amgmwlem  50292