Theorem elrpd 13075

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5111  ℝcr 11116  0cc0 11117   < clt 11260  ℝ⁺crp 13034

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-rp 13035

This theorem is used by:  mul2lt0rgt0  13139  mul2lt0bi  13142  xov1plusxeqvd  13543  zltaddlt1le  13550  sqn0rp  14183  ltexp2a  14222  expcan  14225  ltexp2  14226  leexp2a  14228  expnlbnd2  14290  discr  14296  01sqrexlem4  15322  01sqrexlem7  15325  rpsqrtcl  15341  absrpcl  15365  mulcn2  15673  fprodle  16075  rprisefaccl  16102  rpefcl  16184  eflt  16197  ef01bndlem  16264  stdbdmopn  24728  methaus  24730  nmrpcl  24830  nlmvscnlem1  24896  metnrmlem1a  25069  icopnfcnv  25154  evth  25171  lebnumlem1  25173  nmoleub2lem3  25327  ipcnlem1  25457  minveclem4  25644  pjthlem1  25649  vitalilem4  25823  mbfmulc2lem  25859  itg2gt0  25972  dveflem  26191  dvferm1lem  26196  dvferm2  26199  aaliou3lem3  26560  psercnlem1  26641  pserdvlem1  26643  pserdv  26645  reeff1olem  26662  pilem2  26668  pilem3  26669  tanrpcl  26722  cosordlem  26748  rplogcl  26822  logdivlti  26838  logdivlt  26839  logdivle  26840  recxpcl  26893  rpcxpcl  26894  mulcxp  26903  cxple2  26915  cxpsqrt  26921  cxpcn3  26966  loglesqrt  26979  atanlogaddlem  27131  atantan  27141  atanbnd  27144  rlimcnp  27183  rlimcnp2  27184  efrlim  27187  cxp2limlem  27193  cxp2lim  27194  cxploglim2  27196  jensen  27206  harmonicubnd  27227  fsumharmonic  27229  lgamgulmlem2  27247  ftalem2  27291  basellem3  27300  basellem8  27305  chtrpcl  27392  fsumvma2  27431  chpval2  27435  chpchtsum  27436  chpub  27437  efexple  27498  chebbnd1lem2  27687  chebbnd1lem3  27688  chebbnd1  27689  chtppilimlem1  27690  chtppilimlem2  27691  chtppilim  27692  chebbnd2  27694  chto1lb  27695  chpchtlim  27696  chpo1ub  27697  rplogsumlem2  27702  dchrisumlema  27705  dchrisumlem3  27708  dchrvmasumlem2  27715  dchrvmasumiflem1  27718  dchrisum0lema  27731  chpdifbndlem1  27770  chpdifbndlem2  27771  chpdifbnd  27772  selberg3lem1  27774  pntrsumo1  27782  pntpbnd1a  27802  pntpbnd1  27803  pntpbnd2  27804  pntpbnd  27805  pntibndlem2  27808  pntibndlem3  27809  pntibnd  27810  pntlemd  27811  pntlem3  27826  pntleml  27828  pnt2  27830  pnt  27831  abvcxp  27832  ostth2lem1  27835  padicabv  27847  ostth2lem3  27852  ostth2lem4  27853  ostth2  27854  ostth3  27855  ttgcontlem1  29291  blocnilem  31229  minvecolem4  31305  minvecolem5  31306  pjhthlem1  31816  eigposi  32261  2sqr3minply  34236  xrge0iifhom  34393  cndprobprob  34895  hgt750lem  35105  unblimceq0lem  37154  unblimceq0  37155  knoppndvlem14  37173  knoppndvlem18  37177  knoppndvlem20  37179  tan2h  38322  mblfinlem3  38369  mblfinlem4  38370  itg2addnclem  38381  itg2gt0cn  38385  ftc1anclem7  38409  ftc1anc  38411  dvasin  38414  areacirclem1  38418  areacirclem4  38421  areacirc  38423  geomcau  38470  blbnd  38498  prdsbnd2  38506  rrnequiv  38546  relogbcld  42801  logblebd  42804  3lexlogpow5ineq2  42882  3lexlogpow2ineq1  42885  3lexlogpow2ineq2  42886  3lexlogpow5ineq5  42887  aks4d1p1p3  42896  aks4d1p1p2  42897  aks4d1p1p4  42898  aks4d1p1p6  42900  aks4d1p1p7  42901  aks4d1p1p5  42902  aks4d1p1  42903  aks6d1c7lem1  43007  explt1d  43144  expeq1d  43145  pell14qrrp  43647  pellfundex  43673  pellfundrp  43675  rmspecfund  43696  rmspecpos  43703  areaquad  44003  wwlemuld  44942  radcnvrat  45084  binomcxplemdvbinom  45123  binomcxplemnotnn0  45126  supxrgere  46109  supxrgelem  46113  xralrple2  46130  xralrple3  46149  sqrlearg  46329  sinaover2ne0  46642  ioodvbdlimc1lem1  46705  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  dvnmul  46717  stoweidlem25  46799  stoweidlem28  46802  stoweidlem42  46816  stoweidlem49  46823  wallispilem3  46841  wallispilem4  46842  wallispi  46844  wallispi2lem1  46845  stirlinglem5  46852  stirlinglem10  46857  fourierdlem4  46885  fourierdlem6  46887  fourierdlem7  46888  fourierdlem19  46900  fourierdlem24  46905  fourierdlem26  46907  fourierdlem30  46911  fourierdlem42  46923  fourierdlem51  46931  fourierdlem63  46943  fourierdlem64  46944  fourierdlem65  46945  fourierdlem73  46953  fourierdlem75  46955  fourierdlem79  46959  fourierdlem92  46972  fourierdlem109  46989  fouriersw  47005  etransclem35  47043  qndenserrnbllem  47068  ioorrnopnlem  47078  hoiqssbllem1  47396  hoiqssbllem2  47397  iunhoiioolem  47449  pimrecltpos  47482  smfrec  47563  smfmullem1  47565  smfmullem2  47566  smfmullem3  47567  m1mod0mod1  48157  rege1logbrege0  49397  fldivexpfllog2  49404  fllog2  49407  resum2sqrp  49547  eenglngeehlnmlem2  49577  itschlc0xyqsol1  49605  inlinecirc02plem  49625  amgmwlem  50709