Theorem 2rp 12956

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 12260	. 2 ⊢ 2 ∈ ℝ
2		2pos 12289	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12954	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2109  2c2 12241  ℝ⁺crp 12951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-2 12249  df-rp 12952

This theorem is referenced by:  rphalfcl  12980  ge2halflem1  13068  2tnp1ge0ge0  13791  flhalf  13792  fldiv4lem1div2uz2  13798  discr  14205  2swrd2eqwrdeq  14919  01sqrexlem7  15214  abstri  15297  amgm2  15336  iseralt  15651  climcndslem2  15816  climcnds  15817  efcllem  16043  oexpneg  16315  mod2eq1n2dvds  16317  oddge22np1  16319  evennn02n  16320  nn0ehalf  16348  nno  16352  nn0oddm1d2  16355  flodddiv4t2lthalf  16388  bitsfzolem  16404  bitsfzo  16405  bitsmod  16406  bitsinv1  16412  sadasslem  16440  sadeq  16442  oddprm  16781  iserodd  16806  prmreclem6  16892  prmgaplem7  17028  2expltfac  17063  psgnunilem4  19427  efgsfo  19669  efgredlemd  19674  efgredlem  19677  chfacfscmul0  22745  chfacfpmmul0  22749  psmetge0  24200  xmetge0  24232  metnrmlem3  24750  pcoass  24924  aaliou3lem1  26250  aaliou3lem2  26251  aaliou3lem3  26252  aaliou3lem8  26253  aaliou3lem5  26255  aaliou3lem6  26256  aaliou3lem7  26257  aaliou3lem9  26258  cos02pilt1  26435  cosordlem  26439  logi  26496  2irrexpq  26640  loglesqrt  26671  sqrt2cxp2logb9e3  26709  log2cnv  26854  log2ub  26859  log2le1  26860  birthday  26864  cxp2limlem  26886  divsqrtsumlem  26890  emcllem7  26912  emre  26916  emgt0  26917  harmonicbnd3  26918  zetacvg  26925  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamucov  26948  cht2  27082  cht3  27083  chtub  27123  bclbnd  27191  bposlem6  27200  bposlem7  27201  bposlem8  27202  bposlem9  27203  gausslemma2dlem1a  27276  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgslem3a1  27311  2lgslem3d1  27314  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  chto1ub  27387  chpo1ubb  27392  rplogsumlem1  27395  selbergb  27460  selberg2b  27463  chpdifbndlem2  27465  pntrsumbnd2  27478  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntpbnd  27499  pntibndlem2  27502  pntibndlem3  27503  pntibnd  27504  pntlemr  27513  nrt2irr  30402  nvge0  30602  nmcexi  31955  cshw1s2  32882  constrresqrtcl  33767  sqsscirc1  33898  dya2ub  34261  dya2iocress  34265  dya2iocbrsiga  34266  dya2icobrsiga  34267  dya2icoseg  34268  sxbrsigalem2  34277  omssubadd  34291  fiblem  34389  fibp1  34392  coinflipprob  34471  signstfveq0  34568  hgt750lemd  34639  logdivsqrle  34641  hgt750lem  34642  unbdqndv2  36499  knoppndvlem12  36511  knoppndvlem14  36513  knoppndvlem17  36516  knoppndvlem18  36517  taupilem1  37309  taupilem2  37310  taupi  37311  poimirlem29  37643  itg2addnclem  37665  ftc1anclem7  37693  ftc1anc  37695  isbnd2  37777  lcmineqlem21  42037  lcmineqlem23  42039  3lexlogpow2ineq1  42046  dvrelog2b  42054  dvrelogpow2b  42056  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p6  42069  2np3bcnp1  42132  2ap1caineq  42133  aks6d1c7lem1  42168  asin1half  42345  fltne  42632  flt4lem7  42647  proot1ex  43185  sqrtcvallem2  43626  sqrtcvallem4  43628  sqrtcval  43630  oddfl  45276  sumnnodd  45628  wallispilem3  46065  wallispilem4  46066  wallispi  46068  wallispi2lem1  46069  stirlinglem2  46073  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  stirlingr  46088  dirker2re  46090  dirkerdenne0  46091  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem10  46115  fourierdlem24  46129  fourierdlem62  46166  fourierdlem79  46183  fourierdlem87  46191  sqwvfoura  46226  sqwvfourb  46227  sge0ad2en  46429  ovnsubaddlem1  46568  hoiqssbllem1  46620  hoiqssbllem2  46621  hoiqssbllem3  46622  rehalfge1  47336  ceil5half3  47341  lighneallem3  47608  dfeven3  47659  dfodd4  47660  oexpnegALTV  47678  flnn0div2ge  48522  logbpw2m1  48556  fllog2  48557  blennnelnn  48565  nnpw2blen  48569  blen1b  48577  blennnt2  48578  nnolog2flm1  48579  blennngt2o2  48581  blennn0e2  48583  0dig2nn0e  48601  dignn0flhalflem1  48604  dignn0flhalflem2  48605