Theorem 2rp 11837

Description: 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Assertion

Ref	Expression
2rp	|- 2 e. RR+

Proof of Theorem 2rp

Step	Hyp	Ref	Expression
1		2re 11090	. 2 |- 2 e. RR
2		2pos 11112	. 2 |- 0 < 2
3	1, 2	elrpii 11835	1 |- 2 e. RR+

Syntax hints:   e. wcel 1990   2c2 11070   RR+crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-2 11079  df-rp 11833

This theorem is referenced by:  rphalfcl  11858  flhalf  12631  fldiv4lem1div2uz2  12637  discr  13001  abstri  14070  mod2eq1n2dvds  15071  bitsfzolem  15156  bitsfzo  15157  bitsmod  15158  bitsinv1  15164  sadasslem  15192  sadeq  15194  prmreclem6  15625  2expltfac  15799  psgnunilem4  17917  efgsfo  18152  efgredlemd  18157  efgredlem  18160  chfacfscmul0  20663  chfacfpmmul0  20667  psmetge0  22117  xmetge0  22149  metnrmlem3  22664  pcoass  22824  aaliou3lem1  24097  aaliou3lem2  24098  aaliou3lem3  24099  aaliou3lem8  24100  aaliou3lem5  24102  aaliou3lem6  24103  aaliou3lem7  24104  aaliou3lem9  24105  loglesqrt  24499  log2cnv  24671  log2ub  24676  log2le1  24677  birthday  24681  cxp2limlem  24702  divsqrtsumlem  24706  emcllem7  24728  emre  24732  emgt0  24733  harmonicbnd3  24734  zetacvg  24741  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamucov  24764  cht2  24898  cht3  24899  chtub  24937  bclbnd  25005  bposlem6  25014  bposlem7  25015  bposlem8  25016  bposlem9  25017  gausslemma2dlem1a  25090  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2lgslem3a1  25125  2lgslem3d1  25128  chebbnd1lem2  25159  chebbnd1lem3  25160  chebbnd1  25161  chto1ub  25165  chpo1ubb  25170  rplogsumlem1  25173  selbergb  25238  selberg2b  25241  chpdifbndlem2  25243  pntrsumbnd2  25256  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntpbnd  25277  pntibndlem2  25280  pntibndlem3  25281  pntibnd  25282  pntlemr  25291  nmcexi  28885  sqsscirc1  29954  dya2ub  30332  dya2iocress  30336  dya2iocbrsiga  30337  dya2icobrsiga  30338  dya2icoseg  30339  sxbrsigalem2  30348  omssubadd  30362  fiblem  30460  fibp1  30463  coinflipprob  30541  signstfveq0  30654  hgt750lemd  30726  logdivsqrle  30728  hgt750lem  30729  logi  31620  unbdqndv2  32502  knoppndvlem12  32514  knoppndvlem14  32516  knoppndvlem17  32519  knoppndvlem18  32520  taupilem1  33167  taupilem2  33168  taupi  33169  poimirlem29  33438  itg2addnclem  33461  ftc1anclem7  33491  ftc1anc  33493  isbnd2  33582  proot1ex  37779  oddfl  39489  sumnnodd  39862  wallispilem3  40284  wallispilem4  40285  wallispi  40287  wallispi2lem1  40288  stirlinglem2  40292  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  stirlinglem11  40301  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  stirlingr  40307  dirker2re  40309  dirkerdenne0  40310  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem10  40334  fourierdlem24  40348  fourierdlem62  40385  fourierdlem79  40402  fourierdlem87  40410  sqwvfoura  40445  sqwvfourb  40446  sge0ad2en  40648  ovnsubaddlem1  40784  hoiqssbllem1  40836  hoiqssbllem2  40837  hoiqssbllem3  40838  lighneallem3  41524  dfeven3  41570  dfodd4  41571  flnn0div2ge  42327  logbpw2m1  42361  fllog2  42362  blennnelnn  42370  nnpw2blen  42374  blen1b  42382  blennnt2  42383  nnolog2flm1  42384  blennngt2o2  42386  blennn0e2  42388  0dig2nn0e  42406  dignn0flhalflem1  42409  dignn0flhalflem2  42410