Theorem elrpd 13086

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ℝcr 11126  0cc0 11127   < clt 11270  ℝ⁺crp 13045

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-rp 13046

This theorem is used by:  mul2lt0rgt0  13150  mul2lt0bi  13153  xov1plusxeqvd  13554  zltaddlt1le  13561  sqn0rp  14194  ltexp2a  14233  expcan  14236  ltexp2  14237  leexp2a  14239  expnlbnd2  14301  discr  14307  01sqrexlem4  15335  01sqrexlem7  15338  rpsqrtcl  15354  absrpcl  15378  mulcn2  15686  fprodle  16086  rprisefaccl  16113  rpefcl  16195  eflt  16208  ef01bndlem  16275  stdbdmopn  24747  methaus  24749  nmrpcl  24849  nlmvscnlem1  24915  metnrmlem1a  25088  icopnfcnv  25173  evth  25190  lebnumlem1  25192  nmoleub2lem3  25346  ipcnlem1  25476  minveclem4  25663  pjthlem1  25668  vitalilem4  25842  mbfmulc2lem  25878  itg2gt0  25991  dveflem  26209  dvferm1lem  26214  dvferm2  26217  aaliou3lem3  26583  psercnlem1  26664  pserdvlem1  26666  pserdv  26668  reeff1olem  26685  pilem2  26691  pilem3  26692  tanrpcl  26745  cosordlem  26770  rplogcl  26844  logdivlti  26860  logdivlt  26861  logdivle  26862  recxpcl  26915  rpcxpcl  26916  mulcxp  26925  cxple2  26937  cxpsqrt  26943  cxpcn3  26988  loglesqrt  27001  atanlogaddlem  27153  atantan  27163  atanbnd  27166  rlimcnp  27205  rlimcnp2  27206  efrlim  27209  cxp2limlem  27215  cxp2lim  27216  cxploglim2  27218  jensen  27228  harmonicubnd  27249  fsumharmonic  27251  lgamgulmlem2  27269  ftalem2  27313  basellem3  27322  basellem8  27327  chtrpcl  27414  fsumvma2  27453  chpval2  27457  chpchtsum  27458  chpub  27459  efexple  27520  chebbnd1lem2  27709  chebbnd1lem3  27710  chebbnd1  27711  chtppilimlem1  27712  chtppilimlem2  27713  chtppilim  27714  chebbnd2  27716  chto1lb  27717  chpchtlim  27718  chpo1ub  27719  rplogsumlem2  27724  dchrisumlema  27727  dchrisumlem3  27730  dchrvmasumlem2  27737  dchrvmasumiflem1  27740  dchrisum0lema  27753  chpdifbndlem1  27792  chpdifbndlem2  27793  chpdifbnd  27794  selberg3lem1  27796  pntrsumo1  27804  pntpbnd1a  27824  pntpbnd1  27825  pntpbnd2  27826  pntpbnd  27827  pntibndlem2  27830  pntibndlem3  27831  pntibnd  27832  pntlemd  27833  pntlem3  27848  pntleml  27850  pnt2  27852  pnt  27853  abvcxp  27854  ostth2lem1  27857  padicabv  27869  ostth2lem3  27874  ostth2lem4  27875  ostth2  27876  ostth3  27877  ttgcontlem1  29344  blocnilem  31288  minvecolem4  31364  minvecolem5  31365  pjhthlem1  31875  eigposi  32320  2sqr3minply  34293  xrge0iifhom  34450  cndprobprob  34952  hgt750lem  35162  unblimceq0lem  37206  unblimceq0  37207  knoppndvlem14  37225  knoppndvlem18  37229  knoppndvlem20  37231  tan2h  38369  mblfinlem3  38411  mblfinlem4  38412  itg2addnclem  38423  itg2gt0cn  38427  ftc1anclem7  38451  ftc1anc  38453  dvasin  38456  areacirclem1  38460  areacirclem4  38463  areacirc  38465  geomcau  38512  blbnd  38540  prdsbnd2  38548  rrnequiv  38588  relogbcld  42843  logblebd  42846  3lexlogpow5ineq2  42924  3lexlogpow2ineq1  42927  3lexlogpow2ineq2  42928  3lexlogpow5ineq5  42929  aks4d1p1p3  42938  aks4d1p1p2  42939  aks4d1p1p4  42940  aks4d1p1p6  42942  aks4d1p1p7  42943  aks4d1p1p5  42944  aks4d1p1  42945  aks6d1c7lem1  43049  explt1d  43201  expeq1d  43202  pell14qrrp  43704  pellfundex  43730  pellfundrp  43732  rmspecfund  43753  rmspecpos  43760  areaquad  44060  wwlemuld  44999  radcnvrat  45141  binomcxplemdvbinom  45180  binomcxplemnotnn0  45183  supxrgere  46166  supxrgelem  46170  xralrple2  46187  xralrple3  46206  sqrlearg  46386  sinaover2ne0  46699  ioodvbdlimc1lem1  46762  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  dvnmul  46774  stoweidlem25  46856  stoweidlem28  46859  stoweidlem42  46873  stoweidlem49  46880  wallispilem3  46898  wallispilem4  46899  wallispi  46901  wallispi2lem1  46902  stirlinglem5  46909  stirlinglem10  46914  fourierdlem4  46942  fourierdlem6  46944  fourierdlem7  46945  fourierdlem19  46957  fourierdlem24  46962  fourierdlem26  46964  fourierdlem30  46968  fourierdlem42  46980  fourierdlem51  46988  fourierdlem63  47000  fourierdlem64  47001  fourierdlem65  47002  fourierdlem73  47010  fourierdlem75  47012  fourierdlem79  47016  fourierdlem92  47029  fourierdlem109  47046  fouriersw  47062  etransclem35  47100  qndenserrnbllem  47125  ioorrnopnlem  47135  hoiqssbllem1  47453  hoiqssbllem2  47454  iunhoiioolem  47506  pimrecltpos  47539  smfrec  47620  smfmullem1  47622  smfmullem2  47623  smfmullem3  47624  m1mod0mod1  48251  rege1logbrege0  49491  fldivexpfllog2  49498  fllog2  49501  resum2sqrp  49641  eenglngeehlnmlem2  49671  itschlc0xyqsol1  49699  inlinecirc02plem  49719  amgmwlem  50823