Theorem elrpd 12946

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025  0cc0 11026   < clt 11166  ℝ⁺crp 12905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-rp 12906

This theorem is referenced by:  mul2lt0rgt0  13010  mul2lt0bi  13013  xov1plusxeqvd  13414  zltaddlt1le  13421  sqn0rp  14050  ltexp2a  14089  expcan  14092  ltexp2  14093  leexp2a  14095  expnlbnd2  14157  discr  14163  01sqrexlem4  15168  01sqrexlem7  15171  rpsqrtcl  15187  absrpcl  15211  mulcn2  15519  fprodle  15919  rprisefaccl  15946  rpefcl  16029  eflt  16042  ef01bndlem  16109  stdbdmopn  24462  methaus  24464  nmrpcl  24564  nlmvscnlem1  24630  metnrmlem1a  24803  icopnfcnv  24896  evth  24914  lebnumlem1  24916  nmoleub2lem3  25071  ipcnlem1  25201  minveclem4  25388  pjthlem1  25393  vitalilem4  25568  mbfmulc2lem  25604  itg2gt0  25717  dveflem  25939  dvferm1lem  25944  dvferm2  25947  aaliou3lem3  26308  psercnlem1  26391  pserdvlem1  26393  pserdv  26395  reeff1olem  26412  pilem2  26418  pilem3  26419  tanrpcl  26469  cosordlem  26495  rplogcl  26569  logdivlti  26585  logdivlt  26586  logdivle  26587  recxpcl  26640  rpcxpcl  26641  mulcxp  26650  cxple2  26662  cxpsqrt  26668  cxpcn3  26714  loglesqrt  26727  atanlogaddlem  26879  atantan  26889  atanbnd  26892  rlimcnp  26931  rlimcnp2  26932  efrlim  26935  efrlimOLD  26936  cxp2limlem  26942  cxp2lim  26943  cxploglim2  26945  jensen  26955  harmonicubnd  26976  fsumharmonic  26978  lgamgulmlem2  26996  ftalem2  27040  basellem3  27049  basellem8  27054  chtrpcl  27141  fsumvma2  27181  chpval2  27185  chpchtsum  27186  chpub  27187  efexple  27248  chebbnd1lem2  27437  chebbnd1lem3  27438  chebbnd1  27439  chtppilimlem1  27440  chtppilimlem2  27441  chtppilim  27442  chebbnd2  27444  chto1lb  27445  chpchtlim  27446  chpo1ub  27447  rplogsumlem2  27452  dchrisumlema  27455  dchrisumlem3  27458  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  dchrisum0lema  27481  chpdifbndlem1  27520  chpdifbndlem2  27521  chpdifbnd  27522  selberg3lem1  27524  pntrsumo1  27532  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntpbnd  27555  pntibndlem2  27558  pntibndlem3  27559  pntibnd  27560  pntlemd  27561  pntlem3  27576  pntleml  27578  pnt2  27580  pnt  27581  abvcxp  27582  ostth2lem1  27585  padicabv  27597  ostth2lem3  27602  ostth2lem4  27603  ostth2  27604  ostth3  27605  ttgcontlem1  28957  blocnilem  30879  minvecolem4  30955  minvecolem5  30956  pjhthlem1  31466  eigposi  31911  2sqr3minply  33937  xrge0iifhom  34094  cndprobprob  34595  hgt750lem  34808  unblimceq0lem  36706  unblimceq0  36707  knoppndvlem14  36725  knoppndvlem18  36729  knoppndvlem20  36731  tan2h  37813  mblfinlem3  37860  mblfinlem4  37861  itg2addnclem  37872  itg2gt0cn  37876  ftc1anclem7  37900  ftc1anc  37902  dvasin  37905  areacirclem1  37909  areacirclem4  37912  areacirc  37914  geomcau  37960  blbnd  37988  prdsbnd2  37996  rrnequiv  38036  relogbcld  42237  logblebd  42240  3lexlogpow5ineq2  42319  3lexlogpow2ineq1  42322  3lexlogpow2ineq2  42323  3lexlogpow5ineq5  42324  aks4d1p1p3  42333  aks4d1p1p2  42334  aks4d1p1p4  42335  aks4d1p1p6  42337  aks4d1p1p7  42338  aks4d1p1p5  42339  aks4d1p1  42340  aks6d1c7lem1  42444  explt1d  42588  expeq1d  42589  pell14qrrp  43112  pellfundex  43138  pellfundrp  43140  rmspecfund  43161  rmspecpos  43168  areaquad  43468  wwlemuld  44407  radcnvrat  44565  binomcxplemdvbinom  44604  binomcxplemnotnn0  44607  supxrgere  45588  supxrgelem  45592  xralrple2  45609  xralrple3  45628  sqrlearg  45809  sinaover2ne0  46122  ioodvbdlimc1lem1  46185  ioodvbdlimc1lem2  46186  ioodvbdlimc2lem  46188  dvnmul  46197  stoweidlem25  46279  stoweidlem28  46282  stoweidlem42  46296  stoweidlem49  46303  wallispilem3  46321  wallispilem4  46322  wallispi  46324  wallispi2lem1  46325  stirlinglem5  46332  stirlinglem10  46337  fourierdlem4  46365  fourierdlem6  46367  fourierdlem7  46368  fourierdlem19  46380  fourierdlem24  46385  fourierdlem26  46387  fourierdlem30  46391  fourierdlem42  46403  fourierdlem51  46411  fourierdlem63  46423  fourierdlem64  46424  fourierdlem65  46425  fourierdlem73  46433  fourierdlem75  46435  fourierdlem79  46439  fourierdlem92  46452  fourierdlem109  46469  fouriersw  46485  etransclem35  46523  qndenserrnbllem  46548  ioorrnopnlem  46558  hoiqssbllem1  46876  hoiqssbllem2  46877  iunhoiioolem  46929  pimrecltpos  46962  smfrec  47043  smfmullem1  47045  smfmullem2  47046  smfmullem3  47047  m1mod0mod1  47610  rege1logbrege0  48814  fldivexpfllog2  48821  fllog2  48824  resum2sqrp  48964  eenglngeehlnmlem2  48994  itschlc0xyqsol1  49022  inlinecirc02plem  49042  amgmwlem  50057