Theorem elrpd 13057

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5113  ℝcr 11099  0cc0 11100   < clt 11243  ℝ⁺crp 13016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-rp 13017

This theorem is referenced by:  mul2lt0rgt0  13121  mul2lt0bi  13124  xov1plusxeqvd  13525  zltaddlt1le  13532  sqn0rp  14163  ltexp2a  14202  expcan  14205  ltexp2  14206  leexp2a  14208  expnlbnd2  14270  discr  14276  01sqrexlem4  15296  01sqrexlem7  15299  rpsqrtcl  15315  absrpcl  15339  mulcn2  15647  fprodle  16050  rprisefaccl  16077  rpefcl  16160  eflt  16173  ef01bndlem  16240  stdbdmopn  24644  methaus  24646  nmrpcl  24746  nlmvscnlem1  24812  metnrmlem1a  24985  icopnfcnv  25070  evth  25087  lebnumlem1  25089  nmoleub2lem3  25243  ipcnlem1  25373  minveclem4  25560  pjthlem1  25565  vitalilem4  25739  mbfmulc2lem  25775  itg2gt0  25888  dveflem  26107  dvferm1lem  26112  dvferm2  26115  aaliou3lem3  26474  psercnlem1  26554  pserdvlem1  26556  pserdv  26558  reeff1olem  26575  pilem2  26581  pilem3  26582  tanrpcl  26635  cosordlem  26661  rplogcl  26735  logdivlti  26751  logdivlt  26752  logdivle  26753  recxpcl  26806  rpcxpcl  26807  mulcxp  26816  cxple2  26828  cxpsqrt  26834  cxpcn3  26879  loglesqrt  26892  atanlogaddlem  27044  atantan  27054  atanbnd  27057  rlimcnp  27096  rlimcnp2  27097  efrlim  27100  cxp2limlem  27106  cxp2lim  27107  cxploglim2  27109  jensen  27119  harmonicubnd  27140  fsumharmonic  27142  lgamgulmlem2  27160  ftalem2  27204  basellem3  27213  basellem8  27218  chtrpcl  27305  fsumvma2  27344  chpval2  27348  chpchtsum  27349  chpub  27350  efexple  27411  chebbnd1lem2  27600  chebbnd1lem3  27601  chebbnd1  27602  chtppilimlem1  27603  chtppilimlem2  27604  chtppilim  27605  chebbnd2  27607  chto1lb  27608  chpchtlim  27609  chpo1ub  27610  rplogsumlem2  27615  dchrisumlema  27618  dchrisumlem3  27621  dchrvmasumlem2  27628  dchrvmasumiflem1  27631  dchrisum0lema  27644  chpdifbndlem1  27683  chpdifbndlem2  27684  chpdifbnd  27685  selberg3lem1  27687  pntrsumo1  27695  pntpbnd1a  27715  pntpbnd1  27716  pntpbnd2  27717  pntpbnd  27718  pntibndlem2  27721  pntibndlem3  27722  pntibnd  27723  pntlemd  27724  pntlem3  27739  pntleml  27741  pnt2  27743  pnt  27744  abvcxp  27745  ostth2lem1  27748  padicabv  27760  ostth2lem3  27765  ostth2lem4  27766  ostth2  27767  ostth3  27768  ttgcontlem1  29175  blocnilem  31097  minvecolem4  31173  minvecolem5  31174  pjhthlem1  31684  eigposi  32129  2sqr3minply  34115  xrge0iifhom  34272  cndprobprob  34773  hgt750lem  34983  unblimceq0lem  37018  unblimceq0  37019  knoppndvlem14  37037  knoppndvlem18  37041  knoppndvlem20  37043  tan2h  38185  mblfinlem3  38232  mblfinlem4  38233  itg2addnclem  38244  itg2gt0cn  38248  ftc1anclem7  38272  ftc1anc  38274  dvasin  38277  areacirclem1  38281  areacirclem4  38284  areacirc  38286  geomcau  38332  blbnd  38360  prdsbnd2  38368  rrnequiv  38408  relogbcld  42665  logblebd  42668  3lexlogpow5ineq2  42746  3lexlogpow2ineq1  42749  3lexlogpow2ineq2  42750  3lexlogpow5ineq5  42751  aks4d1p1p3  42760  aks4d1p1p2  42761  aks4d1p1p4  42762  aks4d1p1p6  42764  aks4d1p1p7  42765  aks4d1p1p5  42766  aks4d1p1  42767  aks6d1c7lem1  42871  explt1d  43008  expeq1d  43009  pell14qrrp  43513  pellfundex  43539  pellfundrp  43541  rmspecfund  43562  rmspecpos  43569  areaquad  43869  wwlemuld  44808  radcnvrat  44950  binomcxplemdvbinom  44989  binomcxplemnotnn0  44992  supxrgere  45975  supxrgelem  45979  xralrple2  45996  xralrple3  46015  sqrlearg  46195  sinaover2ne0  46508  ioodvbdlimc1lem1  46571  ioodvbdlimc1lem2  46572  ioodvbdlimc2lem  46574  dvnmul  46583  stoweidlem25  46665  stoweidlem28  46668  stoweidlem42  46682  stoweidlem49  46689  wallispilem3  46707  wallispilem4  46708  wallispi  46710  wallispi2lem1  46711  stirlinglem5  46718  stirlinglem10  46723  fourierdlem4  46751  fourierdlem6  46753  fourierdlem7  46754  fourierdlem19  46766  fourierdlem24  46771  fourierdlem26  46773  fourierdlem30  46777  fourierdlem42  46789  fourierdlem51  46797  fourierdlem63  46809  fourierdlem64  46810  fourierdlem65  46811  fourierdlem73  46819  fourierdlem75  46821  fourierdlem79  46825  fourierdlem92  46838  fourierdlem109  46855  fouriersw  46871  etransclem35  46909  qndenserrnbllem  46934  ioorrnopnlem  46944  hoiqssbllem1  47262  hoiqssbllem2  47263  iunhoiioolem  47315  pimrecltpos  47348  smfrec  47429  smfmullem1  47431  smfmullem2  47432  smfmullem3  47433  m1mod0mod1  48020  rege1logbrege0  49257  fldivexpfllog2  49264  fllog2  49267  resum2sqrp  49407  eenglngeehlnmlem2  49437  itschlc0xyqsol1  49465  inlinecirc02plem  49485  amgmwlem  50510