MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2rp Structured version   Visualization version   Unicode version

Theorem 2rp 11336
Description: 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
Assertion
Ref Expression
2rp  |-  2  e.  RR+

Proof of Theorem 2rp
StepHypRef Expression
1 2re 10707 . 2  |-  2  e.  RR
2 2pos 10729 . 2  |-  0  <  2
31, 2elrpii 11334 1  |-  2  e.  RR+
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1898   2c2 10687   RR+crp 11331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-2 10696  df-rp 11332
This theorem is referenced by:  rphalfcl  11356  flhalf  12094  discr  12441  abstri  13442  bitsfzolem  14456  bitsfzolemOLD  14457  bitsfzo  14458  bitsmod  14459  bitsinv1  14465  sadasslem  14493  sadeq  14495  prmreclem6  14914  2expltfac  15112  psgnunilem4  17187  efgsfo  17438  efgredlemd  17443  efgredlem  17446  chfacfscmul0  19931  chfacfpmmul0  19935  psmetge0  21377  xmetge0  21408  metnrmlem3  21927  metnrmlem3OLD  21942  pcoass  22104  aaliou3lem1  23347  aaliou3lem2  23348  aaliou3lem3  23349  aaliou3lem8  23350  aaliou3lem5  23352  aaliou3lem6  23353  aaliou3lem7  23354  aaliou3lem9  23355  loglesqrt  23747  log2cnv  23919  log2ub  23924  log2le1  23925  birthday  23929  cxp2limlem  23950  divsqrtsumlem  23954  emcllem7  23976  emre  23980  emgt0  23981  harmonicbnd3  23982  zetacvg  23989  lgamgulmlem2  24004  lgamgulmlem3  24005  lgamucov  24012  cht2  24148  cht3  24149  chtub  24189  bclbnd  24257  bposlem6  24266  bposlem7  24267  bposlem8  24268  bposlem9  24269  chebbnd1lem2  24357  chebbnd1lem3  24358  chebbnd1  24359  chto1ub  24363  chpo1ubb  24368  rplogsumlem1  24371  selbergb  24436  selberg2b  24439  chpdifbndlem2  24441  pntrsumbnd2  24454  pntrlog2bndlem4  24467  pntrlog2bndlem5  24468  pntrlog2bndlem6  24470  pntrlog2bnd  24471  pntpbnd1a  24472  pntpbnd1  24473  pntpbnd2  24474  pntpbnd  24475  pntibndlem2  24478  pntibndlem3  24479  pntibnd  24480  pntlemr  24489  nmcexi  27728  sqsscirc1  28763  dya2ub  29141  dya2iocress  29145  dya2iocbrsiga  29146  dya2icobrsiga  29147  dya2icoseg  29148  sxbrsigalem2  29157  omssubadd  29177  omssubaddOLD  29181  fiblem  29280  fibp1  29283  coinflipprob  29361  signstfveq0  29515  logi  30419  taupilem1  31767  taupilem2  31768  taupi  31769  poimirlem29  32014  itg2addnclem  32038  ftc1anclem7  32068  ftc1anc  32070  isbnd2  32160  proot1ex  36123  oddfl  37525  sumnnodd  37748  wallispilem3  37967  wallispilem4  37968  wallispi  37970  wallispi2lem1  37971  stirlinglem2  37975  stirlinglem3  37976  stirlinglem4  37977  stirlinglem5  37978  stirlinglem6  37979  stirlinglem7  37980  stirlinglem10  37983  stirlinglem11  37984  stirlinglem13  37986  stirlinglem14  37987  stirlinglem15  37988  stirlingr  37990  dirker2re  37992  dirkerdenne0  37993  dirkerper  37996  dirkertrigeqlem1  37998  dirkertrigeqlem3  38000  dirkertrigeq  38001  dirkercncflem1  38003  dirkercncflem2  38004  dirkercncflem4  38006  fourierdlem10  38017  fourierdlem24  38031  fourierdlem62  38070  fourierdlem79  38087  fourierdlem87  38095  sqwvfoura  38130  sqwvfourb  38131  sge0ad2en  38311  ovnsubaddlem1  38430  hoiqssbllem1  38482  hoiqssbllem2  38483  hoiqssbllem3  38484  mod2eq1n2dvds  38763  elmod2OLD  38764  dfeven3  38825  dfodd4  38826  flnn0div2ge  40613  logbpw2m1  40651  fllog2  40652  blennnelnn  40660  nnpw2blen  40664  blen1b  40672  blennnt2  40673  nnolog2flm1  40674  blennngt2o2  40676  blennn0e2  40678  0dig2nn0e  40696  dignn0flhalflem1  40699  dignn0flhalflem2  40700
  Copyright terms: Public domain W3C validator