Theorem elrpd 12992

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067  0cc0 11068   < clt 11208  ℝ⁺crp 12951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-rp 12952

This theorem is referenced by:  mul2lt0rgt0  13056  mul2lt0bi  13059  xov1plusxeqvd  13459  zltaddlt1le  13466  sqn0rp  14092  ltexp2a  14131  expcan  14134  ltexp2  14135  leexp2a  14137  expnlbnd2  14199  discr  14205  01sqrexlem4  15211  01sqrexlem7  15214  rpsqrtcl  15230  absrpcl  15254  mulcn2  15562  fprodle  15962  rprisefaccl  15989  rpefcl  16072  eflt  16085  ef01bndlem  16152  stdbdmopn  24406  methaus  24408  nmrpcl  24508  nlmvscnlem1  24574  metnrmlem1a  24747  icopnfcnv  24840  evth  24858  lebnumlem1  24860  nmoleub2lem3  25015  ipcnlem1  25145  minveclem4  25332  pjthlem1  25337  vitalilem4  25512  mbfmulc2lem  25548  itg2gt0  25661  dveflem  25883  dvferm1lem  25888  dvferm2  25891  aaliou3lem3  26252  psercnlem1  26335  pserdvlem1  26337  pserdv  26339  reeff1olem  26356  pilem2  26362  pilem3  26363  tanrpcl  26413  cosordlem  26439  rplogcl  26513  logdivlti  26529  logdivlt  26530  logdivle  26531  recxpcl  26584  rpcxpcl  26585  mulcxp  26594  cxple2  26606  cxpsqrt  26612  cxpcn3  26658  loglesqrt  26671  atanlogaddlem  26823  atantan  26833  atanbnd  26836  rlimcnp  26875  rlimcnp2  26876  efrlim  26879  efrlimOLD  26880  cxp2limlem  26886  cxp2lim  26887  cxploglim2  26889  jensen  26899  harmonicubnd  26920  fsumharmonic  26922  lgamgulmlem2  26940  ftalem2  26984  basellem3  26993  basellem8  26998  chtrpcl  27085  fsumvma2  27125  chpval2  27129  chpchtsum  27130  chpub  27131  efexple  27192  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem1  27384  chtppilimlem2  27385  chtppilim  27386  chebbnd2  27388  chto1lb  27389  chpchtlim  27390  chpo1ub  27391  rplogsumlem2  27396  dchrisumlema  27399  dchrisumlem3  27402  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  dchrisum0lema  27425  chpdifbndlem1  27464  chpdifbndlem2  27465  chpdifbnd  27466  selberg3lem1  27468  pntrsumo1  27476  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntpbnd  27499  pntibndlem2  27502  pntibndlem3  27503  pntibnd  27504  pntlemd  27505  pntlem3  27520  pntleml  27522  pnt2  27524  pnt  27525  abvcxp  27526  ostth2lem1  27529  padicabv  27541  ostth2lem3  27546  ostth2lem4  27547  ostth2  27548  ostth3  27549  ttgcontlem1  28812  blocnilem  30733  minvecolem4  30809  minvecolem5  30810  pjhthlem1  31320  eigposi  31765  2sqr3minply  33770  xrge0iifhom  33927  cndprobprob  34429  hgt750lem  34642  unblimceq0lem  36494  unblimceq0  36495  knoppndvlem14  36513  knoppndvlem18  36517  knoppndvlem20  36519  tan2h  37606  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem  37665  itg2gt0cn  37669  ftc1anclem7  37693  ftc1anc  37695  dvasin  37698  areacirclem1  37702  areacirclem4  37705  areacirc  37707  geomcau  37753  blbnd  37781  prdsbnd2  37789  rrnequiv  37829  relogbcld  41961  logblebd  41964  3lexlogpow5ineq2  42043  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks6d1c7lem1  42168  explt1d  42311  expeq1d  42312  pell14qrrp  42848  pellfundex  42874  pellfundrp  42876  rmspecfund  42897  rmspecpos  42905  areaquad  43205  wwlemuld  44145  radcnvrat  44303  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  supxrgere  45329  supxrgelem  45333  xralrple2  45350  xralrple3  45370  sqrlearg  45551  sinaover2ne0  45866  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmul  45941  stoweidlem25  46023  stoweidlem28  46026  stoweidlem42  46040  stoweidlem49  46047  wallispilem3  46065  wallispilem4  46066  wallispi  46068  wallispi2lem1  46069  stirlinglem5  46076  stirlinglem10  46081  fourierdlem4  46109  fourierdlem6  46111  fourierdlem7  46112  fourierdlem19  46124  fourierdlem24  46129  fourierdlem26  46131  fourierdlem30  46135  fourierdlem42  46147  fourierdlem51  46155  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem73  46177  fourierdlem75  46179  fourierdlem79  46183  fourierdlem92  46196  fourierdlem109  46213  fouriersw  46229  etransclem35  46267  qndenserrnbllem  46292  ioorrnopnlem  46302  hoiqssbllem1  46620  hoiqssbllem2  46621  iunhoiioolem  46673  pimrecltpos  46706  smfrec  46787  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  m1mod0mod1  47355  rege1logbrege0  48547  fldivexpfllog2  48554  fllog2  48557  resum2sqrp  48697  eenglngeehlnmlem2  48727  itschlc0xyqsol1  48755  inlinecirc02plem  48775  amgmwlem  49791