Theorem 2rp 12998

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 12292	. 2 ⊢ 2 ∈ ℝ
2		2pos 12322	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12996	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2142  2c2 12272  ℝ⁺crp 12993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-2 12280  df-rp 12994

This theorem is referenced by:  rphalfcl  13022  ge2halflem1  13110  2tnp1ge0ge0  13839  flhalf  13840  fldiv4lem1div2uz2  13846  discr  14253  2swrd2eqwrdeq  14966  01sqrexlem7  15275  abstri  15358  amgm2  15397  iseralt  15712  climcndslem2  15880  climcnds  15881  efcllem  16107  oexpneg  16379  mod2eq1n2dvds  16381  oddge22np1  16383  evennn02n  16384  nn0ehalf  16412  nno  16416  nn0oddm1d2  16419  flodddiv4t2lthalf  16452  bitsfzolem  16468  bitsfzo  16469  bitsmod  16470  bitsinv1  16476  sadasslem  16504  sadeq  16506  oddprm  16846  iserodd  16871  prmreclem6  16957  prmgaplem7  17093  2expltfac  17128  psgnunilem4  19537  efgsfo  19779  efgredlemd  19784  efgredlem  19787  chfacfscmul0  22918  chfacfpmmul0  22922  psmetge0  24372  xmetge0  24404  metnrmlem3  24922  pcoass  25086  aaliou3lem1  26406  aaliou3lem2  26407  aaliou3lem3  26408  aaliou3lem8  26409  aaliou3lem5  26411  aaliou3lem6  26412  aaliou3lem7  26413  aaliou3lem9  26414  cos02pilt1  26591  cosordlem  26595  logi  26652  2irrexpq  26796  loglesqrt  26826  sqrt2cxp2logb9e3  26864  log2cnv  27009  log2ub  27014  log2le1  27015  birthday  27019  cxp2limlem  27040  divsqrtsumlem  27044  emcllem7  27066  emre  27070  emgt0  27071  harmonicbnd3  27072  zetacvg  27079  lgamgulmlem2  27094  lgamgulmlem3  27095  lgamucov  27102  cht2  27236  cht3  27237  chtub  27276  bclbnd  27344  bposlem6  27353  bposlem7  27354  bposlem8  27355  bposlem9  27356  gausslemma2dlem1a  27429  2lgslem3b  27461  2lgslem3c  27462  2lgslem3d  27463  2lgslem3a1  27464  2lgslem3d1  27467  chebbnd1lem2  27534  chebbnd1lem3  27535  chebbnd1  27536  chto1ub  27540  chpo1ubb  27545  rplogsumlem1  27548  selbergb  27613  selberg2b  27616  chpdifbndlem2  27618  pntrsumbnd2  27631  pntrlog2bndlem4  27644  pntrlog2bndlem5  27645  pntrlog2bndlem6  27647  pntrlog2bnd  27648  pntpbnd1a  27649  pntpbnd1  27650  pntpbnd2  27651  pntpbnd  27652  pntibndlem2  27655  pntibndlem3  27656  pntibnd  27657  pntlemr  27666  nrt2irr  30675  nvge0  30876  nmcexi  32229  cshw1s2  33138  constrresqrtcl  34074  sqsscirc1  34205  dya2ub  34567  dya2iocress  34571  dya2iocbrsiga  34572  dya2icobrsiga  34573  dya2icoseg  34574  sxbrsigalem2  34583  omssubadd  34597  fiblem  34695  fibp1  34698  coinflipprob  34777  signstfveq0  34871  hgt750lemd  34942  logdivsqrle  34944  hgt750lem  34945  unbdqndv2  36949  knoppndvlem12  36961  knoppndvlem14  36963  knoppndvlem17  36966  knoppndvlem18  36967  taupilem1  37813  taupilem2  37814  taupi  37815  poimirlem29  38148  itg2addnclem  38170  ftc1anclem7  38198  ftc1anc  38200  isbnd2  38282  lcmineqlem21  42666  lcmineqlem23  42668  3lexlogpow2ineq1  42675  dvrelog2b  42683  dvrelogpow2b  42685  aks4d1p1p2  42687  aks4d1p1p4  42688  aks4d1p1p6  42690  aks4d1p1p7  42691  aks4d1p1p5  42692  aks4d1p1  42693  aks4d1p6  42698  2np3bcnp1  42761  2ap1caineq  42762  aks6d1c7lem1  42797  asin1half  42966  fltne  43226  flt4lem7  43241  proot1ex  43773  sqrtcvallem2  44213  sqrtcvallem4  44215  sqrtcval  44217  oddfl  45857  sumnnodd  46206  wallispilem3  46641  wallispilem4  46642  wallispi  46644  wallispi2lem1  46645  stirlinglem2  46649  stirlinglem3  46650  stirlinglem4  46651  stirlinglem5  46652  stirlinglem6  46653  stirlinglem7  46654  stirlinglem10  46657  stirlinglem11  46658  stirlinglem13  46660  stirlinglem14  46661  stirlinglem15  46662  stirlingr  46664  dirker2re  46666  dirkerdenne0  46667  dirkerper  46670  dirkertrigeqlem1  46672  dirkertrigeqlem3  46674  dirkertrigeq  46675  dirkercncflem1  46677  dirkercncflem2  46678  dirkercncflem4  46680  fourierdlem10  46691  fourierdlem24  46705  fourierdlem62  46742  fourierdlem79  46759  fourierdlem87  46767  sqwvfoura  46802  sqwvfourb  46803  sge0ad2en  47005  ovnsubaddlem1  47144  hoiqssbllem1  47196  hoiqssbllem2  47197  hoiqssbllem3  47198  goldrapos  47477  rehalfge1  47933  ceil5half3  47940  lighneallem3  48216  dfeven3  48280  dfodd4  48281  oexpnegALTV  48299  flnn0div2ge  49155  logbpw2m1  49189  fllog2  49190  blennnelnn  49198  nnpw2blen  49202  blen1b  49210  blennnt2  49211  nnolog2flm1  49212  blennngt2o2  49214  blennn0e2  49216  0dig2nn0e  49234  dignn0flhalflem1  49237  dignn0flhalflem2  49238