Theorem 2rp 13050

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 12342	. 2 ⊢ 2 ∈ ℝ
2		2pos 12372	. 2 ⊢ 0 < 2
3	1, 2	elrpii 13048	1 ⊢ 2 ∈ ℝ+

This proof depends on syntax axioms:   ∈ wcel 2145  2c2 12322  ℝ⁺crp 13045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-nn 12261  df-2 12330  df-rp 13046

This theorem is used by:  rphalfcl  13074  ge2halflem1  13162  2tnp1ge0ge0  13893  flhalf  13894  fldiv4lem1div2uz2  13900  discr  14307  2swrd2eqwrdeq  15029  01sqrexlem7  15338  abstri  15421  amgm2  15460  iseralt  15775  climcndslem2  15942  climcnds  15943  efcllem  16166  oexpneg  16438  mod2eq1n2dvds  16440  oddge22np1  16442  evennn02n  16443  nn0ehalf  16471  nno  16475  nn0oddm1d2  16478  flodddiv4t2lthalf  16511  bitsfzolem  16527  bitsfzo  16528  bitsmod  16529  bitsinv1  16535  sadasslem  16563  sadeq  16565  oddprm  16905  iserodd  16930  prmreclem6  17016  prmgaplem7  17152  2expltfac  17187  psgnunilem4  19627  efgsfo  19869  efgredlemd  19874  efgredlem  19877  chfacfscmul0  23086  chfacfpmmul0  23090  psmetge0  24541  xmetge0  24573  metnrmlem3  25091  pcoass  25255  aaliou3lem1  26581  aaliou3lem2  26582  aaliou3lem3  26583  aaliou3lem8  26584  aaliou3lem5  26586  aaliou3lem6  26587  aaliou3lem7  26588  aaliou3lem9  26589  cos02pilt1  26766  cosordlem  26770  logi  26827  2irrexpq  26971  loglesqrt  27001  sqrt2cxp2logb9e3  27039  log2cnv  27184  log2ub  27189  log2le1  27190  birthday  27194  cxp2limlem  27215  divsqrtsumlem  27219  emcllem7  27241  emre  27245  emgt0  27246  harmonicbnd3  27247  zetacvg  27254  lgamgulmlem2  27269  lgamgulmlem3  27270  lgamucov  27277  cht2  27411  cht3  27412  chtub  27451  bclbnd  27519  bposlem6  27528  bposlem7  27529  bposlem8  27530  bposlem9  27531  gausslemma2dlem1a  27604  2lgslem3b  27636  2lgslem3c  27637  2lgslem3d  27638  2lgslem3a1  27639  2lgslem3d1  27642  chebbnd1lem2  27709  chebbnd1lem3  27710  chebbnd1  27711  chto1ub  27715  chpo1ubb  27720  rplogsumlem1  27723  selbergb  27788  selberg2b  27791  chpdifbndlem2  27793  pntrsumbnd2  27806  pntrlog2bndlem4  27819  pntrlog2bndlem5  27820  pntrlog2bndlem6  27822  pntrlog2bnd  27823  pntpbnd1a  27824  pntpbnd1  27825  pntpbnd2  27826  pntpbnd  27827  pntibndlem2  27830  pntibndlem3  27831  pntibnd  27832  pntlemr  27841  nrt2irr  30956  nvge0  31157  nmcexi  32510  cshw1s2  33403  constrresqrtcl  34290  sqsscirc1  34421  dya2ub  34784  dya2iocress  34788  dya2iocbrsiga  34789  dya2icobrsiga  34790  dya2icoseg  34791  sxbrsigalem2  34800  omssubadd  34814  fiblem  34912  fibp1  34915  coinflipprob  34994  signstfveq0  35088  hgt750lemd  35159  logdivsqrle  35161  hgt750lem  35162  unbdqndv2  37211  knoppndvlem12  37223  knoppndvlem14  37225  knoppndvlem17  37228  knoppndvlem18  37229  taupilem1  38076  taupilem2  38077  taupi  38078  poimirlem29  38401  itg2addnclem  38423  ftc1anclem7  38451  ftc1anc  38453  isbnd2  38536  lcmineqlem21  42918  lcmineqlem23  42920  3lexlogpow2ineq1  42927  dvrelog2b  42935  dvrelogpow2b  42937  aks4d1p1p2  42939  aks4d1p1p4  42940  aks4d1p1p6  42942  aks4d1p1p7  42943  aks4d1p1p5  42944  aks4d1p1  42945  aks4d1p6  42950  2np3bcnp1  43013  2ap1caineq  43014  aks6d1c7lem1  43049  asin1half  43235  fltne  43493  flt4lem7  43508  proot1ex  44040  sqrtcvallem2  44480  sqrtcvallem4  44482  sqrtcval  44484  oddfl  46114  sumnnodd  46463  wallispilem3  46898  wallispilem4  46899  wallispi  46901  wallispi2lem1  46902  stirlinglem2  46906  stirlinglem3  46907  stirlinglem4  46908  stirlinglem5  46909  stirlinglem6  46910  stirlinglem7  46911  stirlinglem10  46914  stirlinglem11  46915  stirlinglem13  46917  stirlinglem14  46918  stirlinglem15  46919  stirlingr  46921  dirker2re  46923  dirkerdenne0  46924  dirkerper  46927  dirkertrigeqlem1  46929  dirkertrigeqlem3  46931  dirkertrigeq  46932  dirkercncflem1  46934  dirkercncflem2  46935  dirkercncflem4  46937  fourierdlem10  46948  fourierdlem24  46962  fourierdlem62  46999  fourierdlem79  47016  fourierdlem87  47024  sqwvfoura  47059  sqwvfourb  47060  sge0ad2en  47262  ovnsubaddlem1  47401  hoiqssbllem1  47453  hoiqssbllem2  47454  hoiqssbllem3  47455  goldrapos  47751  rehalfge1  48230  ceil5half3  48237  lighneallem3  48513  dfeven3  48577  dfodd4  48578  oexpnegALTV  48596  flnn0div2ge  49466  logbpw2m1  49500  fllog2  49501  blennnelnn  49509  nnpw2blen  49513  blen1b  49521  blennnt2  49522  nnolog2flm1  49523  blennngt2o2  49525  blennn0e2  49527  0dig2nn0e  49545  dignn0flhalflem1  49548  dignn0flhalflem2  49549