Theorem elrpd 12944

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023  0cc0 11024   < clt 11164  ℝ⁺crp 12903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-rp 12904

This theorem is referenced by:  mul2lt0rgt0  13008  mul2lt0bi  13011  xov1plusxeqvd  13412  zltaddlt1le  13419  sqn0rp  14048  ltexp2a  14087  expcan  14090  ltexp2  14091  leexp2a  14093  expnlbnd2  14155  discr  14161  01sqrexlem4  15166  01sqrexlem7  15169  rpsqrtcl  15185  absrpcl  15209  mulcn2  15517  fprodle  15917  rprisefaccl  15944  rpefcl  16027  eflt  16040  ef01bndlem  16107  stdbdmopn  24460  methaus  24462  nmrpcl  24562  nlmvscnlem1  24628  metnrmlem1a  24801  icopnfcnv  24894  evth  24912  lebnumlem1  24914  nmoleub2lem3  25069  ipcnlem1  25199  minveclem4  25386  pjthlem1  25391  vitalilem4  25566  mbfmulc2lem  25602  itg2gt0  25715  dveflem  25937  dvferm1lem  25942  dvferm2  25945  aaliou3lem3  26306  psercnlem1  26389  pserdvlem1  26391  pserdv  26393  reeff1olem  26410  pilem2  26416  pilem3  26417  tanrpcl  26467  cosordlem  26493  rplogcl  26567  logdivlti  26583  logdivlt  26584  logdivle  26585  recxpcl  26638  rpcxpcl  26639  mulcxp  26648  cxple2  26660  cxpsqrt  26666  cxpcn3  26712  loglesqrt  26725  atanlogaddlem  26877  atantan  26887  atanbnd  26890  rlimcnp  26929  rlimcnp2  26930  efrlim  26933  efrlimOLD  26934  cxp2limlem  26940  cxp2lim  26941  cxploglim2  26943  jensen  26953  harmonicubnd  26974  fsumharmonic  26976  lgamgulmlem2  26994  ftalem2  27038  basellem3  27047  basellem8  27052  chtrpcl  27139  fsumvma2  27179  chpval2  27183  chpchtsum  27184  chpub  27185  efexple  27246  chebbnd1lem2  27435  chebbnd1lem3  27436  chebbnd1  27437  chtppilimlem1  27438  chtppilimlem2  27439  chtppilim  27440  chebbnd2  27442  chto1lb  27443  chpchtlim  27444  chpo1ub  27445  rplogsumlem2  27450  dchrisumlema  27453  dchrisumlem3  27456  dchrvmasumlem2  27463  dchrvmasumiflem1  27466  dchrisum0lema  27479  chpdifbndlem1  27518  chpdifbndlem2  27519  chpdifbnd  27520  selberg3lem1  27522  pntrsumo1  27530  pntpbnd1a  27550  pntpbnd1  27551  pntpbnd2  27552  pntpbnd  27553  pntibndlem2  27556  pntibndlem3  27557  pntibnd  27558  pntlemd  27559  pntlem3  27574  pntleml  27576  pnt2  27578  pnt  27579  abvcxp  27580  ostth2lem1  27583  padicabv  27595  ostth2lem3  27600  ostth2lem4  27601  ostth2  27602  ostth3  27603  ttgcontlem1  28906  blocnilem  30828  minvecolem4  30904  minvecolem5  30905  pjhthlem1  31415  eigposi  31860  2sqr3minply  33886  xrge0iifhom  34043  cndprobprob  34544  hgt750lem  34757  unblimceq0lem  36649  unblimceq0  36650  knoppndvlem14  36668  knoppndvlem18  36672  knoppndvlem20  36674  tan2h  37752  mblfinlem3  37799  mblfinlem4  37800  itg2addnclem  37811  itg2gt0cn  37815  ftc1anclem7  37839  ftc1anc  37841  dvasin  37844  areacirclem1  37848  areacirclem4  37851  areacirc  37853  geomcau  37899  blbnd  37927  prdsbnd2  37935  rrnequiv  37975  relogbcld  42166  logblebd  42169  3lexlogpow5ineq2  42248  3lexlogpow2ineq1  42251  3lexlogpow2ineq2  42252  3lexlogpow5ineq5  42253  aks4d1p1p3  42262  aks4d1p1p2  42263  aks4d1p1p4  42264  aks4d1p1p6  42266  aks4d1p1p7  42267  aks4d1p1p5  42268  aks4d1p1  42269  aks6d1c7lem1  42373  explt1d  42520  expeq1d  42521  pell14qrrp  43044  pellfundex  43070  pellfundrp  43072  rmspecfund  43093  rmspecpos  43100  areaquad  43400  wwlemuld  44339  radcnvrat  44497  binomcxplemdvbinom  44536  binomcxplemnotnn0  44539  supxrgere  45520  supxrgelem  45524  xralrple2  45541  xralrple3  45560  sqrlearg  45741  sinaover2ne0  46054  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnmul  46129  stoweidlem25  46211  stoweidlem28  46214  stoweidlem42  46228  stoweidlem49  46235  wallispilem3  46253  wallispilem4  46254  wallispi  46256  wallispi2lem1  46257  stirlinglem5  46264  stirlinglem10  46269  fourierdlem4  46297  fourierdlem6  46299  fourierdlem7  46300  fourierdlem19  46312  fourierdlem24  46317  fourierdlem26  46319  fourierdlem30  46323  fourierdlem42  46335  fourierdlem51  46343  fourierdlem63  46355  fourierdlem64  46356  fourierdlem65  46357  fourierdlem73  46365  fourierdlem75  46367  fourierdlem79  46371  fourierdlem92  46384  fourierdlem109  46401  fouriersw  46417  etransclem35  46455  qndenserrnbllem  46480  ioorrnopnlem  46490  hoiqssbllem1  46808  hoiqssbllem2  46809  iunhoiioolem  46861  pimrecltpos  46894  smfrec  46975  smfmullem1  46977  smfmullem2  46978  smfmullem3  46979  m1mod0mod1  47542  rege1logbrege0  48746  fldivexpfllog2  48753  fllog2  48756  resum2sqrp  48896  eenglngeehlnmlem2  48926  itschlc0xyqsol1  48954  inlinecirc02plem  48974  amgmwlem  49989