Theorem 2rp 12975

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 12282	. 2 ⊢ 2 ∈ ℝ
2		2pos 12311	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12973	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2106  2c2 12263  ℝ⁺crp 12970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-2 12271  df-rp 12971

This theorem is referenced by:  rphalfcl  12997  2tnp1ge0ge0  13790  flhalf  13791  fldiv4lem1div2uz2  13797  discr  14199  2swrd2eqwrdeq  14900  01sqrexlem7  15191  abstri  15273  amgm2  15312  iseralt  15627  climcndslem2  15792  climcnds  15793  efcllem  16017  oexpneg  16284  mod2eq1n2dvds  16286  oddge22np1  16288  evennn02n  16289  nn0ehalf  16317  nno  16321  nn0oddm1d2  16324  flodddiv4t2lthalf  16355  bitsfzolem  16371  bitsfzo  16372  bitsmod  16373  bitsinv1  16379  sadasslem  16407  sadeq  16409  oddprm  16739  iserodd  16764  prmreclem6  16850  prmgaplem7  16986  2expltfac  17022  psgnunilem4  19359  efgsfo  19601  efgredlemd  19606  efgredlem  19609  chfacfscmul0  22351  chfacfpmmul0  22355  psmetge0  23809  xmetge0  23841  metnrmlem3  24368  pcoass  24531  aaliou3lem1  25846  aaliou3lem2  25847  aaliou3lem3  25848  aaliou3lem8  25849  aaliou3lem5  25851  aaliou3lem6  25852  aaliou3lem7  25853  aaliou3lem9  25854  cos02pilt1  26026  cosordlem  26030  2irrexpq  26229  loglesqrt  26255  sqrt2cxp2logb9e3  26293  log2cnv  26438  log2ub  26443  log2le1  26444  birthday  26448  cxp2limlem  26469  divsqrtsumlem  26473  emcllem7  26495  emre  26499  emgt0  26500  harmonicbnd3  26501  zetacvg  26508  lgamgulmlem2  26523  lgamgulmlem3  26524  lgamucov  26531  cht2  26665  cht3  26666  chtub  26704  bclbnd  26772  bposlem6  26781  bposlem7  26782  bposlem8  26783  bposlem9  26784  gausslemma2dlem1a  26857  2lgslem3b  26889  2lgslem3c  26890  2lgslem3d  26891  2lgslem3a1  26892  2lgslem3d1  26895  chebbnd1lem2  26962  chebbnd1lem3  26963  chebbnd1  26964  chto1ub  26968  chpo1ubb  26973  rplogsumlem1  26976  selbergb  27041  selberg2b  27044  chpdifbndlem2  27046  pntrsumbnd2  27059  pntrlog2bndlem4  27072  pntrlog2bndlem5  27073  pntrlog2bndlem6  27075  pntrlog2bnd  27076  pntpbnd1a  27077  pntpbnd1  27078  pntpbnd2  27079  pntpbnd  27080  pntibndlem2  27083  pntibndlem3  27084  pntibnd  27085  pntlemr  27094  nvge0  29913  nmcexi  31266  cshw1s2  32111  sqsscirc1  32876  dya2ub  33257  dya2iocress  33261  dya2iocbrsiga  33262  dya2icobrsiga  33263  dya2icoseg  33264  sxbrsigalem2  33273  omssubadd  33287  fiblem  33385  fibp1  33388  coinflipprob  33466  signstfveq0  33576  hgt750lemd  33648  logdivsqrle  33650  hgt750lem  33651  logi  34692  unbdqndv2  35375  knoppndvlem12  35387  knoppndvlem14  35389  knoppndvlem17  35392  knoppndvlem18  35393  taupilem1  36190  taupilem2  36191  taupi  36192  poimirlem29  36505  itg2addnclem  36527  ftc1anclem7  36555  ftc1anc  36557  isbnd2  36639  lcmineqlem21  40902  lcmineqlem23  40904  3lexlogpow2ineq1  40911  dvrelog2b  40919  dvrelogpow2b  40921  aks4d1p1p2  40923  aks4d1p1p4  40924  aks4d1p1p6  40926  aks4d1p1p7  40927  aks4d1p1p5  40928  aks4d1p1  40929  aks4d1p6  40934  2np3bcnp1  40948  2ap1caineq  40949  fltne  41382  flt4lem7  41397  proot1ex  41928  sqrtcvallem2  42373  sqrtcvallem4  42375  sqrtcval  42377  oddfl  43973  sumnnodd  44332  wallispilem3  44769  wallispilem4  44770  wallispi  44772  wallispi2lem1  44773  stirlinglem2  44777  stirlinglem3  44778  stirlinglem4  44779  stirlinglem5  44780  stirlinglem6  44781  stirlinglem7  44782  stirlinglem10  44785  stirlinglem11  44786  stirlinglem13  44788  stirlinglem14  44789  stirlinglem15  44790  stirlingr  44792  dirker2re  44794  dirkerdenne0  44795  dirkerper  44798  dirkertrigeqlem1  44800  dirkertrigeqlem3  44802  dirkertrigeq  44803  dirkercncflem1  44805  dirkercncflem2  44806  dirkercncflem4  44808  fourierdlem10  44819  fourierdlem24  44833  fourierdlem62  44870  fourierdlem79  44887  fourierdlem87  44895  sqwvfoura  44930  sqwvfourb  44931  sge0ad2en  45133  ovnsubaddlem1  45272  hoiqssbllem1  45324  hoiqssbllem2  45325  hoiqssbllem3  45326  lighneallem3  46261  dfeven3  46312  dfodd4  46313  oexpnegALTV  46331  flnn0div2ge  47172  logbpw2m1  47206  fllog2  47207  blennnelnn  47215  nnpw2blen  47219  blen1b  47227  blennnt2  47228  nnolog2flm1  47229  blennngt2o2  47231  blennn0e2  47233  0dig2nn0e  47251  dignn0flhalflem1  47254  dignn0flhalflem2  47255