Theorem elrpd 13019

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

Syntax hints:   → wi 4   ∈ wcel 2104   class class class wbr 5149  ℝcr 11113  0cc0 11114   < clt 11254  ℝ⁺crp 12980

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-rp 12981

This theorem is referenced by:  mul2lt0rgt0  13083  mul2lt0bi  13086  xov1plusxeqvd  13481  zltaddlt1le  13488  sqn0rp  14098  ltexp2a  14137  expcan  14140  ltexp2  14141  leexp2a  14143  expnlbnd2  14203  discr  14209  01sqrexlem4  15198  01sqrexlem7  15201  rpsqrtcl  15217  absrpcl  15241  mulcn2  15546  fprodle  15946  rprisefaccl  15973  rpefcl  16053  eflt  16066  ef01bndlem  16133  stdbdmopn  24249  methaus  24251  nmrpcl  24351  nlmvscnlem1  24425  metnrmlem1a  24596  icopnfcnv  24689  evth  24707  lebnumlem1  24709  nmoleub2lem3  24864  ipcnlem1  24995  minveclem4  25182  pjthlem1  25187  vitalilem4  25362  mbfmulc2lem  25398  itg2gt0  25512  dveflem  25730  dvferm1lem  25735  dvferm2  25738  aaliou3lem3  26091  psercnlem1  26171  pserdvlem1  26173  pserdv  26175  reeff1olem  26192  pilem2  26198  pilem3  26199  tanrpcl  26248  cosordlem  26273  rplogcl  26346  logdivlti  26362  logdivlt  26363  logdivle  26364  recxpcl  26417  rpcxpcl  26418  mulcxp  26427  cxple2  26439  cxpsqrt  26445  cxpcn3  26490  loglesqrt  26500  atanlogaddlem  26652  atantan  26662  atanbnd  26665  rlimcnp  26704  rlimcnp2  26705  efrlim  26708  cxp2limlem  26714  cxp2lim  26715  cxploglim2  26717  jensen  26727  harmonicubnd  26748  fsumharmonic  26750  lgamgulmlem2  26768  ftalem2  26812  basellem3  26821  basellem8  26826  chtrpcl  26913  fsumvma2  26951  chpval2  26955  chpchtsum  26956  chpub  26957  efexple  27018  chebbnd1lem2  27207  chebbnd1lem3  27208  chebbnd1  27209  chtppilimlem1  27210  chtppilimlem2  27211  chtppilim  27212  chebbnd2  27214  chto1lb  27215  chpchtlim  27216  chpo1ub  27217  rplogsumlem2  27222  dchrisumlema  27225  dchrisumlem3  27228  dchrvmasumlem2  27235  dchrvmasumiflem1  27238  dchrisum0lema  27251  chpdifbndlem1  27290  chpdifbndlem2  27291  chpdifbnd  27292  selberg3lem1  27294  pntrsumo1  27302  pntpbnd1a  27322  pntpbnd1  27323  pntpbnd2  27324  pntpbnd  27325  pntibndlem2  27328  pntibndlem3  27329  pntibnd  27330  pntlemd  27331  pntlem3  27346  pntleml  27348  pnt2  27350  pnt  27351  abvcxp  27352  ostth2lem1  27355  padicabv  27367  ostth2lem3  27372  ostth2lem4  27373  ostth2  27374  ostth3  27375  ttgcontlem1  28407  blocnilem  30322  minvecolem4  30398  minvecolem5  30399  pjhthlem1  30909  eigposi  31354  xrge0iifhom  33213  cndprobprob  33733  hgt750lem  33959  unblimceq0lem  35687  unblimceq0  35688  knoppndvlem14  35706  knoppndvlem18  35710  knoppndvlem20  35712  tan2h  36785  mblfinlem3  36832  mblfinlem4  36833  itg2addnclem  36844  itg2gt0cn  36848  ftc1anclem7  36872  ftc1anc  36874  dvasin  36877  areacirclem1  36881  areacirclem4  36884  areacirc  36886  geomcau  36932  blbnd  36960  prdsbnd2  36968  rrnequiv  37008  relogbcld  41146  logblebd  41149  3lexlogpow5ineq2  41228  3lexlogpow2ineq1  41231  3lexlogpow2ineq2  41232  3lexlogpow5ineq5  41233  aks4d1p1p3  41242  aks4d1p1p2  41243  aks4d1p1p4  41244  aks4d1p1p6  41246  aks4d1p1p7  41247  aks4d1p1p5  41248  aks4d1p1  41249  metakunt29  41321  pell14qrrp  41902  pellfundex  41928  pellfundrp  41930  rmspecfund  41951  rmspecpos  41959  areaquad  42269  wwlemuld  43211  radcnvrat  43377  binomcxplemdvbinom  43416  binomcxplemnotnn0  43419  supxrgere  44343  supxrgelem  44347  xralrple2  44364  xralrple3  44384  sqrlearg  44566  sinaover2ne0  44884  ioodvbdlimc1lem1  44947  ioodvbdlimc1lem2  44948  ioodvbdlimc2lem  44950  dvnmul  44959  stoweidlem25  45041  stoweidlem28  45044  stoweidlem42  45058  stoweidlem49  45065  wallispilem3  45083  wallispilem4  45084  wallispi  45086  wallispi2lem1  45087  stirlinglem5  45094  stirlinglem10  45099  fourierdlem4  45127  fourierdlem6  45129  fourierdlem7  45130  fourierdlem19  45142  fourierdlem24  45147  fourierdlem26  45149  fourierdlem30  45153  fourierdlem42  45165  fourierdlem51  45173  fourierdlem63  45185  fourierdlem64  45186  fourierdlem65  45187  fourierdlem73  45195  fourierdlem75  45197  fourierdlem79  45201  fourierdlem92  45214  fourierdlem109  45231  fouriersw  45247  etransclem35  45285  qndenserrnbllem  45310  ioorrnopnlem  45320  hoiqssbllem1  45638  hoiqssbllem2  45639  iunhoiioolem  45691  pimrecltpos  45724  smfrec  45805  smfmullem1  45807  smfmullem2  45808  smfmullem3  45809  m1mod0mod1  46337  rege1logbrege0  47333  fldivexpfllog2  47340  fllog2  47343  resum2sqrp  47483  eenglngeehlnmlem2  47513  itschlc0xyqsol1  47541  inlinecirc02plem  47561  amgmwlem  47938