Theorem 2rp 12664

Description: 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Assertion

Ref	Expression
2rp	⊢ 2 ∈ ℝ+

Proof of Theorem 2rp

Step	Hyp	Ref	Expression
1		2re 11977	. 2 ⊢ 2 ∈ ℝ
2		2pos 12006	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12662	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2108  2c2 11958  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-2 11966  df-rp 12660

This theorem is referenced by:  rphalfcl  12686  2tnp1ge0ge0  13477  flhalf  13478  fldiv4lem1div2uz2  13484  discr  13883  2swrd2eqwrdeq  14594  sqrlem7  14888  abstri  14970  amgm2  15009  iseralt  15324  climcndslem2  15490  climcnds  15491  efcllem  15715  oexpneg  15982  mod2eq1n2dvds  15984  oddge22np1  15986  evennn02n  15987  nn0ehalf  16015  nno  16019  nn0oddm1d2  16022  flodddiv4t2lthalf  16053  bitsfzolem  16069  bitsfzo  16070  bitsmod  16071  bitsinv1  16077  sadasslem  16105  sadeq  16107  oddprm  16439  iserodd  16464  prmreclem6  16550  prmgaplem7  16686  2expltfac  16722  psgnunilem4  19020  efgsfo  19260  efgredlemd  19265  efgredlem  19268  chfacfscmul0  21915  chfacfpmmul0  21919  psmetge0  23373  xmetge0  23405  metnrmlem3  23930  pcoass  24093  aaliou3lem1  25407  aaliou3lem2  25408  aaliou3lem3  25409  aaliou3lem8  25410  aaliou3lem5  25412  aaliou3lem6  25413  aaliou3lem7  25414  aaliou3lem9  25415  cos02pilt1  25587  cosordlem  25591  2irrexpq  25790  loglesqrt  25816  sqrt2cxp2logb9e3  25854  log2cnv  25999  log2ub  26004  log2le1  26005  birthday  26009  cxp2limlem  26030  divsqrtsumlem  26034  emcllem7  26056  emre  26060  emgt0  26061  harmonicbnd3  26062  zetacvg  26069  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamucov  26092  cht2  26226  cht3  26227  chtub  26265  bclbnd  26333  bposlem6  26342  bposlem7  26343  bposlem8  26344  bposlem9  26345  gausslemma2dlem1a  26418  2lgslem3b  26450  2lgslem3c  26451  2lgslem3d  26452  2lgslem3a1  26453  2lgslem3d1  26456  chebbnd1lem2  26523  chebbnd1lem3  26524  chebbnd1  26525  chto1ub  26529  chpo1ubb  26534  rplogsumlem1  26537  selbergb  26602  selberg2b  26605  chpdifbndlem2  26607  pntrsumbnd2  26620  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntpbnd  26641  pntibndlem2  26644  pntibndlem3  26645  pntibnd  26646  pntlemr  26655  nvge0  28936  nmcexi  30289  cshw1s2  31134  sqsscirc1  31760  dya2ub  32137  dya2iocress  32141  dya2iocbrsiga  32142  dya2icobrsiga  32143  dya2icoseg  32144  sxbrsigalem2  32153  omssubadd  32167  fiblem  32265  fibp1  32268  coinflipprob  32346  signstfveq0  32456  hgt750lemd  32528  logdivsqrle  32530  hgt750lem  32531  logi  33606  unbdqndv2  34618  knoppndvlem12  34630  knoppndvlem14  34632  knoppndvlem17  34635  knoppndvlem18  34636  taupilem1  35419  taupilem2  35420  taupi  35421  poimirlem29  35733  itg2addnclem  35755  ftc1anclem7  35783  ftc1anc  35785  isbnd2  35868  lcmineqlem21  39985  lcmineqlem23  39987  3lexlogpow2ineq1  39994  dvrelog2b  40002  dvrelogpow2b  40004  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p6  40017  2np3bcnp1  40028  2ap1caineq  40029  fltne  40397  flt4lem7  40412  proot1ex  40942  sqrtcvallem2  41134  sqrtcvallem4  41136  sqrtcval  41138  oddfl  42705  sumnnodd  43061  wallispilem3  43498  wallispilem4  43499  wallispi  43501  wallispi2lem1  43502  stirlinglem2  43506  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem10  43514  stirlinglem11  43515  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  stirlingr  43521  dirker2re  43523  dirkerdenne0  43524  dirkerper  43527  dirkertrigeqlem1  43529  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem1  43534  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem10  43548  fourierdlem24  43562  fourierdlem62  43599  fourierdlem79  43616  fourierdlem87  43624  sqwvfoura  43659  sqwvfourb  43660  sge0ad2en  43859  ovnsubaddlem1  43998  hoiqssbllem1  44050  hoiqssbllem2  44051  hoiqssbllem3  44052  lighneallem3  44947  dfeven3  44998  dfodd4  44999  oexpnegALTV  45017  flnn0div2ge  45767  logbpw2m1  45801  fllog2  45802  blennnelnn  45810  nnpw2blen  45814  blen1b  45822  blennnt2  45823  nnolog2flm1  45824  blennngt2o2  45826  blennn0e2  45828  0dig2nn0e  45846  dignn0flhalflem1  45849  dignn0flhalflem2  45850