Theorem elrpd 12431

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5068  ℝcr 10538  0cc0 10539   < clt 10677  ℝ⁺crp 12392

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-rp 12393

This theorem is referenced by:  mul2lt0rgt0  12495  mul2lt0bi  12498  xov1plusxeqvd  12887  zltaddlt1le  12893  sqn0rp  13495  ltexp2a  13533  expcan  13536  ltexp2  13537  leexp2a  13539  expnlbnd2  13598  discr  13604  sqrlem4  14607  sqrlem7  14610  rpsqrtcl  14626  absrpcl  14650  mulcn2  14954  fprodle  15352  rprisefaccl  15379  rpefcl  15459  eflt  15472  ef01bndlem  15539  stdbdmopn  23130  methaus  23132  nmrpcl  23231  nlmvscnlem1  23297  metnrmlem1a  23468  icopnfcnv  23548  evth  23565  lebnumlem1  23567  nmoleub2lem3  23721  ipcnlem1  23850  minveclem4  24037  pjthlem1  24042  vitalilem4  24214  mbfmulc2lem  24250  itg2gt0  24363  dveflem  24578  dvferm1lem  24583  dvferm2  24586  aaliou3lem3  24935  psercnlem1  25015  pserdvlem1  25017  pserdv  25019  reeff1olem  25036  pilem2  25042  pilem3  25043  tanrpcl  25092  cosordlem  25117  rplogcl  25189  logdivlti  25205  logdivlt  25206  logdivle  25207  recxpcl  25260  rpcxpcl  25261  mulcxp  25270  cxple2  25282  cxpsqrt  25288  cxpcn3  25331  loglesqrt  25341  atanlogaddlem  25493  atantan  25503  atanbnd  25506  rlimcnp  25545  rlimcnp2  25546  efrlim  25549  cxp2limlem  25555  cxp2lim  25556  cxploglim2  25558  jensen  25568  harmonicubnd  25589  fsumharmonic  25591  lgamgulmlem2  25609  ftalem2  25653  basellem3  25662  basellem8  25667  chtrpcl  25754  fsumvma2  25792  chpval2  25796  chpchtsum  25797  chpub  25798  efexple  25859  chebbnd1lem2  26048  chebbnd1lem3  26049  chebbnd1  26050  chtppilimlem1  26051  chtppilimlem2  26052  chtppilim  26053  chebbnd2  26055  chto1lb  26056  chpchtlim  26057  chpo1ub  26058  rplogsumlem2  26063  dchrisumlema  26066  dchrisumlem3  26069  dchrvmasumlem2  26076  dchrvmasumiflem1  26079  dchrisum0lema  26092  chpdifbndlem1  26131  chpdifbndlem2  26132  chpdifbnd  26133  selberg3lem1  26135  pntrsumo1  26143  pntpbnd1a  26163  pntpbnd1  26164  pntpbnd2  26165  pntpbnd  26166  pntibndlem2  26169  pntibndlem3  26170  pntibnd  26171  pntlemd  26172  pntlem3  26187  pntleml  26189  pnt2  26191  pnt  26192  abvcxp  26193  ostth2lem1  26196  padicabv  26208  ostth2lem3  26213  ostth2lem4  26214  ostth2  26215  ostth3  26216  ttgcontlem1  26673  blocnilem  28583  minvecolem4  28659  minvecolem5  28660  pjhthlem1  29170  eigposi  29615  xrge0iifhom  31182  cndprobprob  31698  hgt750lem  31924  unblimceq0lem  33847  unblimceq0  33848  knoppndvlem14  33866  knoppndvlem18  33870  knoppndvlem20  33872  tan2h  34886  mblfinlem3  34933  mblfinlem4  34934  itg2addnclem  34945  itg2gt0cn  34949  ftc1anclem7  34975  ftc1anc  34977  dvasin  34980  areacirclem1  34984  areacirclem4  34987  areacirc  34989  geomcau  35036  blbnd  35067  prdsbnd2  35075  rrnequiv  35115  pell14qrrp  39464  pellfundex  39490  pellfundrp  39492  rmspecfund  39513  rmspecpos  39520  areaquad  39830  wwlemuld  40513  radcnvrat  40653  binomcxplemdvbinom  40692  binomcxplemnotnn0  40695  supxrgere  41608  supxrgelem  41612  xralrple2  41629  xralrple3  41649  sqrlearg  41836  sinaover2ne0  42156  ioodvbdlimc1lem1  42223  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  dvnmul  42235  stoweidlem25  42317  stoweidlem28  42320  stoweidlem42  42334  stoweidlem49  42341  wallispilem3  42359  wallispilem4  42360  wallispi  42362  wallispi2lem1  42363  stirlinglem5  42370  stirlinglem10  42375  fourierdlem4  42403  fourierdlem6  42405  fourierdlem7  42406  fourierdlem19  42418  fourierdlem24  42423  fourierdlem26  42425  fourierdlem30  42429  fourierdlem42  42441  fourierdlem51  42449  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  fourierdlem73  42471  fourierdlem75  42473  fourierdlem79  42477  fourierdlem92  42490  fourierdlem109  42507  fouriersw  42523  etransclem35  42561  qndenserrnbllem  42586  ioorrnopnlem  42596  hoiqssbllem1  42911  hoiqssbllem2  42912  iunhoiioolem  42964  pimrecltpos  42994  smfrec  43071  smfmullem1  43073  smfmullem2  43074  smfmullem3  43075  m1mod0mod1  43536  rege1logbrege0  44625  fldivexpfllog2  44632  fllog2  44635  resum2sqrp  44702  eenglngeehlnmlem2  44732  itschlc0xyqsol1  44760  inlinecirc02plem  44780  amgmwlem  44910