Theorem 2rp 13011

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 12312	. 2 ⊢ 2 ∈ ℝ
2		2pos 12341	. 2 ⊢ 0 < 2
3	1, 2	elrpii 13009	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2108  2c2 12293  ℝ⁺crp 13006

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-2 12301  df-rp 13007

This theorem is referenced by:  rphalfcl  13034  ge2halflem1  13122  2tnp1ge0ge0  13844  flhalf  13845  fldiv4lem1div2uz2  13851  discr  14256  2swrd2eqwrdeq  14970  01sqrexlem7  15265  abstri  15347  amgm2  15386  iseralt  15699  climcndslem2  15864  climcnds  15865  efcllem  16091  oexpneg  16362  mod2eq1n2dvds  16364  oddge22np1  16366  evennn02n  16367  nn0ehalf  16395  nno  16399  nn0oddm1d2  16402  flodddiv4t2lthalf  16435  bitsfzolem  16451  bitsfzo  16452  bitsmod  16453  bitsinv1  16459  sadasslem  16487  sadeq  16489  oddprm  16828  iserodd  16853  prmreclem6  16939  prmgaplem7  17075  2expltfac  17110  psgnunilem4  19476  efgsfo  19718  efgredlemd  19723  efgredlem  19726  chfacfscmul0  22794  chfacfpmmul0  22798  psmetge0  24249  xmetge0  24281  metnrmlem3  24799  pcoass  24973  aaliou3lem1  26300  aaliou3lem2  26301  aaliou3lem3  26302  aaliou3lem8  26303  aaliou3lem5  26305  aaliou3lem6  26306  aaliou3lem7  26307  aaliou3lem9  26308  cos02pilt1  26485  cosordlem  26489  logi  26546  2irrexpq  26690  loglesqrt  26721  sqrt2cxp2logb9e3  26759  log2cnv  26904  log2ub  26909  log2le1  26910  birthday  26914  cxp2limlem  26936  divsqrtsumlem  26940  emcllem7  26962  emre  26966  emgt0  26967  harmonicbnd3  26968  zetacvg  26975  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamucov  26998  cht2  27132  cht3  27133  chtub  27173  bclbnd  27241  bposlem6  27250  bposlem7  27251  bposlem8  27252  bposlem9  27253  gausslemma2dlem1a  27326  2lgslem3b  27358  2lgslem3c  27359  2lgslem3d  27360  2lgslem3a1  27361  2lgslem3d1  27364  chebbnd1lem2  27431  chebbnd1lem3  27432  chebbnd1  27433  chto1ub  27437  chpo1ubb  27442  rplogsumlem1  27445  selbergb  27510  selberg2b  27513  chpdifbndlem2  27515  pntrsumbnd2  27528  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntpbnd  27549  pntibndlem2  27552  pntibndlem3  27553  pntibnd  27554  pntlemr  27563  nrt2irr  30400  nvge0  30600  nmcexi  31953  cshw1s2  32882  constrresqrtcl  33757  sqsscirc1  33885  dya2ub  34248  dya2iocress  34252  dya2iocbrsiga  34253  dya2icobrsiga  34254  dya2icoseg  34255  sxbrsigalem2  34264  omssubadd  34278  fiblem  34376  fibp1  34379  coinflipprob  34458  signstfveq0  34555  hgt750lemd  34626  logdivsqrle  34628  hgt750lem  34629  unbdqndv2  36475  knoppndvlem12  36487  knoppndvlem14  36489  knoppndvlem17  36492  knoppndvlem18  36493  taupilem1  37285  taupilem2  37286  taupi  37287  poimirlem29  37619  itg2addnclem  37641  ftc1anclem7  37669  ftc1anc  37671  isbnd2  37753  lcmineqlem21  42008  lcmineqlem23  42010  3lexlogpow2ineq1  42017  dvrelog2b  42025  dvrelogpow2b  42027  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p6  42040  2np3bcnp1  42103  2ap1caineq  42104  aks6d1c7lem1  42139  asin1half  42347  fltne  42614  flt4lem7  42629  proot1ex  43167  sqrtcvallem2  43608  sqrtcvallem4  43610  sqrtcval  43612  oddfl  45254  sumnnodd  45607  wallispilem3  46044  wallispilem4  46045  wallispi  46047  wallispi2lem1  46048  stirlinglem2  46052  stirlinglem3  46053  stirlinglem4  46054  stirlinglem5  46055  stirlinglem6  46056  stirlinglem7  46057  stirlinglem10  46060  stirlinglem11  46061  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  stirlingr  46067  dirker2re  46069  dirkerdenne0  46070  dirkerper  46073  dirkertrigeqlem1  46075  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem1  46080  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem10  46094  fourierdlem24  46108  fourierdlem62  46145  fourierdlem79  46162  fourierdlem87  46170  sqwvfoura  46205  sqwvfourb  46206  sge0ad2en  46408  ovnsubaddlem1  46547  hoiqssbllem1  46599  hoiqssbllem2  46600  hoiqssbllem3  46601  rehalfge1  47312  ceil5half3  47317  lighneallem3  47569  dfeven3  47620  dfodd4  47621  oexpnegALTV  47639  flnn0div2ge  48461  logbpw2m1  48495  fllog2  48496  blennnelnn  48504  nnpw2blen  48508  blen1b  48516  blennnt2  48517  nnolog2flm1  48518  blennngt2o2  48520  blennn0e2  48522  0dig2nn0e  48540  dignn0flhalflem1  48543  dignn0flhalflem2  48544