Theorem 2rp 13021

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 12315	. 2 ⊢ 2 ∈ ℝ
2		2pos 12345	. 2 ⊢ 0 < 2
3	1, 2	elrpii 13019	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2149  2c2 12295  ℝ⁺crp 13016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-nn 12234  df-2 12303  df-rp 13017

This theorem is referenced by:  rphalfcl  13045  ge2halflem1  13133  2tnp1ge0ge0  13862  flhalf  13863  fldiv4lem1div2uz2  13869  discr  14276  2swrd2eqwrdeq  14990  01sqrexlem7  15299  abstri  15382  amgm2  15421  iseralt  15736  climcndslem2  15904  climcnds  15905  efcllem  16131  oexpneg  16403  mod2eq1n2dvds  16405  oddge22np1  16407  evennn02n  16408  nn0ehalf  16436  nno  16440  nn0oddm1d2  16443  flodddiv4t2lthalf  16476  bitsfzolem  16492  bitsfzo  16493  bitsmod  16494  bitsinv1  16500  sadasslem  16528  sadeq  16530  oddprm  16870  iserodd  16895  prmreclem6  16981  prmgaplem7  17117  2expltfac  17152  psgnunilem4  19567  efgsfo  19809  efgredlemd  19814  efgredlem  19817  chfacfscmul0  22984  chfacfpmmul0  22988  psmetge0  24438  xmetge0  24470  metnrmlem3  24988  pcoass  25152  aaliou3lem1  26472  aaliou3lem2  26473  aaliou3lem3  26474  aaliou3lem8  26475  aaliou3lem5  26477  aaliou3lem6  26478  aaliou3lem7  26479  aaliou3lem9  26480  cos02pilt1  26657  cosordlem  26661  logi  26718  2irrexpq  26862  loglesqrt  26892  sqrt2cxp2logb9e3  26930  log2cnv  27075  log2ub  27080  log2le1  27081  birthday  27085  cxp2limlem  27106  divsqrtsumlem  27110  emcllem7  27132  emre  27136  emgt0  27137  harmonicbnd3  27138  zetacvg  27145  lgamgulmlem2  27160  lgamgulmlem3  27161  lgamucov  27168  cht2  27302  cht3  27303  chtub  27342  bclbnd  27410  bposlem6  27419  bposlem7  27420  bposlem8  27421  bposlem9  27422  gausslemma2dlem1a  27495  2lgslem3b  27527  2lgslem3c  27528  2lgslem3d  27529  2lgslem3a1  27530  2lgslem3d1  27533  chebbnd1lem2  27600  chebbnd1lem3  27601  chebbnd1  27602  chto1ub  27606  chpo1ubb  27611  rplogsumlem1  27614  selbergb  27679  selberg2b  27682  chpdifbndlem2  27684  pntrsumbnd2  27697  pntrlog2bndlem4  27710  pntrlog2bndlem5  27711  pntrlog2bndlem6  27713  pntrlog2bnd  27714  pntpbnd1a  27715  pntpbnd1  27716  pntpbnd2  27717  pntpbnd  27718  pntibndlem2  27721  pntibndlem3  27722  pntibnd  27723  pntlemr  27732  nrt2irr  30765  nvge0  30966  nmcexi  32319  cshw1s2  33221  constrresqrtcl  34112  sqsscirc1  34243  dya2ub  34605  dya2iocress  34609  dya2iocbrsiga  34610  dya2icobrsiga  34611  dya2icoseg  34612  sxbrsigalem2  34621  omssubadd  34635  fiblem  34733  fibp1  34736  coinflipprob  34815  signstfveq0  34909  hgt750lemd  34980  logdivsqrle  34982  hgt750lem  34983  unbdqndv2  36989  knoppndvlem12  37001  knoppndvlem14  37003  knoppndvlem17  37006  knoppndvlem18  37007  taupilem1  37853  taupilem2  37854  taupi  37855  poimirlem29  38188  itg2addnclem  38210  ftc1anclem7  38238  ftc1anc  38240  isbnd2  38322  lcmineqlem21  42706  lcmineqlem23  42708  3lexlogpow2ineq1  42715  dvrelog2b  42723  dvrelogpow2b  42725  aks4d1p1p2  42727  aks4d1p1p4  42728  aks4d1p1p6  42730  aks4d1p1p7  42731  aks4d1p1p5  42732  aks4d1p1  42733  aks4d1p6  42738  2np3bcnp1  42801  2ap1caineq  42802  aks6d1c7lem1  42837  asin1half  43008  fltne  43268  flt4lem7  43283  proot1ex  43815  sqrtcvallem2  44255  sqrtcvallem4  44257  sqrtcval  44259  oddfl  45889  sumnnodd  46238  wallispilem3  46673  wallispilem4  46674  wallispi  46676  wallispi2lem1  46677  stirlinglem2  46681  stirlinglem3  46682  stirlinglem4  46683  stirlinglem5  46684  stirlinglem6  46685  stirlinglem7  46686  stirlinglem10  46689  stirlinglem11  46690  stirlinglem13  46692  stirlinglem14  46693  stirlinglem15  46694  stirlingr  46696  dirker2re  46698  dirkerdenne0  46699  dirkerper  46702  dirkertrigeqlem1  46704  dirkertrigeqlem3  46706  dirkertrigeq  46707  dirkercncflem1  46709  dirkercncflem2  46710  dirkercncflem4  46712  fourierdlem10  46723  fourierdlem24  46737  fourierdlem62  46774  fourierdlem79  46791  fourierdlem87  46799  sqwvfoura  46834  sqwvfourb  46835  sge0ad2en  47037  ovnsubaddlem1  47176  hoiqssbllem1  47228  hoiqssbllem2  47229  hoiqssbllem3  47230  goldrapos  47509  rehalfge1  47965  ceil5half3  47972  lighneallem3  48248  dfeven3  48312  dfodd4  48313  oexpnegALTV  48331  flnn0div2ge  49198  logbpw2m1  49232  fllog2  49233  blennnelnn  49241  nnpw2blen  49245  blen1b  49253  blennnt2  49254  nnolog2flm1  49255  blennngt2o2  49257  blennn0e2  49259  0dig2nn0e  49277  dignn0flhalflem1  49280  dignn0flhalflem2  49281