Theorem 2rp 12963

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 12267	. 2 ⊢ 2 ∈ ℝ
2		2pos 12296	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12961	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2109  2c2 12248  ℝ⁺crp 12958

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 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

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 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-2 12256  df-rp 12959

This theorem is referenced by:  rphalfcl  12987  ge2halflem1  13075  2tnp1ge0ge0  13798  flhalf  13799  fldiv4lem1div2uz2  13805  discr  14212  2swrd2eqwrdeq  14926  01sqrexlem7  15221  abstri  15304  amgm2  15343  iseralt  15658  climcndslem2  15823  climcnds  15824  efcllem  16050  oexpneg  16322  mod2eq1n2dvds  16324  oddge22np1  16326  evennn02n  16327  nn0ehalf  16355  nno  16359  nn0oddm1d2  16362  flodddiv4t2lthalf  16395  bitsfzolem  16411  bitsfzo  16412  bitsmod  16413  bitsinv1  16419  sadasslem  16447  sadeq  16449  oddprm  16788  iserodd  16813  prmreclem6  16899  prmgaplem7  17035  2expltfac  17070  psgnunilem4  19434  efgsfo  19676  efgredlemd  19681  efgredlem  19684  chfacfscmul0  22752  chfacfpmmul0  22756  psmetge0  24207  xmetge0  24239  metnrmlem3  24757  pcoass  24931  aaliou3lem1  26257  aaliou3lem2  26258  aaliou3lem3  26259  aaliou3lem8  26260  aaliou3lem5  26262  aaliou3lem6  26263  aaliou3lem7  26264  aaliou3lem9  26265  cos02pilt1  26442  cosordlem  26446  logi  26503  2irrexpq  26647  loglesqrt  26678  sqrt2cxp2logb9e3  26716  log2cnv  26861  log2ub  26866  log2le1  26867  birthday  26871  cxp2limlem  26893  divsqrtsumlem  26897  emcllem7  26919  emre  26923  emgt0  26924  harmonicbnd3  26925  zetacvg  26932  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamucov  26955  cht2  27089  cht3  27090  chtub  27130  bclbnd  27198  bposlem6  27207  bposlem7  27208  bposlem8  27209  bposlem9  27210  gausslemma2dlem1a  27283  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgslem3a1  27318  2lgslem3d1  27321  chebbnd1lem2  27388  chebbnd1lem3  27389  chebbnd1  27390  chto1ub  27394  chpo1ubb  27399  rplogsumlem1  27402  selbergb  27467  selberg2b  27470  chpdifbndlem2  27472  pntrsumbnd2  27485  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntrlog2bnd  27502  pntpbnd1a  27503  pntpbnd1  27504  pntpbnd2  27505  pntpbnd  27506  pntibndlem2  27509  pntibndlem3  27510  pntibnd  27511  pntlemr  27520  nrt2irr  30409  nvge0  30609  nmcexi  31962  cshw1s2  32889  constrresqrtcl  33774  sqsscirc1  33905  dya2ub  34268  dya2iocress  34272  dya2iocbrsiga  34273  dya2icobrsiga  34274  dya2icoseg  34275  sxbrsigalem2  34284  omssubadd  34298  fiblem  34396  fibp1  34399  coinflipprob  34478  signstfveq0  34575  hgt750lemd  34646  logdivsqrle  34648  hgt750lem  34649  unbdqndv2  36506  knoppndvlem12  36518  knoppndvlem14  36520  knoppndvlem17  36523  knoppndvlem18  36524  taupilem1  37316  taupilem2  37317  taupi  37318  poimirlem29  37650  itg2addnclem  37672  ftc1anclem7  37700  ftc1anc  37702  isbnd2  37784  lcmineqlem21  42044  lcmineqlem23  42046  3lexlogpow2ineq1  42053  dvrelog2b  42061  dvrelogpow2b  42063  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p6  42076  2np3bcnp1  42139  2ap1caineq  42140  aks6d1c7lem1  42175  asin1half  42352  fltne  42639  flt4lem7  42654  proot1ex  43192  sqrtcvallem2  43633  sqrtcvallem4  43635  sqrtcval  43637  oddfl  45283  sumnnodd  45635  wallispilem3  46072  wallispilem4  46073  wallispi  46075  wallispi2lem1  46076  stirlinglem2  46080  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem10  46088  stirlinglem11  46089  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  stirlingr  46095  dirker2re  46097  dirkerdenne0  46098  dirkerper  46101  dirkertrigeqlem1  46103  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem10  46122  fourierdlem24  46136  fourierdlem62  46173  fourierdlem79  46190  fourierdlem87  46198  sqwvfoura  46233  sqwvfourb  46234  sge0ad2en  46436  ovnsubaddlem1  46575  hoiqssbllem1  46627  hoiqssbllem2  46628  hoiqssbllem3  46629  rehalfge1  47340  ceil5half3  47345  lighneallem3  47612  dfeven3  47663  dfodd4  47664  oexpnegALTV  47682  flnn0div2ge  48526  logbpw2m1  48560  fllog2  48561  blennnelnn  48569  nnpw2blen  48573  blen1b  48581  blennnt2  48582  nnolog2flm1  48583  blennngt2o2  48585  blennn0e2  48587  0dig2nn0e  48605  dignn0flhalflem1  48608  dignn0flhalflem2  48609