Theorem 2rp 12938

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 12246	. 2 ⊢ 2 ∈ ℝ
2		2pos 12275	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12936	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2119  2c2 12227  ℝ⁺crp 12933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-po 5526  df-so 5527  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-2 12235  df-rp 12934

This theorem is referenced by:  rphalfcl  12962  ge2halflem1  13050  2tnp1ge0ge0  13779  flhalf  13780  fldiv4lem1div2uz2  13786  discr  14193  2swrd2eqwrdeq  14906  01sqrexlem7  15201  abstri  15284  amgm2  15323  iseralt  15638  climcndslem2  15806  climcnds  15807  efcllem  16033  oexpneg  16305  mod2eq1n2dvds  16307  oddge22np1  16309  evennn02n  16310  nn0ehalf  16338  nno  16342  nn0oddm1d2  16345  flodddiv4t2lthalf  16378  bitsfzolem  16394  bitsfzo  16395  bitsmod  16396  bitsinv1  16402  sadasslem  16430  sadeq  16432  oddprm  16772  iserodd  16797  prmreclem6  16883  prmgaplem7  17019  2expltfac  17054  psgnunilem4  19463  efgsfo  19705  efgredlemd  19710  efgredlem  19713  chfacfscmul0  22841  chfacfpmmul0  22845  psmetge0  24295  xmetge0  24327  metnrmlem3  24845  pcoass  25009  aaliou3lem1  26326  aaliou3lem2  26327  aaliou3lem3  26328  aaliou3lem8  26329  aaliou3lem5  26331  aaliou3lem6  26332  aaliou3lem7  26333  aaliou3lem9  26334  cos02pilt1  26508  cosordlem  26512  logi  26569  2irrexpq  26713  loglesqrt  26743  sqrt2cxp2logb9e3  26781  log2cnv  26926  log2ub  26931  log2le1  26932  birthday  26936  cxp2limlem  26957  divsqrtsumlem  26961  emcllem7  26983  emre  26987  emgt0  26988  harmonicbnd3  26989  zetacvg  26996  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamucov  27019  cht2  27153  cht3  27154  chtub  27193  bclbnd  27261  bposlem6  27270  bposlem7  27271  bposlem8  27272  bposlem9  27273  gausslemma2dlem1a  27346  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  2lgslem3a1  27381  2lgslem3d1  27384  chebbnd1lem2  27451  chebbnd1lem3  27452  chebbnd1  27453  chto1ub  27457  chpo1ubb  27462  rplogsumlem1  27465  selbergb  27530  selberg2b  27533  chpdifbndlem2  27535  pntrsumbnd2  27548  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntrlog2bnd  27565  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  pntpbnd  27569  pntibndlem2  27572  pntibndlem3  27573  pntibnd  27574  pntlemr  27583  nrt2irr  30561  nvge0  30762  nmcexi  32115  cshw1s2  33039  constrresqrtcl  33961  sqsscirc1  34092  dya2ub  34454  dya2iocress  34458  dya2iocbrsiga  34459  dya2icobrsiga  34460  dya2icoseg  34461  sxbrsigalem2  34470  omssubadd  34484  fiblem  34582  fibp1  34585  coinflipprob  34664  signstfveq0  34761  hgt750lemd  34832  logdivsqrle  34834  hgt750lem  34835  unbdqndv2  36817  knoppndvlem12  36829  knoppndvlem14  36831  knoppndvlem17  36834  knoppndvlem18  36835  taupilem1  37681  taupilem2  37682  taupi  37683  poimirlem29  38016  itg2addnclem  38038  ftc1anclem7  38066  ftc1anc  38068  isbnd2  38150  lcmineqlem21  42534  lcmineqlem23  42536  3lexlogpow2ineq1  42543  dvrelog2b  42551  dvrelogpow2b  42553  aks4d1p1p2  42555  aks4d1p1p4  42556  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p1  42561  aks4d1p6  42566  2np3bcnp1  42629  2ap1caineq  42630  aks6d1c7lem1  42665  asin1half  42834  fltne  43094  flt4lem7  43109  proot1ex  43641  sqrtcvallem2  44081  sqrtcvallem4  44083  sqrtcval  44085  oddfl  45726  sumnnodd  46075  wallispilem3  46510  wallispilem4  46511  wallispi  46513  wallispi2lem1  46514  stirlinglem2  46518  stirlinglem3  46519  stirlinglem4  46520  stirlinglem5  46521  stirlinglem6  46522  stirlinglem7  46523  stirlinglem10  46526  stirlinglem11  46527  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  stirlingr  46533  dirker2re  46535  dirkerdenne0  46536  dirkerper  46539  dirkertrigeqlem1  46541  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkercncflem1  46546  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem10  46560  fourierdlem24  46574  fourierdlem62  46611  fourierdlem79  46628  fourierdlem87  46636  sqwvfoura  46671  sqwvfourb  46672  sge0ad2en  46874  ovnsubaddlem1  47013  hoiqssbllem1  47065  hoiqssbllem2  47066  hoiqssbllem3  47067  goldrapos  47346  rehalfge1  47802  ceil5half3  47809  lighneallem3  48085  dfeven3  48149  dfodd4  48150  oexpnegALTV  48168  flnn0div2ge  49024  logbpw2m1  49058  fllog2  49059  blennnelnn  49067  nnpw2blen  49071  blen1b  49079  blennnt2  49080  nnolog2flm1  49081  blennngt2o2  49083  blennn0e2  49085  0dig2nn0e  49103  dignn0flhalflem1  49106  dignn0flhalflem2  49107