Theorem 2rp 13014

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 12319	. 2 ⊢ 2 ∈ ℝ
2		2pos 12348	. 2 ⊢ 0 < 2
3	1, 2	elrpii 13012	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2098  2c2 12300  ℝ⁺crp 13009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-2 12308  df-rp 13010

This theorem is referenced by:  rphalfcl  13036  2tnp1ge0ge0  13830  flhalf  13831  fldiv4lem1div2uz2  13837  discr  14238  2swrd2eqwrdeq  14940  01sqrexlem7  15231  abstri  15313  amgm2  15352  iseralt  15667  climcndslem2  15832  climcnds  15833  efcllem  16057  oexpneg  16325  mod2eq1n2dvds  16327  oddge22np1  16329  evennn02n  16330  nn0ehalf  16358  nno  16362  nn0oddm1d2  16365  flodddiv4t2lthalf  16396  bitsfzolem  16412  bitsfzo  16413  bitsmod  16414  bitsinv1  16420  sadasslem  16448  sadeq  16450  oddprm  16782  iserodd  16807  prmreclem6  16893  prmgaplem7  17029  2expltfac  17065  psgnunilem4  19464  efgsfo  19706  efgredlemd  19711  efgredlem  19714  chfacfscmul0  22804  chfacfpmmul0  22808  psmetge0  24262  xmetge0  24294  metnrmlem3  24821  pcoass  24995  aaliou3lem1  26322  aaliou3lem2  26323  aaliou3lem3  26324  aaliou3lem8  26325  aaliou3lem5  26327  aaliou3lem6  26328  aaliou3lem7  26329  aaliou3lem9  26330  cos02pilt1  26505  cosordlem  26509  logi  26566  2irrexpq  26710  loglesqrt  26738  sqrt2cxp2logb9e3  26776  log2cnv  26921  log2ub  26926  log2le1  26927  birthday  26931  cxp2limlem  26953  divsqrtsumlem  26957  emcllem7  26979  emre  26983  emgt0  26984  harmonicbnd3  26985  zetacvg  26992  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamucov  27015  cht2  27149  cht3  27150  chtub  27190  bclbnd  27258  bposlem6  27267  bposlem7  27268  bposlem8  27269  bposlem9  27270  gausslemma2dlem1a  27343  2lgslem3b  27375  2lgslem3c  27376  2lgslem3d  27377  2lgslem3a1  27378  2lgslem3d1  27381  chebbnd1lem2  27448  chebbnd1lem3  27449  chebbnd1  27450  chto1ub  27454  chpo1ubb  27459  rplogsumlem1  27462  selbergb  27527  selberg2b  27530  chpdifbndlem2  27532  pntrsumbnd2  27545  pntrlog2bndlem4  27558  pntrlog2bndlem5  27559  pntrlog2bndlem6  27561  pntrlog2bnd  27562  pntpbnd1a  27563  pntpbnd1  27564  pntpbnd2  27565  pntpbnd  27566  pntibndlem2  27569  pntibndlem3  27570  pntibnd  27571  pntlemr  27580  nrt2irr  30355  nvge0  30555  nmcexi  31908  cshw1s2  32770  sqsscirc1  33640  dya2ub  34021  dya2iocress  34025  dya2iocbrsiga  34026  dya2icobrsiga  34027  dya2icoseg  34028  sxbrsigalem2  34037  omssubadd  34051  fiblem  34149  fibp1  34152  coinflipprob  34230  signstfveq0  34340  hgt750lemd  34411  logdivsqrle  34413  hgt750lem  34414  unbdqndv2  36117  knoppndvlem12  36129  knoppndvlem14  36131  knoppndvlem17  36134  knoppndvlem18  36135  taupilem1  36931  taupilem2  36932  taupi  36933  poimirlem29  37253  itg2addnclem  37275  ftc1anclem7  37303  ftc1anc  37305  isbnd2  37387  lcmineqlem21  41652  lcmineqlem23  41654  3lexlogpow2ineq1  41661  dvrelog2b  41669  dvrelogpow2b  41671  aks4d1p1p2  41673  aks4d1p1p4  41674  aks4d1p1p6  41676  aks4d1p1p7  41677  aks4d1p1p5  41678  aks4d1p1  41679  aks4d1p6  41684  2np3bcnp1  41747  2ap1caineq  41748  aks6d1c7lem1  41783  fltne  42203  flt4lem7  42218  proot1ex  42766  sqrtcvallem2  43209  sqrtcvallem4  43211  sqrtcval  43213  oddfl  44797  sumnnodd  45156  wallispilem3  45593  wallispilem4  45594  wallispi  45596  wallispi2lem1  45597  stirlinglem2  45601  stirlinglem3  45602  stirlinglem4  45603  stirlinglem5  45604  stirlinglem6  45605  stirlinglem7  45606  stirlinglem10  45609  stirlinglem11  45610  stirlinglem13  45612  stirlinglem14  45613  stirlinglem15  45614  stirlingr  45616  dirker2re  45618  dirkerdenne0  45619  dirkerper  45622  dirkertrigeqlem1  45624  dirkertrigeqlem3  45626  dirkertrigeq  45627  dirkercncflem1  45629  dirkercncflem2  45630  dirkercncflem4  45632  fourierdlem10  45643  fourierdlem24  45657  fourierdlem62  45694  fourierdlem79  45711  fourierdlem87  45719  sqwvfoura  45754  sqwvfourb  45755  sge0ad2en  45957  ovnsubaddlem1  46096  hoiqssbllem1  46148  hoiqssbllem2  46149  hoiqssbllem3  46150  lighneallem3  47084  dfeven3  47135  dfodd4  47136  oexpnegALTV  47154  flnn0div2ge  47792  logbpw2m1  47826  fllog2  47827  blennnelnn  47835  nnpw2blen  47839  blen1b  47847  blennnt2  47848  nnolog2flm1  47849  blennngt2o2  47851  blennn0e2  47853  0dig2nn0e  47871  dignn0flhalflem1  47874  dignn0flhalflem2  47875