Theorem 2rp 13125

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 12417	. 2 ⊢ 2 ∈ ℝ
2		2pos 12447	. 2 ⊢ 0 < 2
3	1, 2	elrpii 13123	1 ⊢ 2 ∈ ℝ+

This proof depends on syntax axioms:   ∈ wcel 2145  2c2 12397  ℝ⁺crp 13120

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 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  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 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-2 12405  df-rp 13121

This theorem is used by:  rphalfcl  13149  ge2halflem1  13237  2tnp1ge0ge0  13969  flhalf  13970  fldiv4lem1div2uz2  13976  discr  14384  2swrd2eqwrdeq  15106  01sqrexlem7  15415  abstri  15498  amgm2  15537  iseralt  15852  climcndslem2  16019  climcnds  16020  efcllem  16243  oexpneg  16515  mod2eq1n2dvds  16517  oddge22np1  16519  evennn02n  16520  nn0ehalf  16548  nno  16552  nn0oddm1d2  16555  flodddiv4t2lthalf  16588  bitsfzolem  16604  bitsfzo  16605  bitsmod  16606  bitsinv1  16612  sadasslem  16640  sadeq  16642  oddprm  16988  iserodd  17013  prmreclem6  17099  prmgaplem7  17235  2expltfac  17270  psgnunilem4  19711  efgsfo  19953  efgredlemd  19958  efgredlem  19961  chfacfscmul0  23176  chfacfpmmul0  23180  psmetge0  24631  xmetge0  24663  metnrmlem3  25181  pcoass  25345  aaliou3lem1  26669  aaliou3lem2  26670  aaliou3lem3  26671  aaliou3lem8  26672  aaliou3lem5  26674  aaliou3lem6  26675  aaliou3lem7  26676  aaliou3lem9  26677  cos02pilt1  26854  cosordlem  26858  logi  26915  2irrexpq  27059  loglesqrt  27089  sqrt2cxp2logb9e3  27127  log2cnv  27272  log2ub  27277  log2le1  27278  birthday  27282  cxp2limlem  27303  divsqrtsumlem  27307  emcllem7  27329  emre  27333  emgt0  27334  harmonicbnd3  27335  zetacvg  27342  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamucov  27365  cht2  27499  cht3  27500  chtub  27539  bclbnd  27607  bposlem6  27616  bposlem7  27617  bposlem8  27618  bposlem9  27619  gausslemma2dlem1a  27692  2lgslem3b  27724  2lgslem3c  27725  2lgslem3d  27726  2lgslem3a1  27727  2lgslem3d1  27730  chebbnd1lem2  27797  chebbnd1lem3  27798  chebbnd1  27799  chto1ub  27803  chpo1ubb  27808  rplogsumlem1  27811  selbergb  27876  selberg2b  27879  chpdifbndlem2  27881  pntrsumbnd2  27894  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntrlog2bndlem6  27910  pntrlog2bnd  27911  pntpbnd1a  27912  pntpbnd1  27913  pntpbnd2  27914  pntpbnd  27915  pntibndlem2  27918  pntibndlem3  27919  pntibnd  27920  pntlemr  27929  fltne  27975  flt4lem7  27989  nrt2irr  31074  nvge0  31275  nmcexi  32628  cshw1s2  33521  constrresqrtcl  34409  sqsscirc1  34540  dya2ub  34902  dya2iocress  34906  dya2iocbrsiga  34907  dya2icobrsiga  34908  dya2icoseg  34909  sxbrsigalem2  34918  omssubadd  34932  fiblem  35030  fibp1  35033  coinflipprob  35112  signstfveq0  35206  hgt750lemd  35277  logdivsqrle  35279  hgt750lem  35280  unbdqndv2  37377  knoppndvlem12  37389  knoppndvlem14  37391  knoppndvlem17  37394  knoppndvlem18  37395  taupilem1  38242  taupilem2  38243  taupi  38244  poimirlem29  38567  itg2addnclem  38589  ftc1anclem7  38617  ftc1anc  38619  isbnd2  38717  lcmineqlem21  43099  lcmineqlem23  43101  3lexlogpow2ineq1  43108  dvrelog2b  43116  dvrelogpow2b  43118  aks4d1p1p2  43120  aks4d1p1p4  43121  aks4d1p1p6  43123  aks4d1p1p7  43124  aks4d1p1p5  43125  aks4d1p1  43126  aks4d1p6  43131  2np3bcnp1  43194  2ap1caineq  43195  aks6d1c7lem1  43230  asin1half  43408  proot1ex  44197  sqrtcvallem2  44636  sqrtcvallem4  44638  sqrtcval  44640  oddfl  46293  sumnnodd  46641  wallispilem3  47076  wallispilem4  47077  wallispi  47079  wallispi2lem1  47080  stirlinglem2  47084  stirlinglem3  47085  stirlinglem4  47086  stirlinglem5  47087  stirlinglem6  47088  stirlinglem7  47089  stirlinglem10  47092  stirlinglem11  47093  stirlinglem13  47095  stirlinglem14  47096  stirlinglem15  47097  stirlingr  47099  dirker2re  47101  dirkerdenne0  47102  dirkerper  47105  dirkertrigeqlem1  47107  dirkertrigeqlem3  47109  dirkertrigeq  47110  dirkercncflem1  47112  dirkercncflem2  47113  dirkercncflem4  47115  fourierdlem10  47126  fourierdlem24  47140  fourierdlem62  47177  fourierdlem79  47194  fourierdlem87  47202  sqwvfoura  47237  sqwvfourb  47238  sge0ad2en  47440  ovnsubaddlem1  47579  hoiqssbllem1  47631  hoiqssbllem2  47632  hoiqssbllem3  47633  goldrapos  47929  rehalfge1  48408  ceil5half3  48415  lighneallem3  48691  dfeven3  48755  dfodd4  48756  oexpnegALTV  48774  flnn0div2ge  49644  logbpw2m1  49678  fllog2  49679  blennnelnn  49687  nnpw2blen  49691  blen1b  49699  blennnt2  49700  nnolog2flm1  49701  blennngt2o2  49703  blennn0e2  49705  0dig2nn0e  49723  dignn0flhalflem1  49726  dignn0flhalflem2  49727