Theorem 2rp 12142

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 11449	. 2 ⊢ 2 ∈ ℝ
2		2pos 11485	. 2 ⊢ 0 < 2
3	1, 2	elrpii 12140	1 ⊢ 2 ∈ ℝ+

Syntax hints:   ∈ wcel 2106  2c2 11430  ℝ⁺crp 12137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-2 11438  df-rp 12138

This theorem is referenced by:  rphalfcl  12166  2tnp1ge0ge0  12949  flhalf  12950  fldiv4lem1div2uz2  12956  discr  13320  2swrd2eqwrdeq  14104  2swrd2eqwrdeqOLD  14105  sqrlem7  14396  abstri  14477  amgm2  14516  iseralt  14823  climcndslem2  14986  climcnds  14987  efcllem  15210  oexpneg  15473  mod2eq1n2dvds  15475  oddge22np1  15477  evennn02n  15478  nn0ehalf  15508  nno  15512  nn0oddm1d2  15515  flodddiv4t2lthalf  15546  bitsfzolem  15562  bitsfzo  15563  bitsmod  15564  bitsinv1  15570  sadasslem  15598  sadeq  15600  oddprm  15919  iserodd  15944  prmreclem6  16029  prmgaplem7  16165  2expltfac  16198  psgnunilem4  18301  efgsfo  18537  efgredlemd  18542  efgredlem  18545  efgredlemOLD  18546  chfacfscmul0  21070  chfacfpmmul0  21074  psmetge0  22525  xmetge0  22557  metnrmlem3  23072  pcoass  23231  aaliou3lem1  24534  aaliou3lem2  24535  aaliou3lem3  24536  aaliou3lem8  24537  aaliou3lem5  24539  aaliou3lem6  24540  aaliou3lem7  24541  aaliou3lem9  24542  2irrexpq  24913  loglesqrt  24939  sqrt2cxp2logb9e3  24977  log2cnv  25123  log2ub  25128  log2le1  25129  birthday  25133  cxp2limlem  25154  divsqrtsumlem  25158  emcllem7  25180  emre  25184  emgt0  25185  harmonicbnd3  25186  zetacvg  25193  lgamgulmlem2  25208  lgamgulmlem3  25209  lgamucov  25216  cht2  25350  cht3  25351  chtub  25389  bclbnd  25457  bposlem6  25466  bposlem7  25467  bposlem8  25468  bposlem9  25469  gausslemma2dlem1a  25542  2lgslem3b  25574  2lgslem3c  25575  2lgslem3d  25576  2lgslem3a1  25577  2lgslem3d1  25580  chebbnd1lem2  25611  chebbnd1lem3  25612  chebbnd1  25613  chto1ub  25617  chpo1ubb  25622  rplogsumlem1  25625  selbergb  25690  selberg2b  25693  chpdifbndlem2  25695  pntrsumbnd2  25708  pntrlog2bndlem4  25721  pntrlog2bndlem5  25722  pntrlog2bndlem6  25724  pntrlog2bnd  25725  pntpbnd1a  25726  pntpbnd1  25727  pntpbnd2  25728  pntpbnd  25729  pntibndlem2  25732  pntibndlem3  25733  pntibnd  25734  pntlemr  25743  nvge0  28100  nmcexi  29457  sqsscirc1  30552  dya2ub  30930  dya2iocress  30934  dya2iocbrsiga  30935  dya2icobrsiga  30936  dya2icoseg  30937  sxbrsigalem2  30946  omssubadd  30960  fiblem  31059  fibp1  31062  coinflipprob  31140  signstfveq0  31255  signstfveq0OLD  31256  hgt750lemd  31328  logdivsqrle  31330  hgt750lem  31331  logi  32214  unbdqndv2  33084  knoppndvlem12  33096  knoppndvlem14  33098  knoppndvlem17  33101  knoppndvlem18  33102  taupilem1  33763  taupilem2  33764  taupi  33765  poimirlem29  34048  itg2addnclem  34070  ftc1anclem7  34100  ftc1anc  34102  isbnd2  34190  proot1ex  38720  oddfl  40381  sumnnodd  40752  wallispilem3  41193  wallispilem4  41194  wallispi  41196  wallispi2lem1  41197  stirlinglem2  41201  stirlinglem3  41202  stirlinglem4  41203  stirlinglem5  41204  stirlinglem6  41205  stirlinglem7  41206  stirlinglem10  41209  stirlinglem11  41210  stirlinglem13  41212  stirlinglem14  41213  stirlinglem15  41214  stirlingr  41216  dirker2re  41218  dirkerdenne0  41219  dirkerper  41222  dirkertrigeqlem1  41224  dirkertrigeqlem3  41226  dirkertrigeq  41227  dirkercncflem1  41229  dirkercncflem2  41230  dirkercncflem4  41232  fourierdlem10  41243  fourierdlem24  41257  fourierdlem62  41294  fourierdlem79  41311  fourierdlem87  41319  sqwvfoura  41354  sqwvfourb  41355  sge0ad2en  41554  ovnsubaddlem1  41693  hoiqssbllem1  41745  hoiqssbllem2  41746  hoiqssbllem3  41747  lighneallem3  42527  dfeven3  42577  dfodd4  42578  oexpnegALTV  42595  flnn0div2ge  43324  logbpw2m1  43358  fllog2  43359  blennnelnn  43367  nnpw2blen  43371  blen1b  43379  blennnt2  43380  nnolog2flm1  43381  blennngt2o2  43383  blennn0e2  43385  0dig2nn0e  43403  dignn0flhalflem1  43406  dignn0flhalflem2  43407