Theorem 2rp 13039

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 12332	. 2 ⊢ 2 ∈ ℝ
2		2pos 12362	. 2 ⊢ 0 < 2
3	1, 2	elrpii 13037	1 ⊢ 2 ∈ ℝ+

This proof depends on syntax axioms:   ∈ wcel 2146  2c2 12312  ℝ⁺crp 13034

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-nn 12251  df-2 12320  df-rp 13035

This theorem is used by:  rphalfcl  13063  ge2halflem1  13151  2tnp1ge0ge0  13882  flhalf  13883  fldiv4lem1div2uz2  13889  discr  14296  2swrd2eqwrdeq  15016  01sqrexlem7  15325  abstri  15408  amgm2  15447  iseralt  15762  climcndslem2  15929  climcnds  15930  efcllem  16155  oexpneg  16427  mod2eq1n2dvds  16429  oddge22np1  16431  evennn02n  16432  nn0ehalf  16460  nno  16464  nn0oddm1d2  16467  flodddiv4t2lthalf  16500  bitsfzolem  16516  bitsfzo  16517  bitsmod  16518  bitsinv1  16524  sadasslem  16552  sadeq  16554  oddprm  16894  iserodd  16919  prmreclem6  17005  prmgaplem7  17141  2expltfac  17176  psgnunilem4  19613  efgsfo  19855  efgredlemd  19860  efgredlem  19863  chfacfscmul0  23067  chfacfpmmul0  23071  psmetge0  24522  xmetge0  24554  metnrmlem3  25072  pcoass  25236  aaliou3lem1  26558  aaliou3lem2  26559  aaliou3lem3  26560  aaliou3lem8  26561  aaliou3lem5  26563  aaliou3lem6  26564  aaliou3lem7  26565  aaliou3lem9  26566  cos02pilt1  26744  cosordlem  26748  logi  26805  2irrexpq  26949  loglesqrt  26979  sqrt2cxp2logb9e3  27017  log2cnv  27162  log2ub  27167  log2le1  27168  birthday  27172  cxp2limlem  27193  divsqrtsumlem  27197  emcllem7  27219  emre  27223  emgt0  27224  harmonicbnd3  27225  zetacvg  27232  lgamgulmlem2  27247  lgamgulmlem3  27248  lgamucov  27255  cht2  27389  cht3  27390  chtub  27429  bclbnd  27497  bposlem6  27506  bposlem7  27507  bposlem8  27508  bposlem9  27509  gausslemma2dlem1a  27582  2lgslem3b  27614  2lgslem3c  27615  2lgslem3d  27616  2lgslem3a1  27617  2lgslem3d1  27620  chebbnd1lem2  27687  chebbnd1lem3  27688  chebbnd1  27689  chto1ub  27693  chpo1ubb  27698  rplogsumlem1  27701  selbergb  27766  selberg2b  27769  chpdifbndlem2  27771  pntrsumbnd2  27784  pntrlog2bndlem4  27797  pntrlog2bndlem5  27798  pntrlog2bndlem6  27800  pntrlog2bnd  27801  pntpbnd1a  27802  pntpbnd1  27803  pntpbnd2  27804  pntpbnd  27805  pntibndlem2  27808  pntibndlem3  27809  pntibnd  27810  pntlemr  27819  nrt2irr  30897  nvge0  31098  nmcexi  32451  cshw1s2  33346  constrresqrtcl  34233  sqsscirc1  34364  dya2ub  34727  dya2iocress  34731  dya2iocbrsiga  34732  dya2icobrsiga  34733  dya2icoseg  34734  sxbrsigalem2  34743  omssubadd  34757  fiblem  34855  fibp1  34858  coinflipprob  34937  signstfveq0  35031  hgt750lemd  35102  logdivsqrle  35104  hgt750lem  35105  unbdqndv2  37159  knoppndvlem12  37171  knoppndvlem14  37173  knoppndvlem17  37176  knoppndvlem18  37177  taupilem1  38024  taupilem2  38025  taupi  38026  poimirlem29  38359  itg2addnclem  38381  ftc1anclem7  38409  ftc1anc  38411  isbnd2  38494  lcmineqlem21  42876  lcmineqlem23  42878  3lexlogpow2ineq1  42885  dvrelog2b  42893  dvrelogpow2b  42895  aks4d1p1p2  42897  aks4d1p1p4  42898  aks4d1p1p6  42900  aks4d1p1p7  42901  aks4d1p1p5  42902  aks4d1p1  42903  aks4d1p6  42908  2np3bcnp1  42971  2ap1caineq  42972  aks6d1c7lem1  43007  asin1half  43178  fltne  43436  flt4lem7  43451  proot1ex  43983  sqrtcvallem2  44423  sqrtcvallem4  44425  sqrtcval  44427  oddfl  46057  sumnnodd  46406  wallispilem3  46841  wallispilem4  46842  wallispi  46844  wallispi2lem1  46845  stirlinglem2  46849  stirlinglem3  46850  stirlinglem4  46851  stirlinglem5  46852  stirlinglem6  46853  stirlinglem7  46854  stirlinglem10  46857  stirlinglem11  46858  stirlinglem13  46860  stirlinglem14  46861  stirlinglem15  46862  stirlingr  46864  dirker2re  46866  dirkerdenne0  46867  dirkerper  46870  dirkertrigeqlem1  46872  dirkertrigeqlem3  46874  dirkertrigeq  46875  dirkercncflem1  46877  dirkercncflem2  46878  dirkercncflem4  46880  fourierdlem10  46891  fourierdlem24  46905  fourierdlem62  46942  fourierdlem79  46959  fourierdlem87  46967  sqwvfoura  47002  sqwvfourb  47003  sge0ad2en  47205  ovnsubaddlem1  47344  hoiqssbllem1  47396  hoiqssbllem2  47397  hoiqssbllem3  47398  goldrapos  47680  rehalfge1  48136  ceil5half3  48143  lighneallem3  48419  dfeven3  48483  dfodd4  48484  oexpnegALTV  48502  flnn0div2ge  49372  logbpw2m1  49406  fllog2  49407  blennnelnn  49415  nnpw2blen  49419  blen1b  49427  blennnt2  49428  nnolog2flm1  49429  blennngt2o2  49431  blennn0e2  49433  0dig2nn0e  49451  dignn0flhalflem1  49454  dignn0flhalflem2  49455