Theorem elrpd 12416

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525  0cc0 10526   < clt 10664  ℝ⁺crp 12377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-rp 12378

This theorem is referenced by:  mul2lt0rgt0  12480  mul2lt0bi  12483  xov1plusxeqvd  12876  zltaddlt1le  12883  sqn0rp  13488  ltexp2a  13526  expcan  13529  ltexp2  13530  leexp2a  13532  expnlbnd2  13591  discr  13597  sqrlem4  14597  sqrlem7  14600  rpsqrtcl  14616  absrpcl  14640  mulcn2  14944  fprodle  15342  rprisefaccl  15369  rpefcl  15449  eflt  15462  ef01bndlem  15529  stdbdmopn  23125  methaus  23127  nmrpcl  23226  nlmvscnlem1  23292  metnrmlem1a  23463  icopnfcnv  23547  evth  23564  lebnumlem1  23566  nmoleub2lem3  23720  ipcnlem1  23849  minveclem4  24036  pjthlem1  24041  vitalilem4  24215  mbfmulc2lem  24251  itg2gt0  24364  dveflem  24582  dvferm1lem  24587  dvferm2  24590  aaliou3lem3  24940  psercnlem1  25020  pserdvlem1  25022  pserdv  25024  reeff1olem  25041  pilem2  25047  pilem3  25048  tanrpcl  25097  cosordlem  25122  rplogcl  25195  logdivlti  25211  logdivlt  25212  logdivle  25213  recxpcl  25266  rpcxpcl  25267  mulcxp  25276  cxple2  25288  cxpsqrt  25294  cxpcn3  25337  loglesqrt  25347  atanlogaddlem  25499  atantan  25509  atanbnd  25512  rlimcnp  25551  rlimcnp2  25552  efrlim  25555  cxp2limlem  25561  cxp2lim  25562  cxploglim2  25564  jensen  25574  harmonicubnd  25595  fsumharmonic  25597  lgamgulmlem2  25615  ftalem2  25659  basellem3  25668  basellem8  25673  chtrpcl  25760  fsumvma2  25798  chpval2  25802  chpchtsum  25803  chpub  25804  efexple  25865  chebbnd1lem2  26054  chebbnd1lem3  26055  chebbnd1  26056  chtppilimlem1  26057  chtppilimlem2  26058  chtppilim  26059  chebbnd2  26061  chto1lb  26062  chpchtlim  26063  chpo1ub  26064  rplogsumlem2  26069  dchrisumlema  26072  dchrisumlem3  26075  dchrvmasumlem2  26082  dchrvmasumiflem1  26085  dchrisum0lema  26098  chpdifbndlem1  26137  chpdifbndlem2  26138  chpdifbnd  26139  selberg3lem1  26141  pntrsumo1  26149  pntpbnd1a  26169  pntpbnd1  26170  pntpbnd2  26171  pntpbnd  26172  pntibndlem2  26175  pntibndlem3  26176  pntibnd  26177  pntlemd  26178  pntlem3  26193  pntleml  26195  pnt2  26197  pnt  26198  abvcxp  26199  ostth2lem1  26202  padicabv  26214  ostth2lem3  26219  ostth2lem4  26220  ostth2  26221  ostth3  26222  ttgcontlem1  26679  blocnilem  28587  minvecolem4  28663  minvecolem5  28664  pjhthlem1  29174  eigposi  29619  xrge0iifhom  31290  cndprobprob  31806  hgt750lem  32032  unblimceq0lem  33958  unblimceq0  33959  knoppndvlem14  33977  knoppndvlem18  33981  knoppndvlem20  33983  tan2h  35049  mblfinlem3  35096  mblfinlem4  35097  itg2addnclem  35108  itg2gt0cn  35112  ftc1anclem7  35136  ftc1anc  35138  dvasin  35141  areacirclem1  35145  areacirclem4  35148  areacirc  35150  geomcau  35197  blbnd  35225  prdsbnd2  35233  rrnequiv  35273  relogbcld  39259  logblebd  39262  3lexlogpow5ineq2  39342  metakunt29  39378  pell14qrrp  39801  pellfundex  39827  pellfundrp  39829  rmspecfund  39850  rmspecpos  39857  areaquad  40166  wwlemuld  40859  radcnvrat  41018  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  supxrgere  41965  supxrgelem  41969  xralrple2  41986  xralrple3  42006  sqrlearg  42190  sinaover2ne0  42510  ioodvbdlimc1lem1  42573  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnmul  42585  stoweidlem25  42667  stoweidlem28  42670  stoweidlem42  42684  stoweidlem49  42691  wallispilem3  42709  wallispilem4  42710  wallispi  42712  wallispi2lem1  42713  stirlinglem5  42720  stirlinglem10  42725  fourierdlem4  42753  fourierdlem6  42755  fourierdlem7  42756  fourierdlem19  42768  fourierdlem24  42773  fourierdlem26  42775  fourierdlem30  42779  fourierdlem42  42791  fourierdlem51  42799  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem73  42821  fourierdlem75  42823  fourierdlem79  42827  fourierdlem92  42840  fourierdlem109  42857  fouriersw  42873  etransclem35  42911  qndenserrnbllem  42936  ioorrnopnlem  42946  hoiqssbllem1  43261  hoiqssbllem2  43262  iunhoiioolem  43314  pimrecltpos  43344  smfrec  43421  smfmullem1  43423  smfmullem2  43424  smfmullem3  43425  m1mod0mod1  43886  rege1logbrege0  44972  fldivexpfllog2  44979  fllog2  44982  resum2sqrp  45122  eenglngeehlnmlem2  45152  itschlc0xyqsol1  45180  inlinecirc02plem  45200  amgmwlem  45330