Theorem elrpd 12977

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝcr 11031  0cc0 11032   < clt 11173  ℝ⁺crp 12936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-rp 12937

This theorem is referenced by:  mul2lt0rgt0  13041  mul2lt0bi  13044  xov1plusxeqvd  13445  zltaddlt1le  13452  sqn0rp  14083  ltexp2a  14122  expcan  14125  ltexp2  14126  leexp2a  14128  expnlbnd2  14190  discr  14196  01sqrexlem4  15201  01sqrexlem7  15204  rpsqrtcl  15220  absrpcl  15244  mulcn2  15552  fprodle  15955  rprisefaccl  15982  rpefcl  16065  eflt  16078  ef01bndlem  16145  stdbdmopn  24496  methaus  24498  nmrpcl  24598  nlmvscnlem1  24664  metnrmlem1a  24837  icopnfcnv  24922  evth  24939  lebnumlem1  24941  nmoleub2lem3  25095  ipcnlem1  25225  minveclem4  25412  pjthlem1  25417  vitalilem4  25591  mbfmulc2lem  25627  itg2gt0  25740  dveflem  25959  dvferm1lem  25964  dvferm2  25967  aaliou3lem3  26324  psercnlem1  26406  pserdvlem1  26408  pserdv  26410  reeff1olem  26427  pilem2  26433  pilem3  26434  tanrpcl  26484  cosordlem  26510  rplogcl  26584  logdivlti  26600  logdivlt  26601  logdivle  26602  recxpcl  26655  rpcxpcl  26656  mulcxp  26665  cxple2  26677  cxpsqrt  26683  cxpcn3  26728  loglesqrt  26741  atanlogaddlem  26893  atantan  26903  atanbnd  26906  rlimcnp  26945  rlimcnp2  26946  efrlim  26949  efrlimOLD  26950  cxp2limlem  26956  cxp2lim  26957  cxploglim2  26959  jensen  26969  harmonicubnd  26990  fsumharmonic  26992  lgamgulmlem2  27010  ftalem2  27054  basellem3  27063  basellem8  27068  chtrpcl  27155  fsumvma2  27194  chpval2  27198  chpchtsum  27199  chpub  27200  efexple  27261  chebbnd1lem2  27450  chebbnd1lem3  27451  chebbnd1  27452  chtppilimlem1  27453  chtppilimlem2  27454  chtppilim  27455  chebbnd2  27457  chto1lb  27458  chpchtlim  27459  chpo1ub  27460  rplogsumlem2  27465  dchrisumlema  27468  dchrisumlem3  27471  dchrvmasumlem2  27478  dchrvmasumiflem1  27481  dchrisum0lema  27494  chpdifbndlem1  27533  chpdifbndlem2  27534  chpdifbnd  27535  selberg3lem1  27537  pntrsumo1  27545  pntpbnd1a  27565  pntpbnd1  27566  pntpbnd2  27567  pntpbnd  27568  pntibndlem2  27571  pntibndlem3  27572  pntibnd  27573  pntlemd  27574  pntlem3  27589  pntleml  27591  pnt2  27593  pnt  27594  abvcxp  27595  ostth2lem1  27598  padicabv  27610  ostth2lem3  27615  ostth2lem4  27616  ostth2  27617  ostth3  27618  ttgcontlem1  28970  blocnilem  30893  minvecolem4  30969  minvecolem5  30970  pjhthlem1  31480  eigposi  31925  2sqr3minply  33943  xrge0iifhom  34100  cndprobprob  34601  hgt750lem  34814  unblimceq0lem  36785  unblimceq0  36786  knoppndvlem14  36804  knoppndvlem18  36808  knoppndvlem20  36810  tan2h  37950  mblfinlem3  37997  mblfinlem4  37998  itg2addnclem  38009  itg2gt0cn  38013  ftc1anclem7  38037  ftc1anc  38039  dvasin  38042  areacirclem1  38046  areacirclem4  38049  areacirc  38051  geomcau  38097  blbnd  38125  prdsbnd2  38133  rrnequiv  38173  relogbcld  42430  logblebd  42433  3lexlogpow5ineq2  42511  3lexlogpow2ineq1  42514  3lexlogpow2ineq2  42515  3lexlogpow5ineq5  42516  aks4d1p1p3  42525  aks4d1p1p2  42526  aks4d1p1p4  42527  aks4d1p1p6  42529  aks4d1p1p7  42530  aks4d1p1p5  42531  aks4d1p1  42532  aks6d1c7lem1  42636  explt1d  42772  expeq1d  42773  pell14qrrp  43309  pellfundex  43335  pellfundrp  43337  rmspecfund  43358  rmspecpos  43365  areaquad  43665  wwlemuld  44604  radcnvrat  44762  binomcxplemdvbinom  44801  binomcxplemnotnn0  44804  supxrgere  45784  supxrgelem  45788  xralrple2  45805  xralrple3  45824  sqrlearg  46004  sinaover2ne0  46317  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnmul  46392  stoweidlem25  46474  stoweidlem28  46477  stoweidlem42  46491  stoweidlem49  46498  wallispilem3  46516  wallispilem4  46517  wallispi  46519  wallispi2lem1  46520  stirlinglem5  46527  stirlinglem10  46532  fourierdlem4  46560  fourierdlem6  46562  fourierdlem7  46563  fourierdlem19  46575  fourierdlem24  46580  fourierdlem26  46582  fourierdlem30  46586  fourierdlem42  46598  fourierdlem51  46606  fourierdlem63  46618  fourierdlem64  46619  fourierdlem65  46620  fourierdlem73  46628  fourierdlem75  46630  fourierdlem79  46634  fourierdlem92  46647  fourierdlem109  46664  fouriersw  46680  etransclem35  46718  qndenserrnbllem  46743  ioorrnopnlem  46753  hoiqssbllem1  47071  hoiqssbllem2  47072  iunhoiioolem  47124  pimrecltpos  47157  smfrec  47238  smfmullem1  47240  smfmullem2  47241  smfmullem3  47242  m1mod0mod1  47823  rege1logbrege0  49049  fldivexpfllog2  49056  fllog2  49059  resum2sqrp  49199  eenglngeehlnmlem2  49229  itschlc0xyqsol1  49257  inlinecirc02plem  49277  amgmwlem  50292