Theorem 2rp 12941

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 12249	. 2 ⊢ 2 ∈ ℝ
2		2pos 12278	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12939	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2114  2c2 12230  ℝ⁺crp 12936

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-2 12238  df-rp 12937

This theorem is referenced by:  rphalfcl  12965  ge2halflem1  13053  2tnp1ge0ge0  13782  flhalf  13783  fldiv4lem1div2uz2  13789  discr  14196  2swrd2eqwrdeq  14909  01sqrexlem7  15204  abstri  15287  amgm2  15326  iseralt  15641  climcndslem2  15809  climcnds  15810  efcllem  16036  oexpneg  16308  mod2eq1n2dvds  16310  oddge22np1  16312  evennn02n  16313  nn0ehalf  16341  nno  16345  nn0oddm1d2  16348  flodddiv4t2lthalf  16381  bitsfzolem  16397  bitsfzo  16398  bitsmod  16399  bitsinv1  16405  sadasslem  16433  sadeq  16435  oddprm  16775  iserodd  16800  prmreclem6  16886  prmgaplem7  17022  2expltfac  17057  psgnunilem4  19466  efgsfo  19708  efgredlemd  19713  efgredlem  19716  chfacfscmul0  22836  chfacfpmmul0  22840  psmetge0  24290  xmetge0  24322  metnrmlem3  24840  pcoass  25004  aaliou3lem1  26322  aaliou3lem2  26323  aaliou3lem3  26324  aaliou3lem8  26325  aaliou3lem5  26327  aaliou3lem6  26328  aaliou3lem7  26329  aaliou3lem9  26330  cos02pilt1  26506  cosordlem  26510  logi  26567  2irrexpq  26711  loglesqrt  26741  sqrt2cxp2logb9e3  26779  log2cnv  26924  log2ub  26929  log2le1  26930  birthday  26934  cxp2limlem  26956  divsqrtsumlem  26960  emcllem7  26982  emre  26986  emgt0  26987  harmonicbnd3  26988  zetacvg  26995  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamucov  27018  cht2  27152  cht3  27153  chtub  27192  bclbnd  27260  bposlem6  27269  bposlem7  27270  bposlem8  27271  bposlem9  27272  gausslemma2dlem1a  27345  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  2lgslem3a1  27380  2lgslem3d1  27383  chebbnd1lem2  27450  chebbnd1lem3  27451  chebbnd1  27452  chto1ub  27456  chpo1ubb  27461  rplogsumlem1  27464  selbergb  27529  selberg2b  27532  chpdifbndlem2  27534  pntrsumbnd2  27547  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntrlog2bnd  27564  pntpbnd1a  27565  pntpbnd1  27566  pntpbnd2  27567  pntpbnd  27568  pntibndlem2  27571  pntibndlem3  27572  pntibnd  27573  pntlemr  27582  nrt2irr  30561  nvge0  30762  nmcexi  32115  cshw1s2  33038  constrresqrtcl  33940  sqsscirc1  34071  dya2ub  34433  dya2iocress  34437  dya2iocbrsiga  34438  dya2icobrsiga  34439  dya2icoseg  34440  sxbrsigalem2  34449  omssubadd  34463  fiblem  34561  fibp1  34564  coinflipprob  34643  signstfveq0  34740  hgt750lemd  34811  logdivsqrle  34813  hgt750lem  34814  unbdqndv2  36790  knoppndvlem12  36802  knoppndvlem14  36804  knoppndvlem17  36807  knoppndvlem18  36808  taupilem1  37654  taupilem2  37655  taupi  37656  poimirlem29  37987  itg2addnclem  38009  ftc1anclem7  38037  ftc1anc  38039  isbnd2  38121  lcmineqlem21  42505  lcmineqlem23  42507  3lexlogpow2ineq1  42514  dvrelog2b  42522  dvrelogpow2b  42524  aks4d1p1p2  42526  aks4d1p1p4  42527  aks4d1p1p6  42529  aks4d1p1p7  42530  aks4d1p1p5  42531  aks4d1p1  42532  aks4d1p6  42537  2np3bcnp1  42600  2ap1caineq  42601  aks6d1c7lem1  42636  asin1half  42806  fltne  43094  flt4lem7  43109  proot1ex  43645  sqrtcvallem2  44085  sqrtcvallem4  44087  sqrtcval  44089  oddfl  45732  sumnnodd  46081  wallispilem3  46516  wallispilem4  46517  wallispi  46519  wallispi2lem1  46520  stirlinglem2  46524  stirlinglem3  46525  stirlinglem4  46526  stirlinglem5  46527  stirlinglem6  46528  stirlinglem7  46529  stirlinglem10  46532  stirlinglem11  46533  stirlinglem13  46535  stirlinglem14  46536  stirlinglem15  46537  stirlingr  46539  dirker2re  46541  dirkerdenne0  46542  dirkerper  46545  dirkertrigeqlem1  46547  dirkertrigeqlem3  46549  dirkertrigeq  46550  dirkercncflem1  46552  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem10  46566  fourierdlem24  46580  fourierdlem62  46617  fourierdlem79  46634  fourierdlem87  46642  sqwvfoura  46677  sqwvfourb  46678  sge0ad2en  46880  ovnsubaddlem1  47019  hoiqssbllem1  47071  hoiqssbllem2  47072  hoiqssbllem3  47073  goldrapos  47348  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