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

Theorem elrpd 12418
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 12381 . 2 (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
41, 2, 3sylanbrc 583 1 (𝜑𝐴 ∈ ℝ+)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105   class class class wbr 5058  cr 10525  0cc0 10526   < clt 10664  +crp 12379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-rp 12380
This theorem is referenced by:  mul2lt0rgt0  12482  mul2lt0bi  12485  xov1plusxeqvd  12874  zltaddlt1le  12880  sqn0rp  13482  ltexp2a  13520  expcan  13523  ltexp2  13524  leexp2a  13526  expnlbnd2  13585  discr  13591  sqrlem4  14595  sqrlem7  14598  rpsqrtcl  14614  absrpcl  14638  mulcn2  14942  fprodle  15340  rprisefaccl  15367  rpefcl  15447  eflt  15460  ef01bndlem  15527  stdbdmopn  23057  methaus  23059  nmrpcl  23158  nlmvscnlem1  23224  metnrmlem1a  23395  icopnfcnv  23475  evth  23492  lebnumlem1  23494  nmoleub2lem3  23648  ipcnlem1  23777  minveclem4  23964  pjthlem1  23969  vitalilem4  24141  mbfmulc2lem  24177  itg2gt0  24290  dveflem  24505  dvferm1lem  24510  dvferm2  24513  aaliou3lem3  24862  psercnlem1  24942  pserdvlem1  24944  pserdv  24946  reeff1olem  24963  pilem2  24969  pilem3  24970  tanrpcl  25019  cosordlem  25042  rplogcl  25114  logdivlti  25130  logdivlt  25131  logdivle  25132  recxpcl  25185  rpcxpcl  25186  mulcxp  25195  cxple2  25207  cxpsqrt  25213  cxpcn3  25256  loglesqrt  25266  atanlogaddlem  25418  atantan  25428  atanbnd  25431  rlimcnp  25471  rlimcnp2  25472  efrlim  25475  cxp2limlem  25481  cxp2lim  25482  cxploglim2  25484  jensen  25494  harmonicubnd  25515  fsumharmonic  25517  lgamgulmlem2  25535  ftalem2  25579  basellem3  25588  basellem8  25593  chtrpcl  25680  fsumvma2  25718  chpval2  25722  chpchtsum  25723  chpub  25724  efexple  25785  chebbnd1lem2  25974  chebbnd1lem3  25975  chebbnd1  25976  chtppilimlem1  25977  chtppilimlem2  25978  chtppilim  25979  chebbnd2  25981  chto1lb  25982  chpchtlim  25983  chpo1ub  25984  rplogsumlem2  25989  dchrisumlema  25992  dchrisumlem3  25995  dchrvmasumlem2  26002  dchrvmasumiflem1  26005  dchrisum0lema  26018  chpdifbndlem1  26057  chpdifbndlem2  26058  chpdifbnd  26059  selberg3lem1  26061  pntrsumo1  26069  pntpbnd1a  26089  pntpbnd1  26090  pntpbnd2  26091  pntpbnd  26092  pntibndlem2  26095  pntibndlem3  26096  pntibnd  26097  pntlemd  26098  pntlem3  26113  pntleml  26115  pnt2  26117  pnt  26118  abvcxp  26119  ostth2lem1  26122  padicabv  26134  ostth2lem3  26139  ostth2lem4  26140  ostth2  26141  ostth3  26142  ttgcontlem1  26599  blocnilem  28509  minvecolem4  28585  minvecolem5  28586  pjhthlem1  29096  eigposi  29541  xrge0iifhom  31080  cndprobprob  31596  hgt750lem  31822  unblimceq0lem  33743  unblimceq0  33744  knoppndvlem14  33762  knoppndvlem18  33766  knoppndvlem20  33768  tan2h  34766  mblfinlem3  34813  mblfinlem4  34814  itg2addnclem  34825  itg2gt0cn  34829  ftc1anclem7  34855  ftc1anc  34857  dvasin  34860  areacirclem1  34864  areacirclem4  34867  areacirc  34869  geomcau  34917  blbnd  34948  prdsbnd2  34956  rrnequiv  34996  pell14qrrp  39337  pellfundex  39363  pellfundrp  39365  rmspecfund  39386  rmspecpos  39393  areaquad  39703  wwlemuld  40386  radcnvrat  40526  binomcxplemdvbinom  40565  binomcxplemnotnn0  40568  supxrgere  41481  supxrgelem  41485  xralrple2  41502  xralrple3  41522  sqrlearg  41709  sinaover2ne0  42029  ioodvbdlimc1lem1  42096  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnmul  42108  stoweidlem25  42191  stoweidlem28  42194  stoweidlem42  42208  stoweidlem49  42215  wallispilem3  42233  wallispilem4  42234  wallispi  42236  wallispi2lem1  42237  stirlinglem5  42244  stirlinglem10  42249  fourierdlem4  42277  fourierdlem6  42279  fourierdlem7  42280  fourierdlem19  42292  fourierdlem24  42297  fourierdlem26  42299  fourierdlem30  42303  fourierdlem42  42315  fourierdlem51  42323  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem73  42345  fourierdlem75  42347  fourierdlem79  42351  fourierdlem92  42364  fourierdlem109  42381  fouriersw  42397  etransclem35  42435  qndenserrnbllem  42460  ioorrnopnlem  42470  hoiqssbllem1  42785  hoiqssbllem2  42786  iunhoiioolem  42838  pimrecltpos  42868  smfrec  42945  smfmullem1  42947  smfmullem2  42948  smfmullem3  42949  m1mod0mod1  43410  rege1logbrege0  44516  fldivexpfllog2  44523  fllog2  44526  resum2sqrp  44593  eenglngeehlnmlem2  44623  itschlc0xyqsol1  44651  inlinecirc02plem  44671  amgmwlem  44801
  Copyright terms: Public domain W3C validator