Theorem elrpd 13010

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5148  ℝcr 11106  0cc0 11107   < clt 11245  ℝ⁺crp 12971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-rp 12972

This theorem is referenced by:  mul2lt0rgt0  13074  mul2lt0bi  13077  xov1plusxeqvd  13472  zltaddlt1le  13479  sqn0rp  14089  ltexp2a  14128  expcan  14131  ltexp2  14132  leexp2a  14134  expnlbnd2  14194  discr  14200  01sqrexlem4  15189  01sqrexlem7  15192  rpsqrtcl  15208  absrpcl  15232  mulcn2  15537  fprodle  15937  rprisefaccl  15964  rpefcl  16044  eflt  16057  ef01bndlem  16124  stdbdmopn  24019  methaus  24021  nmrpcl  24121  nlmvscnlem1  24195  metnrmlem1a  24366  icopnfcnv  24450  evth  24467  lebnumlem1  24469  nmoleub2lem3  24623  ipcnlem1  24754  minveclem4  24941  pjthlem1  24946  vitalilem4  25120  mbfmulc2lem  25156  itg2gt0  25270  dveflem  25488  dvferm1lem  25493  dvferm2  25496  aaliou3lem3  25849  psercnlem1  25929  pserdvlem1  25931  pserdv  25933  reeff1olem  25950  pilem2  25956  pilem3  25957  tanrpcl  26006  cosordlem  26031  rplogcl  26104  logdivlti  26120  logdivlt  26121  logdivle  26122  recxpcl  26175  rpcxpcl  26176  mulcxp  26185  cxple2  26197  cxpsqrt  26203  cxpcn3  26246  loglesqrt  26256  atanlogaddlem  26408  atantan  26418  atanbnd  26421  rlimcnp  26460  rlimcnp2  26461  efrlim  26464  cxp2limlem  26470  cxp2lim  26471  cxploglim2  26473  jensen  26483  harmonicubnd  26504  fsumharmonic  26506  lgamgulmlem2  26524  ftalem2  26568  basellem3  26577  basellem8  26582  chtrpcl  26669  fsumvma2  26707  chpval2  26711  chpchtsum  26712  chpub  26713  efexple  26774  chebbnd1lem2  26963  chebbnd1lem3  26964  chebbnd1  26965  chtppilimlem1  26966  chtppilimlem2  26967  chtppilim  26968  chebbnd2  26970  chto1lb  26971  chpchtlim  26972  chpo1ub  26973  rplogsumlem2  26978  dchrisumlema  26981  dchrisumlem3  26984  dchrvmasumlem2  26991  dchrvmasumiflem1  26994  dchrisum0lema  27007  chpdifbndlem1  27046  chpdifbndlem2  27047  chpdifbnd  27048  selberg3lem1  27050  pntrsumo1  27058  pntpbnd1a  27078  pntpbnd1  27079  pntpbnd2  27080  pntpbnd  27081  pntibndlem2  27084  pntibndlem3  27085  pntibnd  27086  pntlemd  27087  pntlem3  27102  pntleml  27104  pnt2  27106  pnt  27107  abvcxp  27108  ostth2lem1  27111  padicabv  27123  ostth2lem3  27128  ostth2lem4  27129  ostth2  27130  ostth3  27131  ttgcontlem1  28132  blocnilem  30045  minvecolem4  30121  minvecolem5  30122  pjhthlem1  30632  eigposi  31077  xrge0iifhom  32906  cndprobprob  33426  hgt750lem  33652  unblimceq0lem  35371  unblimceq0  35372  knoppndvlem14  35390  knoppndvlem18  35394  knoppndvlem20  35396  tan2h  36469  mblfinlem3  36516  mblfinlem4  36517  itg2addnclem  36528  itg2gt0cn  36532  ftc1anclem7  36556  ftc1anc  36558  dvasin  36561  areacirclem1  36565  areacirclem4  36568  areacirc  36570  geomcau  36616  blbnd  36644  prdsbnd2  36652  rrnequiv  36692  relogbcld  40827  logblebd  40830  3lexlogpow5ineq2  40909  3lexlogpow2ineq1  40912  3lexlogpow2ineq2  40913  3lexlogpow5ineq5  40914  aks4d1p1p3  40923  aks4d1p1p2  40924  aks4d1p1p4  40925  aks4d1p1p6  40927  aks4d1p1p7  40928  aks4d1p1p5  40929  aks4d1p1  40930  metakunt29  41002  pell14qrrp  41584  pellfundex  41610  pellfundrp  41612  rmspecfund  41633  rmspecpos  41641  areaquad  41951  wwlemuld  42893  radcnvrat  43059  binomcxplemdvbinom  43098  binomcxplemnotnn0  43101  supxrgere  44030  supxrgelem  44034  xralrple2  44051  xralrple3  44071  sqrlearg  44253  sinaover2ne0  44571  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnmul  44646  stoweidlem25  44728  stoweidlem28  44731  stoweidlem42  44745  stoweidlem49  44752  wallispilem3  44770  wallispilem4  44771  wallispi  44773  wallispi2lem1  44774  stirlinglem5  44781  stirlinglem10  44786  fourierdlem4  44814  fourierdlem6  44816  fourierdlem7  44817  fourierdlem19  44829  fourierdlem24  44834  fourierdlem26  44836  fourierdlem30  44840  fourierdlem42  44852  fourierdlem51  44860  fourierdlem63  44872  fourierdlem64  44873  fourierdlem65  44874  fourierdlem73  44882  fourierdlem75  44884  fourierdlem79  44888  fourierdlem92  44901  fourierdlem109  44918  fouriersw  44934  etransclem35  44972  qndenserrnbllem  44997  ioorrnopnlem  45007  hoiqssbllem1  45325  hoiqssbllem2  45326  iunhoiioolem  45378  pimrecltpos  45411  smfrec  45492  smfmullem1  45494  smfmullem2  45495  smfmullem3  45496  m1mod0mod1  46024  rege1logbrege0  47198  fldivexpfllog2  47205  fllog2  47208  resum2sqrp  47348  eenglngeehlnmlem2  47378  itschlc0xyqsol1  47406  inlinecirc02plem  47426  amgmwlem  47803