Theorem elrpd 12983

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037  0cc0 11038   < clt 11179  ℝ⁺crp 12942

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-rp 12943

This theorem is referenced by:  mul2lt0rgt0  13047  mul2lt0bi  13050  xov1plusxeqvd  13451  zltaddlt1le  13458  sqn0rp  14089  ltexp2a  14128  expcan  14131  ltexp2  14132  leexp2a  14134  expnlbnd2  14196  discr  14202  01sqrexlem4  15207  01sqrexlem7  15210  rpsqrtcl  15226  absrpcl  15250  mulcn2  15558  fprodle  15961  rprisefaccl  15988  rpefcl  16071  eflt  16084  ef01bndlem  16151  stdbdmopn  24483  methaus  24485  nmrpcl  24585  nlmvscnlem1  24651  metnrmlem1a  24824  icopnfcnv  24909  evth  24926  lebnumlem1  24928  nmoleub2lem3  25082  ipcnlem1  25212  minveclem4  25399  pjthlem1  25404  vitalilem4  25578  mbfmulc2lem  25614  itg2gt0  25727  dveflem  25946  dvferm1lem  25951  dvferm2  25954  aaliou3lem3  26310  psercnlem1  26390  pserdvlem1  26392  pserdv  26394  reeff1olem  26411  pilem2  26417  pilem3  26418  tanrpcl  26468  cosordlem  26494  rplogcl  26568  logdivlti  26584  logdivlt  26585  logdivle  26586  recxpcl  26639  rpcxpcl  26640  mulcxp  26649  cxple2  26661  cxpsqrt  26667  cxpcn3  26712  loglesqrt  26725  atanlogaddlem  26877  atantan  26887  atanbnd  26890  rlimcnp  26929  rlimcnp2  26930  efrlim  26933  cxp2limlem  26939  cxp2lim  26940  cxploglim2  26942  jensen  26952  harmonicubnd  26973  fsumharmonic  26975  lgamgulmlem2  26993  ftalem2  27037  basellem3  27046  basellem8  27051  chtrpcl  27138  fsumvma2  27177  chpval2  27181  chpchtsum  27182  chpub  27183  efexple  27244  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  chtppilimlem2  27437  chtppilim  27438  chebbnd2  27440  chto1lb  27441  chpchtlim  27442  chpo1ub  27443  rplogsumlem2  27448  dchrisumlema  27451  dchrisumlem3  27454  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0lema  27477  chpdifbndlem1  27516  chpdifbndlem2  27517  chpdifbnd  27518  selberg3lem1  27520  pntrsumo1  27528  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntpbnd  27551  pntibndlem2  27554  pntibndlem3  27555  pntibnd  27556  pntlemd  27557  pntlem3  27572  pntleml  27574  pnt2  27576  pnt  27577  abvcxp  27578  ostth2lem1  27581  padicabv  27593  ostth2lem3  27598  ostth2lem4  27599  ostth2  27600  ostth3  27601  ttgcontlem1  28953  blocnilem  30875  minvecolem4  30951  minvecolem5  30952  pjhthlem1  31462  eigposi  31907  2sqr3minply  33924  xrge0iifhom  34081  cndprobprob  34582  hgt750lem  34795  unblimceq0lem  36766  unblimceq0  36767  knoppndvlem14  36785  knoppndvlem18  36789  knoppndvlem20  36791  tan2h  37933  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem  37992  itg2gt0cn  37996  ftc1anclem7  38020  ftc1anc  38022  dvasin  38025  areacirclem1  38029  areacirclem4  38032  areacirc  38034  geomcau  38080  blbnd  38108  prdsbnd2  38116  rrnequiv  38156  relogbcld  42413  logblebd  42416  3lexlogpow5ineq2  42494  3lexlogpow2ineq1  42497  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks6d1c7lem1  42619  explt1d  42755  expeq1d  42756  pell14qrrp  43288  pellfundex  43314  pellfundrp  43316  rmspecfund  43337  rmspecpos  43344  areaquad  43644  wwlemuld  44583  radcnvrat  44741  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  supxrgere  45763  supxrgelem  45767  xralrple2  45784  xralrple3  45803  sqrlearg  45983  sinaover2ne0  46296  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmul  46371  stoweidlem25  46453  stoweidlem28  46456  stoweidlem42  46470  stoweidlem49  46477  wallispilem3  46495  wallispilem4  46496  wallispi  46498  wallispi2lem1  46499  stirlinglem5  46506  stirlinglem10  46511  fourierdlem4  46539  fourierdlem6  46541  fourierdlem7  46542  fourierdlem19  46554  fourierdlem24  46559  fourierdlem26  46561  fourierdlem30  46565  fourierdlem42  46577  fourierdlem51  46585  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem73  46607  fourierdlem75  46609  fourierdlem79  46613  fourierdlem92  46626  fourierdlem109  46643  fouriersw  46659  etransclem35  46697  qndenserrnbllem  46722  ioorrnopnlem  46732  hoiqssbllem1  47050  hoiqssbllem2  47051  iunhoiioolem  47103  pimrecltpos  47136  smfrec  47217  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  m1mod0mod1  47808  rege1logbrege0  49034  fldivexpfllog2  49041  fllog2  49044  resum2sqrp  49184  eenglngeehlnmlem2  49214  itschlc0xyqsol1  49242  inlinecirc02plem  49262  amgmwlem  50277