Theorem elrpd 13039

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

Syntax hints:   → wi 4   ∈ wcel 2099   class class class wbr 5142  ℝcr 11131  0cc0 11132   < clt 11272  ℝ⁺crp 13000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-rp 13001

This theorem is referenced by:  mul2lt0rgt0  13103  mul2lt0bi  13106  xov1plusxeqvd  13501  zltaddlt1le  13508  sqn0rp  14117  ltexp2a  14156  expcan  14159  ltexp2  14160  leexp2a  14162  expnlbnd2  14222  discr  14228  01sqrexlem4  15218  01sqrexlem7  15221  rpsqrtcl  15237  absrpcl  15261  mulcn2  15566  fprodle  15966  rprisefaccl  15993  rpefcl  16074  eflt  16087  ef01bndlem  16154  stdbdmopn  24420  methaus  24422  nmrpcl  24522  nlmvscnlem1  24596  metnrmlem1a  24767  icopnfcnv  24860  evth  24878  lebnumlem1  24880  nmoleub2lem3  25035  ipcnlem1  25166  minveclem4  25353  pjthlem1  25358  vitalilem4  25533  mbfmulc2lem  25569  itg2gt0  25683  dveflem  25904  dvferm1lem  25909  dvferm2  25912  aaliou3lem3  26272  psercnlem1  26355  pserdvlem1  26357  pserdv  26359  reeff1olem  26376  pilem2  26382  pilem3  26383  tanrpcl  26432  cosordlem  26457  rplogcl  26531  logdivlti  26547  logdivlt  26548  logdivle  26549  recxpcl  26602  rpcxpcl  26603  mulcxp  26612  cxple2  26624  cxpsqrt  26630  cxpcn3  26676  loglesqrt  26686  atanlogaddlem  26838  atantan  26848  atanbnd  26851  rlimcnp  26890  rlimcnp2  26891  efrlim  26894  efrlimOLD  26895  cxp2limlem  26901  cxp2lim  26902  cxploglim2  26904  jensen  26914  harmonicubnd  26935  fsumharmonic  26937  lgamgulmlem2  26955  ftalem2  26999  basellem3  27008  basellem8  27013  chtrpcl  27100  fsumvma2  27140  chpval2  27144  chpchtsum  27145  chpub  27146  efexple  27207  chebbnd1lem2  27396  chebbnd1lem3  27397  chebbnd1  27398  chtppilimlem1  27399  chtppilimlem2  27400  chtppilim  27401  chebbnd2  27403  chto1lb  27404  chpchtlim  27405  chpo1ub  27406  rplogsumlem2  27411  dchrisumlema  27414  dchrisumlem3  27417  dchrvmasumlem2  27424  dchrvmasumiflem1  27427  dchrisum0lema  27440  chpdifbndlem1  27479  chpdifbndlem2  27480  chpdifbnd  27481  selberg3lem1  27483  pntrsumo1  27491  pntpbnd1a  27511  pntpbnd1  27512  pntpbnd2  27513  pntpbnd  27514  pntibndlem2  27517  pntibndlem3  27518  pntibnd  27519  pntlemd  27520  pntlem3  27535  pntleml  27537  pnt2  27539  pnt  27540  abvcxp  27541  ostth2lem1  27544  padicabv  27556  ostth2lem3  27561  ostth2lem4  27562  ostth2  27563  ostth3  27564  ttgcontlem1  28688  blocnilem  30607  minvecolem4  30683  minvecolem5  30684  pjhthlem1  31194  eigposi  31639  xrge0iifhom  33532  cndprobprob  34052  hgt750lem  34277  unblimceq0lem  35975  unblimceq0  35976  knoppndvlem14  35994  knoppndvlem18  35998  knoppndvlem20  36000  tan2h  37079  mblfinlem3  37126  mblfinlem4  37127  itg2addnclem  37138  itg2gt0cn  37142  ftc1anclem7  37166  ftc1anc  37168  dvasin  37171  areacirclem1  37175  areacirclem4  37178  areacirc  37180  geomcau  37226  blbnd  37254  prdsbnd2  37262  rrnequiv  37302  relogbcld  41437  logblebd  41440  3lexlogpow5ineq2  41520  3lexlogpow2ineq1  41523  3lexlogpow2ineq2  41524  3lexlogpow5ineq5  41525  aks4d1p1p3  41534  aks4d1p1p2  41535  aks4d1p1p4  41536  aks4d1p1p6  41538  aks4d1p1p7  41539  aks4d1p1p5  41540  aks4d1p1  41541  aks6d1c7lem1  41646  metakunt29  41679  pell14qrrp  42274  pellfundex  42300  pellfundrp  42302  rmspecfund  42323  rmspecpos  42331  areaquad  42638  wwlemuld  43580  radcnvrat  43745  binomcxplemdvbinom  43784  binomcxplemnotnn0  43787  supxrgere  44709  supxrgelem  44713  xralrple2  44730  xralrple3  44750  sqrlearg  44932  sinaover2ne0  45250  ioodvbdlimc1lem1  45313  ioodvbdlimc1lem2  45314  ioodvbdlimc2lem  45316  dvnmul  45325  stoweidlem25  45407  stoweidlem28  45410  stoweidlem42  45424  stoweidlem49  45431  wallispilem3  45449  wallispilem4  45450  wallispi  45452  wallispi2lem1  45453  stirlinglem5  45460  stirlinglem10  45465  fourierdlem4  45493  fourierdlem6  45495  fourierdlem7  45496  fourierdlem19  45508  fourierdlem24  45513  fourierdlem26  45515  fourierdlem30  45519  fourierdlem42  45531  fourierdlem51  45539  fourierdlem63  45551  fourierdlem64  45552  fourierdlem65  45553  fourierdlem73  45561  fourierdlem75  45563  fourierdlem79  45567  fourierdlem92  45580  fourierdlem109  45597  fouriersw  45613  etransclem35  45651  qndenserrnbllem  45676  ioorrnopnlem  45686  hoiqssbllem1  46004  hoiqssbllem2  46005  iunhoiioolem  46057  pimrecltpos  46090  smfrec  46171  smfmullem1  46173  smfmullem2  46174  smfmullem3  46175  m1mod0mod1  46703  rege1logbrege0  47625  fldivexpfllog2  47632  fllog2  47635  resum2sqrp  47775  eenglngeehlnmlem2  47805  itschlc0xyqsol1  47833  inlinecirc02plem  47853  amgmwlem  48229