Theorem elrpd 12429

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536  0cc0 10537   < clt 10675  ℝ⁺crp 12390

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-rp 12391

This theorem is referenced by:  mul2lt0rgt0  12493  mul2lt0bi  12496  xov1plusxeqvd  12885  zltaddlt1le  12891  sqn0rp  13493  ltexp2a  13531  expcan  13534  ltexp2  13535  leexp2a  13537  expnlbnd2  13596  discr  13602  sqrlem4  14605  sqrlem7  14608  rpsqrtcl  14624  absrpcl  14648  mulcn2  14952  fprodle  15350  rprisefaccl  15377  rpefcl  15457  eflt  15470  ef01bndlem  15537  stdbdmopn  23128  methaus  23130  nmrpcl  23229  nlmvscnlem1  23295  metnrmlem1a  23466  icopnfcnv  23546  evth  23563  lebnumlem1  23565  nmoleub2lem3  23719  ipcnlem1  23848  minveclem4  24035  pjthlem1  24040  vitalilem4  24212  mbfmulc2lem  24248  itg2gt0  24361  dveflem  24576  dvferm1lem  24581  dvferm2  24584  aaliou3lem3  24933  psercnlem1  25013  pserdvlem1  25015  pserdv  25017  reeff1olem  25034  pilem2  25040  pilem3  25041  tanrpcl  25090  cosordlem  25115  rplogcl  25187  logdivlti  25203  logdivlt  25204  logdivle  25205  recxpcl  25258  rpcxpcl  25259  mulcxp  25268  cxple2  25280  cxpsqrt  25286  cxpcn3  25329  loglesqrt  25339  atanlogaddlem  25491  atantan  25501  atanbnd  25504  rlimcnp  25543  rlimcnp2  25544  efrlim  25547  cxp2limlem  25553  cxp2lim  25554  cxploglim2  25556  jensen  25566  harmonicubnd  25587  fsumharmonic  25589  lgamgulmlem2  25607  ftalem2  25651  basellem3  25660  basellem8  25665  chtrpcl  25752  fsumvma2  25790  chpval2  25794  chpchtsum  25795  chpub  25796  efexple  25857  chebbnd1lem2  26046  chebbnd1lem3  26047  chebbnd1  26048  chtppilimlem1  26049  chtppilimlem2  26050  chtppilim  26051  chebbnd2  26053  chto1lb  26054  chpchtlim  26055  chpo1ub  26056  rplogsumlem2  26061  dchrisumlema  26064  dchrisumlem3  26067  dchrvmasumlem2  26074  dchrvmasumiflem1  26077  dchrisum0lema  26090  chpdifbndlem1  26129  chpdifbndlem2  26130  chpdifbnd  26131  selberg3lem1  26133  pntrsumo1  26141  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntpbnd  26164  pntibndlem2  26167  pntibndlem3  26168  pntibnd  26169  pntlemd  26170  pntlem3  26185  pntleml  26187  pnt2  26189  pnt  26190  abvcxp  26191  ostth2lem1  26194  padicabv  26206  ostth2lem3  26211  ostth2lem4  26212  ostth2  26213  ostth3  26214  ttgcontlem1  26671  blocnilem  28581  minvecolem4  28657  minvecolem5  28658  pjhthlem1  29168  eigposi  29613  xrge0iifhom  31180  cndprobprob  31696  hgt750lem  31922  unblimceq0lem  33845  unblimceq0  33846  knoppndvlem14  33864  knoppndvlem18  33868  knoppndvlem20  33870  tan2h  34899  mblfinlem3  34946  mblfinlem4  34947  itg2addnclem  34958  itg2gt0cn  34962  ftc1anclem7  34988  ftc1anc  34990  dvasin  34993  areacirclem1  34997  areacirclem4  35000  areacirc  35002  geomcau  35049  blbnd  35080  prdsbnd2  35088  rrnequiv  35128  pell14qrrp  39477  pellfundex  39503  pellfundrp  39505  rmspecfund  39526  rmspecpos  39533  areaquad  39843  wwlemuld  40526  radcnvrat  40666  binomcxplemdvbinom  40705  binomcxplemnotnn0  40708  supxrgere  41621  supxrgelem  41625  xralrple2  41642  xralrple3  41662  sqrlearg  41849  sinaover2ne0  42169  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvnmul  42248  stoweidlem25  42330  stoweidlem28  42333  stoweidlem42  42347  stoweidlem49  42354  wallispilem3  42372  wallispilem4  42373  wallispi  42375  wallispi2lem1  42376  stirlinglem5  42383  stirlinglem10  42388  fourierdlem4  42416  fourierdlem6  42418  fourierdlem7  42419  fourierdlem19  42431  fourierdlem24  42436  fourierdlem26  42438  fourierdlem30  42442  fourierdlem42  42454  fourierdlem51  42462  fourierdlem63  42474  fourierdlem64  42475  fourierdlem65  42476  fourierdlem73  42484  fourierdlem75  42486  fourierdlem79  42490  fourierdlem92  42503  fourierdlem109  42520  fouriersw  42536  etransclem35  42574  qndenserrnbllem  42599  ioorrnopnlem  42609  hoiqssbllem1  42924  hoiqssbllem2  42925  iunhoiioolem  42977  pimrecltpos  43007  smfrec  43084  smfmullem1  43086  smfmullem2  43087  smfmullem3  43088  m1mod0mod1  43549  rege1logbrege0  44638  fldivexpfllog2  44645  fllog2  44648  resum2sqrp  44715  eenglngeehlnmlem2  44745  itschlc0xyqsol1  44773  inlinecirc02plem  44793  amgmwlem  44923