Theorem 2rp 12898

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 12202	. 2 ⊢ 2 ∈ ℝ
2		2pos 12231	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12896	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2109  2c2 12183  ℝ⁺crp 12893

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 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-2 12191  df-rp 12894

This theorem is referenced by:  rphalfcl  12922  ge2halflem1  13010  2tnp1ge0ge0  13733  flhalf  13734  fldiv4lem1div2uz2  13740  discr  14147  2swrd2eqwrdeq  14860  01sqrexlem7  15155  abstri  15238  amgm2  15277  iseralt  15592  climcndslem2  15757  climcnds  15758  efcllem  15984  oexpneg  16256  mod2eq1n2dvds  16258  oddge22np1  16260  evennn02n  16261  nn0ehalf  16289  nno  16293  nn0oddm1d2  16296  flodddiv4t2lthalf  16329  bitsfzolem  16345  bitsfzo  16346  bitsmod  16347  bitsinv1  16353  sadasslem  16381  sadeq  16383  oddprm  16722  iserodd  16747  prmreclem6  16833  prmgaplem7  16969  2expltfac  17004  psgnunilem4  19376  efgsfo  19618  efgredlemd  19623  efgredlem  19626  chfacfscmul0  22743  chfacfpmmul0  22747  psmetge0  24198  xmetge0  24230  metnrmlem3  24748  pcoass  24922  aaliou3lem1  26248  aaliou3lem2  26249  aaliou3lem3  26250  aaliou3lem8  26251  aaliou3lem5  26253  aaliou3lem6  26254  aaliou3lem7  26255  aaliou3lem9  26256  cos02pilt1  26433  cosordlem  26437  logi  26494  2irrexpq  26638  loglesqrt  26669  sqrt2cxp2logb9e3  26707  log2cnv  26852  log2ub  26857  log2le1  26858  birthday  26862  cxp2limlem  26884  divsqrtsumlem  26888  emcllem7  26910  emre  26914  emgt0  26915  harmonicbnd3  26916  zetacvg  26923  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamucov  26946  cht2  27080  cht3  27081  chtub  27121  bclbnd  27189  bposlem6  27198  bposlem7  27199  bposlem8  27200  bposlem9  27201  gausslemma2dlem1a  27274  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  2lgslem3a1  27309  2lgslem3d1  27312  chebbnd1lem2  27379  chebbnd1lem3  27380  chebbnd1  27381  chto1ub  27385  chpo1ubb  27390  rplogsumlem1  27393  selbergb  27458  selberg2b  27461  chpdifbndlem2  27463  pntrsumbnd2  27476  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6  27492  pntrlog2bnd  27493  pntpbnd1a  27494  pntpbnd1  27495  pntpbnd2  27496  pntpbnd  27497  pntibndlem2  27500  pntibndlem3  27501  pntibnd  27502  pntlemr  27511  nrt2irr  30417  nvge0  30617  nmcexi  31970  cshw1s2  32903  constrresqrtcl  33750  sqsscirc1  33881  dya2ub  34244  dya2iocress  34248  dya2iocbrsiga  34249  dya2icobrsiga  34250  dya2icoseg  34251  sxbrsigalem2  34260  omssubadd  34274  fiblem  34372  fibp1  34375  coinflipprob  34454  signstfveq0  34551  hgt750lemd  34622  logdivsqrle  34624  hgt750lem  34625  unbdqndv2  36495  knoppndvlem12  36507  knoppndvlem14  36509  knoppndvlem17  36512  knoppndvlem18  36513  taupilem1  37305  taupilem2  37306  taupi  37307  poimirlem29  37639  itg2addnclem  37661  ftc1anclem7  37689  ftc1anc  37691  isbnd2  37773  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  42627  flt4lem7  42642  proot1ex  43179  sqrtcvallem2  43620  sqrtcvallem4  43622  sqrtcval  43624  oddfl  45270  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  47329  ceil5half3  47334  lighneallem3  47601  dfeven3  47652  dfodd4  47653  oexpnegALTV  47671  flnn0div2ge  48528  logbpw2m1  48562  fllog2  48563  blennnelnn  48571  nnpw2blen  48575  blen1b  48583  blennnt2  48584  nnolog2flm1  48585  blennngt2o2  48587  blennn0e2  48589  0dig2nn0e  48607  dignn0flhalflem1  48610  dignn0flhalflem2  48611