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

Theorem 2rp 11672
Description: 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
Assertion
Ref Expression
2rp 2 ∈ ℝ+

Proof of Theorem 2rp
StepHypRef Expression
1 2re 10940 . 2 2 ∈ ℝ
2 2pos 10962 . 2 0 < 2
31, 2elrpii 11670 1 2 ∈ ℝ+
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  2c2 10920  +crp 11667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-2 10929  df-rp 11668
This theorem is referenced by:  rphalfcl  11693  flhalf  12451  fldiv4lem1div2uz2  12457  discr  12821  abstri  13867  mod2eq1n2dvds  14858  bitsfzolem  14943  bitsfzo  14944  bitsmod  14945  bitsinv1  14951  sadasslem  14979  sadeq  14981  prmreclem6  15412  2expltfac  15586  psgnunilem4  17689  efgsfo  17924  efgredlemd  17929  efgredlem  17932  chfacfscmul0  20430  chfacfpmmul0  20434  psmetge0  21875  xmetge0  21907  metnrmlem3  22420  pcoass  22580  aaliou3lem1  23846  aaliou3lem2  23847  aaliou3lem3  23848  aaliou3lem8  23849  aaliou3lem5  23851  aaliou3lem6  23852  aaliou3lem7  23853  aaliou3lem9  23854  loglesqrt  24244  log2cnv  24416  log2ub  24421  log2le1  24422  birthday  24426  cxp2limlem  24447  divsqrtsumlem  24451  emcllem7  24473  emre  24477  emgt0  24478  harmonicbnd3  24479  zetacvg  24486  lgamgulmlem2  24501  lgamgulmlem3  24502  lgamucov  24509  cht2  24643  cht3  24644  chtub  24682  bclbnd  24750  bposlem6  24759  bposlem7  24760  bposlem8  24761  bposlem9  24762  gausslemma2dlem1a  24835  2lgslem3b  24867  2lgslem3c  24868  2lgslem3d  24869  2lgslem3a1  24870  2lgslem3d1  24873  chebbnd1lem2  24904  chebbnd1lem3  24905  chebbnd1  24906  chto1ub  24910  chpo1ubb  24915  rplogsumlem1  24918  selbergb  24983  selberg2b  24986  chpdifbndlem2  24988  pntrsumbnd2  25001  pntrlog2bndlem4  25014  pntrlog2bndlem5  25015  pntrlog2bndlem6  25017  pntrlog2bnd  25018  pntpbnd1a  25019  pntpbnd1  25020  pntpbnd2  25021  pntpbnd  25022  pntibndlem2  25025  pntibndlem3  25026  pntibnd  25027  pntlemr  25036  nmcexi  28103  sqsscirc1  29116  dya2ub  29493  dya2iocress  29497  dya2iocbrsiga  29498  dya2icobrsiga  29499  dya2icoseg  29500  sxbrsigalem2  29509  omssubadd  29523  fiblem  29621  fibp1  29624  coinflipprob  29702  signstfveq0  29814  logi  30707  unbdqndv2  31506  knoppndvlem12  31518  knoppndvlem14  31520  knoppndvlem17  31523  knoppndvlem18  31524  taupilem1  32168  taupilem2  32169  taupi  32170  poimirlem29  32432  itg2addnclem  32455  ftc1anclem7  32485  ftc1anc  32487  isbnd2  32576  proot1ex  36622  oddfl  38254  sumnnodd  38521  wallispilem3  38784  wallispilem4  38785  wallispi  38787  wallispi2lem1  38788  stirlinglem2  38792  stirlinglem3  38793  stirlinglem4  38794  stirlinglem5  38795  stirlinglem6  38796  stirlinglem7  38797  stirlinglem10  38800  stirlinglem11  38801  stirlinglem13  38803  stirlinglem14  38804  stirlinglem15  38805  stirlingr  38807  dirker2re  38809  dirkerdenne0  38810  dirkerper  38813  dirkertrigeqlem1  38815  dirkertrigeqlem3  38817  dirkertrigeq  38818  dirkercncflem1  38820  dirkercncflem2  38821  dirkercncflem4  38823  fourierdlem10  38834  fourierdlem24  38848  fourierdlem62  38885  fourierdlem79  38902  fourierdlem87  38910  sqwvfoura  38945  sqwvfourb  38946  sge0ad2en  39148  ovnsubaddlem1  39284  hoiqssbllem1  39336  hoiqssbllem2  39337  hoiqssbllem3  39338  lighneallem3  39887  dfeven3  39933  dfodd4  39934  flnn0div2ge  42143  logbpw2m1  42181  fllog2  42182  blennnelnn  42190  nnpw2blen  42194  blen1b  42202  blennnt2  42203  nnolog2flm1  42204  blennngt2o2  42206  blennn0e2  42208  0dig2nn0e  42226  dignn0flhalflem1  42229  dignn0flhalflem2  42230
  Copyright terms: Public domain W3C validator