Theorem 2rp 12895

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 12199	. 2 ⊢ 2 ∈ ℝ
2		2pos 12228	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12893	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2111  2c2 12180  ℝ⁺crp 12890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-2 12188  df-rp 12891

This theorem is referenced by:  rphalfcl  12919  ge2halflem1  13007  2tnp1ge0ge0  13733  flhalf  13734  fldiv4lem1div2uz2  13740  discr  14147  2swrd2eqwrdeq  14860  01sqrexlem7  15155  abstri  15238  amgm2  15277  iseralt  15592  climcndslem2  15757  climcnds  15758  efcllem  15984  oexpneg  16256  mod2eq1n2dvds  16258  oddge22np1  16260  evennn02n  16261  nn0ehalf  16289  nno  16293  nn0oddm1d2  16296  flodddiv4t2lthalf  16329  bitsfzolem  16345  bitsfzo  16346  bitsmod  16347  bitsinv1  16353  sadasslem  16381  sadeq  16383  oddprm  16722  iserodd  16747  prmreclem6  16833  prmgaplem7  16969  2expltfac  17004  psgnunilem4  19409  efgsfo  19651  efgredlemd  19656  efgredlem  19659  chfacfscmul0  22773  chfacfpmmul0  22777  psmetge0  24227  xmetge0  24259  metnrmlem3  24777  pcoass  24951  aaliou3lem1  26277  aaliou3lem2  26278  aaliou3lem3  26279  aaliou3lem8  26280  aaliou3lem5  26282  aaliou3lem6  26283  aaliou3lem7  26284  aaliou3lem9  26285  cos02pilt1  26462  cosordlem  26466  logi  26523  2irrexpq  26667  loglesqrt  26698  sqrt2cxp2logb9e3  26736  log2cnv  26881  log2ub  26886  log2le1  26887  birthday  26891  cxp2limlem  26913  divsqrtsumlem  26917  emcllem7  26939  emre  26943  emgt0  26944  harmonicbnd3  26945  zetacvg  26952  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamucov  26975  cht2  27109  cht3  27110  chtub  27150  bclbnd  27218  bposlem6  27227  bposlem7  27228  bposlem8  27229  bposlem9  27230  gausslemma2dlem1a  27303  2lgslem3b  27335  2lgslem3c  27336  2lgslem3d  27337  2lgslem3a1  27338  2lgslem3d1  27341  chebbnd1lem2  27408  chebbnd1lem3  27409  chebbnd1  27410  chto1ub  27414  chpo1ubb  27419  rplogsumlem1  27422  selbergb  27487  selberg2b  27490  chpdifbndlem2  27492  pntrsumbnd2  27505  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntrlog2bnd  27522  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntpbnd  27526  pntibndlem2  27529  pntibndlem3  27530  pntibnd  27531  pntlemr  27540  nrt2irr  30453  nvge0  30653  nmcexi  32006  cshw1s2  32941  constrresqrtcl  33790  sqsscirc1  33921  dya2ub  34283  dya2iocress  34287  dya2iocbrsiga  34288  dya2icobrsiga  34289  dya2icoseg  34290  sxbrsigalem2  34299  omssubadd  34313  fiblem  34411  fibp1  34414  coinflipprob  34493  signstfveq0  34590  hgt750lemd  34661  logdivsqrle  34663  hgt750lem  34664  unbdqndv2  36555  knoppndvlem12  36567  knoppndvlem14  36569  knoppndvlem17  36572  knoppndvlem18  36573  taupilem1  37365  taupilem2  37366  taupi  37367  poimirlem29  37699  itg2addnclem  37721  ftc1anclem7  37749  ftc1anc  37751  isbnd2  37833  lcmineqlem21  42152  lcmineqlem23  42154  3lexlogpow2ineq1  42161  dvrelog2b  42169  dvrelogpow2b  42171  aks4d1p1p2  42173  aks4d1p1p4  42174  aks4d1p1p6  42176  aks4d1p1p7  42177  aks4d1p1p5  42178  aks4d1p1  42179  aks4d1p6  42184  2np3bcnp1  42247  2ap1caineq  42248  aks6d1c7lem1  42283  asin1half  42460  fltne  42747  flt4lem7  42762  proot1ex  43299  sqrtcvallem2  43740  sqrtcvallem4  43742  sqrtcval  43744  oddfl  45389  sumnnodd  45740  wallispilem3  46175  wallispilem4  46176  wallispi  46178  wallispi2lem1  46179  stirlinglem2  46183  stirlinglem3  46184  stirlinglem4  46185  stirlinglem5  46186  stirlinglem6  46187  stirlinglem7  46188  stirlinglem10  46191  stirlinglem11  46192  stirlinglem13  46194  stirlinglem14  46195  stirlinglem15  46196  stirlingr  46198  dirker2re  46200  dirkerdenne0  46201  dirkerper  46204  dirkertrigeqlem1  46206  dirkertrigeqlem3  46208  dirkertrigeq  46209  dirkercncflem1  46211  dirkercncflem2  46212  dirkercncflem4  46214  fourierdlem10  46225  fourierdlem24  46239  fourierdlem62  46276  fourierdlem79  46293  fourierdlem87  46301  sqwvfoura  46336  sqwvfourb  46337  sge0ad2en  46539  ovnsubaddlem1  46678  hoiqssbllem1  46730  hoiqssbllem2  46731  hoiqssbllem3  46732  rehalfge1  47445  ceil5half3  47450  lighneallem3  47717  dfeven3  47768  dfodd4  47769  oexpnegALTV  47787  flnn0div2ge  48644  logbpw2m1  48678  fllog2  48679  blennnelnn  48687  nnpw2blen  48691  blen1b  48699  blennnt2  48700  nnolog2flm1  48701  blennngt2o2  48703  blennn0e2  48705  0dig2nn0e  48723  dignn0flhalflem1  48726  dignn0flhalflem2  48727