Theorem elrpd 13052

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  ℝcr 11094  0cc0 11095   < clt 11238  ℝ⁺crp 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-rp 13012

This theorem is referenced by:  mul2lt0rgt0  13116  mul2lt0bi  13119  xov1plusxeqvd  13520  zltaddlt1le  13527  sqn0rp  14159  ltexp2a  14198  expcan  14201  ltexp2  14202  leexp2a  14204  expnlbnd2  14266  discr  14272  01sqrexlem4  15292  01sqrexlem7  15295  rpsqrtcl  15311  absrpcl  15335  mulcn2  15643  fprodle  16046  rprisefaccl  16073  rpefcl  16155  eflt  16168  ef01bndlem  16235  stdbdmopn  24675  methaus  24677  nmrpcl  24777  nlmvscnlem1  24843  metnrmlem1a  25016  icopnfcnv  25101  evth  25118  lebnumlem1  25120  nmoleub2lem3  25274  ipcnlem1  25404  minveclem4  25591  pjthlem1  25596  vitalilem4  25770  mbfmulc2lem  25806  itg2gt0  25919  dveflem  26138  dvferm1lem  26143  dvferm2  26146  aaliou3lem3  26507  psercnlem1  26588  pserdvlem1  26590  pserdv  26592  reeff1olem  26609  pilem2  26615  pilem3  26616  tanrpcl  26669  cosordlem  26695  rplogcl  26769  logdivlti  26785  logdivlt  26786  logdivle  26787  recxpcl  26840  rpcxpcl  26841  mulcxp  26850  cxple2  26862  cxpsqrt  26868  cxpcn3  26913  loglesqrt  26926  atanlogaddlem  27078  atantan  27088  atanbnd  27091  rlimcnp  27130  rlimcnp2  27131  efrlim  27134  cxp2limlem  27140  cxp2lim  27141  cxploglim2  27143  jensen  27153  harmonicubnd  27174  fsumharmonic  27176  lgamgulmlem2  27194  ftalem2  27238  basellem3  27247  basellem8  27252  chtrpcl  27339  fsumvma2  27378  chpval2  27382  chpchtsum  27383  chpub  27384  efexple  27445  chebbnd1lem2  27634  chebbnd1lem3  27635  chebbnd1  27636  chtppilimlem1  27637  chtppilimlem2  27638  chtppilim  27639  chebbnd2  27641  chto1lb  27642  chpchtlim  27643  chpo1ub  27644  rplogsumlem2  27649  dchrisumlema  27652  dchrisumlem3  27655  dchrvmasumlem2  27662  dchrvmasumiflem1  27665  dchrisum0lema  27678  chpdifbndlem1  27717  chpdifbndlem2  27718  chpdifbnd  27719  selberg3lem1  27721  pntrsumo1  27729  pntpbnd1a  27749  pntpbnd1  27750  pntpbnd2  27751  pntpbnd  27752  pntibndlem2  27755  pntibndlem3  27756  pntibnd  27757  pntlemd  27758  pntlem3  27773  pntleml  27775  pnt2  27777  pnt  27778  abvcxp  27779  ostth2lem1  27782  padicabv  27794  ostth2lem3  27799  ostth2lem4  27800  ostth2  27801  ostth3  27802  ttgcontlem1  29234  blocnilem  31156  minvecolem4  31232  minvecolem5  31233  pjhthlem1  31743  eigposi  32188  2sqr3minply  34170  xrge0iifhom  34327  cndprobprob  34828  hgt750lem  35038  unblimceq0lem  37115  unblimceq0  37116  knoppndvlem14  37134  knoppndvlem18  37138  knoppndvlem20  37140  tan2h  38283  mblfinlem3  38330  mblfinlem4  38331  itg2addnclem  38342  itg2gt0cn  38346  ftc1anclem7  38370  ftc1anc  38372  dvasin  38375  areacirclem1  38379  areacirclem4  38382  areacirc  38384  geomcau  38430  blbnd  38458  prdsbnd2  38466  rrnequiv  38506  relogbcld  42761  logblebd  42764  3lexlogpow5ineq2  42842  3lexlogpow2ineq1  42845  3lexlogpow2ineq2  42846  3lexlogpow5ineq5  42847  aks4d1p1p3  42856  aks4d1p1p2  42857  aks4d1p1p4  42858  aks4d1p1p6  42860  aks4d1p1p7  42861  aks4d1p1p5  42862  aks4d1p1  42863  aks6d1c7lem1  42967  explt1d  43104  expeq1d  43105  pell14qrrp  43607  pellfundex  43633  pellfundrp  43635  rmspecfund  43656  rmspecpos  43663  areaquad  43963  wwlemuld  44902  radcnvrat  45044  binomcxplemdvbinom  45083  binomcxplemnotnn0  45086  supxrgere  46069  supxrgelem  46073  xralrple2  46090  xralrple3  46109  sqrlearg  46289  sinaover2ne0  46602  ioodvbdlimc1lem1  46665  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  dvnmul  46677  stoweidlem25  46759  stoweidlem28  46762  stoweidlem42  46776  stoweidlem49  46783  wallispilem3  46801  wallispilem4  46802  wallispi  46804  wallispi2lem1  46805  stirlinglem5  46812  stirlinglem10  46817  fourierdlem4  46845  fourierdlem6  46847  fourierdlem7  46848  fourierdlem19  46860  fourierdlem24  46865  fourierdlem26  46867  fourierdlem30  46871  fourierdlem42  46883  fourierdlem51  46891  fourierdlem63  46903  fourierdlem64  46904  fourierdlem65  46905  fourierdlem73  46913  fourierdlem75  46915  fourierdlem79  46919  fourierdlem92  46932  fourierdlem109  46949  fouriersw  46965  etransclem35  47003  qndenserrnbllem  47028  ioorrnopnlem  47038  hoiqssbllem1  47356  hoiqssbllem2  47357  iunhoiioolem  47409  pimrecltpos  47442  smfrec  47523  smfmullem1  47525  smfmullem2  47526  smfmullem3  47527  m1mod0mod1  48117  rege1logbrege0  49358  fldivexpfllog2  49365  fllog2  49368  resum2sqrp  49508  eenglngeehlnmlem2  49538  itschlc0xyqsol1  49566  inlinecirc02plem  49586  amgmwlem  50669