Theorem 2rp 12908

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

Syntax hints:   ∈ wcel 2113  2c2 12198  ℝ⁺crp 12903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-2 12206  df-rp 12904

This theorem is referenced by:  rphalfcl  12932  ge2halflem1  13020  2tnp1ge0ge0  13747  flhalf  13748  fldiv4lem1div2uz2  13754  discr  14161  2swrd2eqwrdeq  14874  01sqrexlem7  15169  abstri  15252  amgm2  15291  iseralt  15606  climcndslem2  15771  climcnds  15772  efcllem  15998  oexpneg  16270  mod2eq1n2dvds  16272  oddge22np1  16274  evennn02n  16275  nn0ehalf  16303  nno  16307  nn0oddm1d2  16310  flodddiv4t2lthalf  16343  bitsfzolem  16359  bitsfzo  16360  bitsmod  16361  bitsinv1  16367  sadasslem  16395  sadeq  16397  oddprm  16736  iserodd  16761  prmreclem6  16847  prmgaplem7  16983  2expltfac  17018  psgnunilem4  19424  efgsfo  19666  efgredlemd  19671  efgredlem  19674  chfacfscmul0  22800  chfacfpmmul0  22804  psmetge0  24254  xmetge0  24286  metnrmlem3  24804  pcoass  24978  aaliou3lem1  26304  aaliou3lem2  26305  aaliou3lem3  26306  aaliou3lem8  26307  aaliou3lem5  26309  aaliou3lem6  26310  aaliou3lem7  26311  aaliou3lem9  26312  cos02pilt1  26489  cosordlem  26493  logi  26550  2irrexpq  26694  loglesqrt  26725  sqrt2cxp2logb9e3  26763  log2cnv  26908  log2ub  26913  log2le1  26914  birthday  26918  cxp2limlem  26940  divsqrtsumlem  26944  emcllem7  26966  emre  26970  emgt0  26971  harmonicbnd3  26972  zetacvg  26979  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamucov  27002  cht2  27136  cht3  27137  chtub  27177  bclbnd  27245  bposlem6  27254  bposlem7  27255  bposlem8  27256  bposlem9  27257  gausslemma2dlem1a  27330  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  2lgslem3a1  27365  2lgslem3d1  27368  chebbnd1lem2  27435  chebbnd1lem3  27436  chebbnd1  27437  chto1ub  27441  chpo1ubb  27446  rplogsumlem1  27449  selbergb  27514  selberg2b  27517  chpdifbndlem2  27519  pntrsumbnd2  27532  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntrlog2bnd  27549  pntpbnd1a  27550  pntpbnd1  27551  pntpbnd2  27552  pntpbnd  27553  pntibndlem2  27556  pntibndlem3  27557  pntibnd  27558  pntlemr  27567  nrt2irr  30497  nvge0  30697  nmcexi  32050  cshw1s2  32991  constrresqrtcl  33883  sqsscirc1  34014  dya2ub  34376  dya2iocress  34380  dya2iocbrsiga  34381  dya2icobrsiga  34382  dya2icoseg  34383  sxbrsigalem2  34392  omssubadd  34406  fiblem  34504  fibp1  34507  coinflipprob  34586  signstfveq0  34683  hgt750lemd  34754  logdivsqrle  34756  hgt750lem  34757  unbdqndv2  36654  knoppndvlem12  36666  knoppndvlem14  36668  knoppndvlem17  36671  knoppndvlem18  36672  taupilem1  37465  taupilem2  37466  taupi  37467  poimirlem29  37789  itg2addnclem  37811  ftc1anclem7  37839  ftc1anc  37841  isbnd2  37923  lcmineqlem21  42242  lcmineqlem23  42244  3lexlogpow2ineq1  42251  dvrelog2b  42259  dvrelogpow2b  42261  aks4d1p1p2  42263  aks4d1p1p4  42264  aks4d1p1p6  42266  aks4d1p1p7  42267  aks4d1p1p5  42268  aks4d1p1  42269  aks4d1p6  42274  2np3bcnp1  42337  2ap1caineq  42338  aks6d1c7lem1  42373  asin1half  42554  fltne  42829  flt4lem7  42844  proot1ex  43380  sqrtcvallem2  43820  sqrtcvallem4  43822  sqrtcval  43824  oddfl  45468  sumnnodd  45818  wallispilem3  46253  wallispilem4  46254  wallispi  46256  wallispi2lem1  46257  stirlinglem2  46261  stirlinglem3  46262  stirlinglem4  46263  stirlinglem5  46264  stirlinglem6  46265  stirlinglem7  46266  stirlinglem10  46269  stirlinglem11  46270  stirlinglem13  46272  stirlinglem14  46273  stirlinglem15  46274  stirlingr  46276  dirker2re  46278  dirkerdenne0  46279  dirkerper  46282  dirkertrigeqlem1  46284  dirkertrigeqlem3  46286  dirkertrigeq  46287  dirkercncflem1  46289  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem10  46303  fourierdlem24  46317  fourierdlem62  46354  fourierdlem79  46371  fourierdlem87  46379  sqwvfoura  46414  sqwvfourb  46415  sge0ad2en  46617  ovnsubaddlem1  46756  hoiqssbllem1  46808  hoiqssbllem2  46809  hoiqssbllem3  46810  rehalfge1  47523  ceil5half3  47528  lighneallem3  47795  dfeven3  47846  dfodd4  47847  oexpnegALTV  47865  flnn0div2ge  48721  logbpw2m1  48755  fllog2  48756  blennnelnn  48764  nnpw2blen  48768  blen1b  48776  blennnt2  48777  nnolog2flm1  48778  blennngt2o2  48780  blennn0e2  48782  0dig2nn0e  48800  dignn0flhalflem1  48803  dignn0flhalflem2  48804