MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrpd Structured version   Visualization version   GIF version

Theorem elrpd 11907
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
StepHypRef Expression
1 elrpd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 elrpd.2 . 2 (𝜑 → 0 < 𝐴)
3 elrp 11872 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3sylanbrc 699 1 (𝜑𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030   class class class wbr 4685  cr 9973  0cc0 9974   < clt 10112  +crp 11870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-rp 11871
This theorem is referenced by:  mul2lt0rgt0  11971  mul2lt0bi  11974  xov1plusxeqvd  12356  zltaddlt1le  12362  ltexp2a  12952  expcan  12953  ltexp2  12954  leexp2a  12956  expnlbnd2  13035  discr  13041  sqrlem4  14030  sqrlem7  14033  rpsqrtcl  14049  absrpcl  14072  rlimrege0  14354  mulcn2  14370  fprodle  14771  rprisefaccl  14798  rpefcl  14878  eflt  14891  ef01bndlem  14958  stdbdmopn  22370  methaus  22372  nmrpcl  22471  nlmvscnlem1  22537  metnrmlem1a  22708  icopnfcnv  22788  evth  22805  lebnumlem1  22807  nmoleub2lem3  22961  ipcnlem1  23090  minveclem4  23249  vitalilem4  23425  mbfmulc2lem  23459  itg2gt0  23572  dveflem  23787  dvferm1lem  23792  dvferm2  23795  aaliou3lem3  24144  psercnlem1  24224  pserdvlem1  24226  pserdv  24228  reeff1olem  24245  pilem2  24251  pilem3  24252  tanrpcl  24301  cosordlem  24322  rplogcl  24395  logdivlti  24411  logdivlt  24412  logdivle  24413  dvloglem  24439  recxpcl  24466  rpcxpcl  24467  mulcxp  24476  cxple2  24488  cxpsqrt  24494  cxpcn3  24534  loglesqrt  24544  atanlogaddlem  24685  atantan  24695  atanbnd  24698  rlimcnp  24737  rlimcnp2  24738  efrlim  24741  cxp2limlem  24747  cxp2lim  24748  cxploglim2  24750  jensen  24760  harmonicubnd  24781  fsumharmonic  24783  lgamgulmlem2  24801  ftalem2  24845  basellem3  24854  basellem8  24859  chtrpcl  24946  fsumvma2  24984  chpval2  24988  chpchtsum  24989  chpub  24990  efexple  25051  chebbnd1lem2  25204  chebbnd1lem3  25205  chebbnd1  25206  chtppilimlem1  25207  chtppilimlem2  25208  chtppilim  25209  chebbnd2  25211  chto1lb  25212  chpchtlim  25213  chpo1ub  25214  rplogsumlem2  25219  dchrisumlema  25222  dchrisumlem3  25225  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  dchrisum0lema  25248  chpdifbndlem1  25287  chpdifbndlem2  25288  chpdifbnd  25289  selberg3lem1  25291  pntrsumo1  25299  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntpbnd  25322  pntibndlem2  25325  pntibndlem3  25326  pntibnd  25327  pntlemd  25328  pntlem3  25343  pntleml  25345  pnt2  25347  pnt  25348  abvcxp  25349  ostth2lem1  25352  padicabv  25364  ostth2lem3  25369  ostth2lem4  25370  ostth2  25371  ostth3  25372  ttgcontlem1  25810  blocnilem  27787  minvecolem4  27864  minvecolem5  27865  xrge0iifhom  30111  cndprobprob  30628  hgt750lem  30857  unblimceq0lem  32622  unblimceq0  32623  knoppndvlem14  32641  knoppndvlem18  32645  knoppndvlem20  32647  tan2h  33531  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem  33591  itg2gt0cn  33595  ftc1anclem7  33621  ftc1anc  33623  dvasin  33626  areacirclem1  33630  areacirclem4  33633  areacirc  33635  geomcau  33685  blbnd  33716  prdsbnd2  33724  rrnequiv  33764  pell14qrrp  37741  pellfundex  37767  pellfundrp  37769  rmspecfund  37791  rmspecpos  37798  areaquad  38119  wwlemuld  38771  radcnvrat  38830  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  supxrgere  39862  supxrgelem  39866  xralrple2  39883  xralrple3  39903  sqrlearg  40098  sinaover2ne0  40397  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnmul  40476  stoweidlem25  40560  stoweidlem28  40563  stoweidlem42  40577  stoweidlem49  40584  wallispilem3  40602  wallispilem4  40603  wallispi  40605  wallispi2lem1  40606  stirlinglem5  40613  stirlinglem10  40618  fourierdlem4  40646  fourierdlem6  40648  fourierdlem7  40649  fourierdlem19  40661  fourierdlem24  40666  fourierdlem26  40668  fourierdlem30  40672  fourierdlem42  40684  fourierdlem51  40692  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem73  40714  fourierdlem75  40716  fourierdlem79  40720  fourierdlem92  40733  fourierdlem109  40750  fouriersw  40766  etransclem35  40804  qndenserrnbllem  40832  ioorrnopnlem  40842  hoiqssbllem1  41157  hoiqssbllem2  41158  iunhoiioolem  41210  pimrecltpos  41240  smfrec  41317  smfmullem1  41319  smfmullem2  41320  smfmullem3  41321  m1mod0mod1  41664  rege1logbrege0  42677  fldivexpfllog2  42684  fllog2  42687  amgmwlem  42876
  Copyright terms: Public domain W3C validator