Theorem 2rp 12962

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 12261	. 2 ⊢ 2 ∈ ℝ
2		2pos 12290	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12960	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2109  2c2 12242  ℝ⁺crp 12957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150  ax-pre-mulgt0 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-riota 7346  df-ov 7392  df-oprab 7393  df-mpo 7394  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11216  df-mnf 11217  df-xr 11218  df-ltxr 11219  df-le 11220  df-sub 11413  df-neg 11414  df-2 12250  df-rp 12958

This theorem is referenced by:  rphalfcl  12986  ge2halflem1  13074  2tnp1ge0ge0  13797  flhalf  13798  fldiv4lem1div2uz2  13804  discr  14211  2swrd2eqwrdeq  14925  01sqrexlem7  15220  abstri  15303  amgm2  15342  iseralt  15657  climcndslem2  15822  climcnds  15823  efcllem  16049  oexpneg  16321  mod2eq1n2dvds  16323  oddge22np1  16325  evennn02n  16326  nn0ehalf  16354  nno  16358  nn0oddm1d2  16361  flodddiv4t2lthalf  16394  bitsfzolem  16410  bitsfzo  16411  bitsmod  16412  bitsinv1  16418  sadasslem  16446  sadeq  16448  oddprm  16787  iserodd  16812  prmreclem6  16898  prmgaplem7  17034  2expltfac  17069  psgnunilem4  19433  efgsfo  19675  efgredlemd  19680  efgredlem  19683  chfacfscmul0  22751  chfacfpmmul0  22755  psmetge0  24206  xmetge0  24238  metnrmlem3  24756  pcoass  24930  aaliou3lem1  26256  aaliou3lem2  26257  aaliou3lem3  26258  aaliou3lem8  26259  aaliou3lem5  26261  aaliou3lem6  26262  aaliou3lem7  26263  aaliou3lem9  26264  cos02pilt1  26441  cosordlem  26445  logi  26502  2irrexpq  26646  loglesqrt  26677  sqrt2cxp2logb9e3  26715  log2cnv  26860  log2ub  26865  log2le1  26866  birthday  26870  cxp2limlem  26892  divsqrtsumlem  26896  emcllem7  26918  emre  26922  emgt0  26923  harmonicbnd3  26924  zetacvg  26931  lgamgulmlem2  26946  lgamgulmlem3  26947  lgamucov  26954  cht2  27088  cht3  27089  chtub  27129  bclbnd  27197  bposlem6  27206  bposlem7  27207  bposlem8  27208  bposlem9  27209  gausslemma2dlem1a  27282  2lgslem3b  27314  2lgslem3c  27315  2lgslem3d  27316  2lgslem3a1  27317  2lgslem3d1  27320  chebbnd1lem2  27387  chebbnd1lem3  27388  chebbnd1  27389  chto1ub  27393  chpo1ubb  27398  rplogsumlem1  27401  selbergb  27466  selberg2b  27469  chpdifbndlem2  27471  pntrsumbnd2  27484  pntrlog2bndlem4  27497  pntrlog2bndlem5  27498  pntrlog2bndlem6  27500  pntrlog2bnd  27501  pntpbnd1a  27502  pntpbnd1  27503  pntpbnd2  27504  pntpbnd  27505  pntibndlem2  27508  pntibndlem3  27509  pntibnd  27510  pntlemr  27519  nrt2irr  30408  nvge0  30608  nmcexi  31961  cshw1s2  32888  constrresqrtcl  33773  sqsscirc1  33904  dya2ub  34267  dya2iocress  34271  dya2iocbrsiga  34272  dya2icobrsiga  34273  dya2icoseg  34274  sxbrsigalem2  34283  omssubadd  34297  fiblem  34395  fibp1  34398  coinflipprob  34477  signstfveq0  34574  hgt750lemd  34645  logdivsqrle  34647  hgt750lem  34648  unbdqndv2  36494  knoppndvlem12  36506  knoppndvlem14  36508  knoppndvlem17  36511  knoppndvlem18  36512  taupilem1  37304  taupilem2  37305  taupi  37306  poimirlem29  37638  itg2addnclem  37660  ftc1anclem7  37688  ftc1anc  37690  isbnd2  37772  lcmineqlem21  42032  lcmineqlem23  42034  3lexlogpow2ineq1  42041  dvrelog2b  42049  dvrelogpow2b  42051  aks4d1p1p2  42053  aks4d1p1p4  42054  aks4d1p1p6  42056  aks4d1p1p7  42057  aks4d1p1p5  42058  aks4d1p1  42059  aks4d1p6  42064  2np3bcnp1  42127  2ap1caineq  42128  aks6d1c7lem1  42163  asin1half  42340  fltne  42625  flt4lem7  42640  proot1ex  43178  sqrtcvallem2  43619  sqrtcvallem4  43621  sqrtcval  43623  oddfl  45269  sumnnodd  45621  wallispilem3  46058  wallispilem4  46059  wallispi  46061  wallispi2lem1  46062  stirlinglem2  46066  stirlinglem3  46067  stirlinglem4  46068  stirlinglem5  46069  stirlinglem6  46070  stirlinglem7  46071  stirlinglem10  46074  stirlinglem11  46075  stirlinglem13  46077  stirlinglem14  46078  stirlinglem15  46079  stirlingr  46081  dirker2re  46083  dirkerdenne0  46084  dirkerper  46087  dirkertrigeqlem1  46089  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkercncflem1  46094  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem10  46108  fourierdlem24  46122  fourierdlem62  46159  fourierdlem79  46176  fourierdlem87  46184  sqwvfoura  46219  sqwvfourb  46220  sge0ad2en  46422  ovnsubaddlem1  46561  hoiqssbllem1  46613  hoiqssbllem2  46614  hoiqssbllem3  46615  rehalfge1  47326  ceil5half3  47331  lighneallem3  47598  dfeven3  47649  dfodd4  47650  oexpnegALTV  47668  flnn0div2ge  48512  logbpw2m1  48546  fllog2  48547  blennnelnn  48555  nnpw2blen  48559  blen1b  48567  blennnt2  48568  nnolog2flm1  48569  blennngt2o2  48571  blennn0e2  48573  0dig2nn0e  48591  dignn0flhalflem1  48594  dignn0flhalflem2  48595