Theorem elrpd 13174

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5106  ℝcr 11212  0cc0 11213   < clt 11356  ℝ⁺crp 13133

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-rp 13134

This theorem is used by:  mul2lt0rgt0  13238  mul2lt0bi  13241  xov1plusxeqvd  13642  zltaddlt1le  13649  sqn0rp  14283  ltexp2a  14322  expcan  14325  ltexp2  14326  leexp2a  14328  expnlbnd2  14391  discr  14397  01sqrexlem4  15427  01sqrexlem7  15430  rpsqrtcl  15446  absrpcl  15470  mulcn2  15778  fprodle  16178  rprisefaccl  16205  rpefcl  16287  eflt  16300  ef01bndlem  16367  stdbdmopn  24852  methaus  24854  nmrpcl  24954  nlmvscnlem1  25020  metnrmlem1a  25193  icopnfcnv  25278  evth  25295  lebnumlem1  25297  nmoleub2lem3  25451  ipcnlem1  25581  minveclem4  25768  pjthlem1  25773  vitalilem4  25947  mbfmulc2lem  25983  itg2gt0  26096  dveflem  26314  dvferm1lem  26319  dvferm2  26322  aaliou3lem3  26686  psercnlem1  26767  pserdvlem1  26769  pserdv  26771  reeff1olem  26788  pilem2  26794  pilem3  26795  tanrpcl  26848  cosordlem  26873  rplogcl  26947  logdivlti  26963  logdivlt  26964  logdivle  26965  recxpcl  27018  rpcxpcl  27019  mulcxp  27028  cxple2  27040  cxpsqrt  27046  cxpcn3  27091  loglesqrt  27104  atanlogaddlem  27256  atantan  27266  atanbnd  27269  rlimcnp  27308  rlimcnp2  27309  efrlim  27312  cxp2limlem  27318  cxp2lim  27319  cxploglim2  27321  jensen  27331  harmonicubnd  27352  fsumharmonic  27354  lgamgulmlem2  27372  ftalem2  27416  basellem3  27425  basellem8  27430  chtrpcl  27517  fsumvma2  27556  chpval2  27560  chpchtsum  27561  chpub  27562  efexple  27623  chebbnd1lem2  27812  chebbnd1lem3  27813  chebbnd1  27814  chtppilimlem1  27815  chtppilimlem2  27816  chtppilim  27817  chebbnd2  27819  chto1lb  27820  chpchtlim  27821  chpo1ub  27822  rplogsumlem2  27827  dchrisumlema  27830  dchrisumlem3  27833  dchrvmasumlem2  27840  dchrvmasumiflem1  27843  dchrisum0lema  27856  chpdifbndlem1  27895  chpdifbndlem2  27896  chpdifbnd  27897  selberg3lem1  27899  pntrsumo1  27907  pntpbnd1a  27927  pntpbnd1  27928  pntpbnd2  27929  pntpbnd  27930  pntibndlem2  27933  pntibndlem3  27934  pntibnd  27935  pntlemd  27936  pntlem3  27951  pntleml  27953  pnt2  27955  pnt  27956  abvcxp  27957  ostth2lem1  27960  padicabv  27972  ostth2lem3  27977  ostth2lem4  27978  ostth2  27979  ostth3  27980  ttgcontlem1  29477  blocnilem  31421  minvecolem4  31497  minvecolem5  31498  pjhthlem1  32008  eigposi  32453  2sqr3minply  34468  xrge0iifhom  34625  cndprobprob  35126  hgt750lem  35336  unblimceq0lem  37502  unblimceq0  37503  knoppndvlem14  37521  knoppndvlem18  37525  knoppndvlem20  37527  tan2h  38678  mblfinlem3  38720  mblfinlem4  38721  itg2addnclem  38732  itg2gt0cn  38736  ftc1anclem7  38760  ftc1anc  38762  dvasin  38765  areacirclem1  38769  areacirclem4  38772  areacirc  38774  geomcau  38836  blbnd  38864  prdsbnd2  38872  rrnequiv  38912  relogbcld  43167  logblebd  43170  3lexlogpow5ineq2  43248  3lexlogpow2ineq1  43251  3lexlogpow2ineq2  43252  3lexlogpow5ineq5  43253  aks4d1p1p3  43262  aks4d1p1p2  43263  aks4d1p1p4  43264  aks4d1p1p6  43266  aks4d1p1p7  43267  aks4d1p1p5  43268  aks4d1p1  43269  aks6d1c7lem1  43373  explt1d  43523  expeq1d  43524  pell14qrrp  44010  pellfundex  44036  pellfundrp  44038  rmspecfund  44059  rmspecpos  44066  areaquad  44361  wwlemuld  45299  radcnvrat  45441  binomcxplemdvbinom  45480  binomcxplemnotnn0  45483  supxrgere  46487  supxrgelem  46491  xralrple2  46508  xralrple3  46527  sqrlearg  46707  sinaover2ne0  47020  ioodvbdlimc1lem1  47083  ioodvbdlimc1lem2  47084  ioodvbdlimc2lem  47086  dvnmul  47095  stoweidlem25  47177  stoweidlem28  47180  stoweidlem42  47194  stoweidlem49  47201  wallispilem3  47219  wallispilem4  47220  wallispi  47222  wallispi2lem1  47223  stirlinglem5  47230  stirlinglem10  47235  fourierdlem4  47263  fourierdlem6  47265  fourierdlem7  47266  fourierdlem19  47278  fourierdlem24  47283  fourierdlem26  47285  fourierdlem30  47289  fourierdlem42  47301  fourierdlem51  47309  fourierdlem63  47321  fourierdlem64  47322  fourierdlem65  47323  fourierdlem73  47331  fourierdlem75  47333  fourierdlem79  47337  fourierdlem92  47350  fourierdlem109  47367  fouriersw  47383  etransclem35  47421  qndenserrnbllem  47446  ioorrnopnlem  47456  hoiqssbllem1  47774  hoiqssbllem2  47775  iunhoiioolem  47827  pimrecltpos  47860  smfrec  47941  smfmullem1  47943  smfmullem2  47944  smfmullem3  47945  m1mod0mod1  48572  rege1logbrege0  49812  fldivexpfllog2  49819  fllog2  49822  resum2sqrp  49962  eenglngeehlnmlem2  49993  itschlc0xyqsol1  50020  inlinecirc02plem  50040  amgmwlem  51204