Theorem 2rp 13016

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 12310	. 2 ⊢ 2 ∈ ℝ
2		2pos 12340	. 2 ⊢ 0 < 2
3	1, 2	elrpii 13014	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2143  2c2 12290  ℝ⁺crp 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-2 12298  df-rp 13012

This theorem is referenced by:  rphalfcl  13040  ge2halflem1  13128  2tnp1ge0ge0  13858  flhalf  13859  fldiv4lem1div2uz2  13865  discr  14272  2swrd2eqwrdeq  14986  01sqrexlem7  15295  abstri  15378  amgm2  15417  iseralt  15732  climcndslem2  15900  climcnds  15901  efcllem  16126  oexpneg  16398  mod2eq1n2dvds  16400  oddge22np1  16402  evennn02n  16403  nn0ehalf  16431  nno  16435  nn0oddm1d2  16438  flodddiv4t2lthalf  16471  bitsfzolem  16487  bitsfzo  16488  bitsmod  16489  bitsinv1  16495  sadasslem  16523  sadeq  16525  oddprm  16865  iserodd  16890  prmreclem6  16976  prmgaplem7  17112  2expltfac  17147  psgnunilem4  19562  efgsfo  19804  efgredlemd  19809  efgredlem  19812  chfacfscmul0  23015  chfacfpmmul0  23019  psmetge0  24469  xmetge0  24501  metnrmlem3  25019  pcoass  25183  aaliou3lem1  26505  aaliou3lem2  26506  aaliou3lem3  26507  aaliou3lem8  26508  aaliou3lem5  26510  aaliou3lem6  26511  aaliou3lem7  26512  aaliou3lem9  26513  cos02pilt1  26691  cosordlem  26695  logi  26752  2irrexpq  26896  loglesqrt  26926  sqrt2cxp2logb9e3  26964  log2cnv  27109  log2ub  27114  log2le1  27115  birthday  27119  cxp2limlem  27140  divsqrtsumlem  27144  emcllem7  27166  emre  27170  emgt0  27171  harmonicbnd3  27172  zetacvg  27179  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamucov  27202  cht2  27336  cht3  27337  chtub  27376  bclbnd  27444  bposlem6  27453  bposlem7  27454  bposlem8  27455  bposlem9  27456  gausslemma2dlem1a  27529  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  2lgslem3a1  27564  2lgslem3d1  27567  chebbnd1lem2  27634  chebbnd1lem3  27635  chebbnd1  27636  chto1ub  27640  chpo1ubb  27645  rplogsumlem1  27648  selbergb  27713  selberg2b  27716  chpdifbndlem2  27718  pntrsumbnd2  27731  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntpbnd1a  27749  pntpbnd1  27750  pntpbnd2  27751  pntpbnd  27752  pntibndlem2  27755  pntibndlem3  27756  pntibnd  27757  pntlemr  27766  nrt2irr  30824  nvge0  31025  nmcexi  32378  cshw1s2  33280  constrresqrtcl  34167  sqsscirc1  34298  dya2ub  34660  dya2iocress  34664  dya2iocbrsiga  34665  dya2icobrsiga  34666  dya2icoseg  34667  sxbrsigalem2  34676  omssubadd  34690  fiblem  34788  fibp1  34791  coinflipprob  34870  signstfveq0  34964  hgt750lemd  35035  logdivsqrle  35037  hgt750lem  35038  unbdqndv2  37120  knoppndvlem12  37132  knoppndvlem14  37134  knoppndvlem17  37137  knoppndvlem18  37138  taupilem1  37985  taupilem2  37986  taupi  37987  poimirlem29  38320  itg2addnclem  38342  ftc1anclem7  38370  ftc1anc  38372  isbnd2  38454  lcmineqlem21  42836  lcmineqlem23  42838  3lexlogpow2ineq1  42845  dvrelog2b  42853  dvrelogpow2b  42855  aks4d1p1p2  42857  aks4d1p1p4  42858  aks4d1p1p6  42860  aks4d1p1p7  42861  aks4d1p1p5  42862  aks4d1p1  42863  aks4d1p6  42868  2np3bcnp1  42931  2ap1caineq  42932  aks6d1c7lem1  42967  asin1half  43138  fltne  43396  flt4lem7  43411  proot1ex  43943  sqrtcvallem2  44383  sqrtcvallem4  44385  sqrtcval  44387  oddfl  46017  sumnnodd  46366  wallispilem3  46801  wallispilem4  46802  wallispi  46804  wallispi2lem1  46805  stirlinglem2  46809  stirlinglem3  46810  stirlinglem4  46811  stirlinglem5  46812  stirlinglem6  46813  stirlinglem7  46814  stirlinglem10  46817  stirlinglem11  46818  stirlinglem13  46820  stirlinglem14  46821  stirlinglem15  46822  stirlingr  46824  dirker2re  46826  dirkerdenne0  46827  dirkerper  46830  dirkertrigeqlem1  46832  dirkertrigeqlem3  46834  dirkertrigeq  46835  dirkercncflem1  46837  dirkercncflem2  46838  dirkercncflem4  46840  fourierdlem10  46851  fourierdlem24  46865  fourierdlem62  46902  fourierdlem79  46919  fourierdlem87  46927  sqwvfoura  46962  sqwvfourb  46963  sge0ad2en  47165  ovnsubaddlem1  47304  hoiqssbllem1  47356  hoiqssbllem2  47357  hoiqssbllem3  47358  goldrapos  47640  rehalfge1  48096  ceil5half3  48103  lighneallem3  48379  dfeven3  48443  dfodd4  48444  oexpnegALTV  48462  flnn0div2ge  49333  logbpw2m1  49367  fllog2  49368  blennnelnn  49376  nnpw2blen  49380  blen1b  49388  blennnt2  49389  nnolog2flm1  49390  blennngt2o2  49392  blennn0e2  49394  0dig2nn0e  49412  dignn0flhalflem1  49415  dignn0flhalflem2  49416