MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2rp Structured version   Visualization version   GIF version

Theorem 2rp 12371
Description: 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
Assertion
Ref Expression
2rp 2 ∈ ℝ+

Proof of Theorem 2rp
StepHypRef Expression
1 2re 11688 . 2 2 ∈ ℝ
2 2pos 11717 . 2 0 < 2
31, 2elrpii 12369 1 2 ∈ ℝ+
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  2c2 11669  +crp 12366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5177  ax-nul 5184  ax-pow 5240  ax-pr 5304  ax-un 7437  ax-resscn 10570  ax-1cn 10571  ax-icn 10572  ax-addcl 10573  ax-addrcl 10574  ax-mulcl 10575  ax-mulrcl 10576  ax-mulcom 10577  ax-addass 10578  ax-mulass 10579  ax-distr 10580  ax-i2m1 10581  ax-1ne0 10582  ax-1rid 10583  ax-rnegex 10584  ax-rrecex 10585  ax-cnre 10586  ax-pre-lttri 10587  ax-pre-lttrn 10588  ax-pre-ltadd 10589  ax-pre-mulgt0 10590
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rab 3134  df-v 3475  df-sbc 3752  df-csb 3860  df-dif 3915  df-un 3917  df-in 3919  df-ss 3928  df-nul 4268  df-if 4442  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4813  df-br 5041  df-opab 5103  df-mpt 5121  df-id 5434  df-po 5448  df-so 5449  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-riota 7089  df-ov 7134  df-oprab 7135  df-mpo 7136  df-er 8265  df-en 8486  df-dom 8487  df-sdom 8488  df-pnf 10653  df-mnf 10654  df-xr 10655  df-ltxr 10656  df-le 10657  df-sub 10848  df-neg 10849  df-2 11677  df-rp 12367
This theorem is referenced by:  rphalfcl  12393  2tnp1ge0ge0  13181  flhalf  13182  fldiv4lem1div2uz2  13188  discr  13584  2swrd2eqwrdeq  14293  sqrlem7  14586  abstri  14668  amgm2  14707  iseralt  15019  climcndslem2  15183  climcnds  15184  efcllem  15409  oexpneg  15672  mod2eq1n2dvds  15674  oddge22np1  15676  evennn02n  15677  nn0ehalf  15705  nno  15709  nn0oddm1d2  15712  flodddiv4t2lthalf  15743  bitsfzolem  15759  bitsfzo  15760  bitsmod  15761  bitsinv1  15767  sadasslem  15795  sadeq  15797  oddprm  16123  iserodd  16148  prmreclem6  16233  prmgaplem7  16369  2expltfac  16402  psgnunilem4  18601  efgsfo  18841  efgredlemd  18846  efgredlem  18849  chfacfscmul0  21439  chfacfpmmul0  21443  psmetge0  22895  xmetge0  22927  metnrmlem3  23442  pcoass  23605  aaliou3lem1  24914  aaliou3lem2  24915  aaliou3lem3  24916  aaliou3lem8  24917  aaliou3lem5  24919  aaliou3lem6  24920  aaliou3lem7  24921  aaliou3lem9  24922  cos02pilt1  25094  cosordlem  25098  2irrexpq  25297  loglesqrt  25323  sqrt2cxp2logb9e3  25361  log2cnv  25506  log2ub  25511  log2le1  25512  birthday  25516  cxp2limlem  25537  divsqrtsumlem  25541  emcllem7  25563  emre  25567  emgt0  25568  harmonicbnd3  25569  zetacvg  25576  lgamgulmlem2  25591  lgamgulmlem3  25592  lgamucov  25599  cht2  25733  cht3  25734  chtub  25772  bclbnd  25840  bposlem6  25849  bposlem7  25850  bposlem8  25851  bposlem9  25852  gausslemma2dlem1a  25925  2lgslem3b  25957  2lgslem3c  25958  2lgslem3d  25959  2lgslem3a1  25960  2lgslem3d1  25963  chebbnd1lem2  26030  chebbnd1lem3  26031  chebbnd1  26032  chto1ub  26036  chpo1ubb  26041  rplogsumlem1  26044  selbergb  26109  selberg2b  26112  chpdifbndlem2  26114  pntrsumbnd2  26127  pntrlog2bndlem4  26140  pntrlog2bndlem5  26141  pntrlog2bndlem6  26143  pntrlog2bnd  26144  pntpbnd1a  26145  pntpbnd1  26146  pntpbnd2  26147  pntpbnd  26148  pntibndlem2  26151  pntibndlem3  26152  pntibnd  26153  pntlemr  26162  nvge0  28432  nmcexi  29785  cshw1s2  30618  sqsscirc1  31156  dya2ub  31533  dya2iocress  31537  dya2iocbrsiga  31538  dya2icobrsiga  31539  dya2icoseg  31540  sxbrsigalem2  31549  omssubadd  31563  fiblem  31661  fibp1  31664  coinflipprob  31742  signstfveq0  31852  hgt750lemd  31924  logdivsqrle  31926  hgt750lem  31927  logi  32971  unbdqndv2  33855  knoppndvlem12  33867  knoppndvlem14  33869  knoppndvlem17  33872  knoppndvlem18  33873  taupilem1  34616  taupilem2  34617  taupi  34618  poimirlem29  34959  itg2addnclem  34981  ftc1anclem7  35009  ftc1anc  35011  isbnd2  35094  lcmineqlem21  39190  lcmineqlem23  39192  fltne  39396  proot1ex  39925  oddfl  41684  sumnnodd  42050  wallispilem3  42487  wallispilem4  42488  wallispi  42490  wallispi2lem1  42491  stirlinglem2  42495  stirlinglem3  42496  stirlinglem4  42497  stirlinglem5  42498  stirlinglem6  42499  stirlinglem7  42500  stirlinglem10  42503  stirlinglem11  42504  stirlinglem13  42506  stirlinglem14  42507  stirlinglem15  42508  stirlingr  42510  dirker2re  42512  dirkerdenne0  42513  dirkerper  42516  dirkertrigeqlem1  42518  dirkertrigeqlem3  42520  dirkertrigeq  42521  dirkercncflem1  42523  dirkercncflem2  42524  dirkercncflem4  42526  fourierdlem10  42537  fourierdlem24  42551  fourierdlem62  42588  fourierdlem79  42605  fourierdlem87  42613  sqwvfoura  42648  sqwvfourb  42649  sge0ad2en  42848  ovnsubaddlem1  42987  hoiqssbllem1  43039  hoiqssbllem2  43040  hoiqssbllem3  43041  lighneallem3  43902  dfeven3  43953  dfodd4  43954  oexpnegALTV  43972  flnn0div2ge  44723  logbpw2m1  44757  fllog2  44758  blennnelnn  44766  nnpw2blen  44770  blen1b  44778  blennnt2  44779  nnolog2flm1  44780  blennngt2o2  44782  blennn0e2  44784  0dig2nn0e  44802  dignn0flhalflem1  44805  dignn0flhalflem2  44806
  Copyright terms: Public domain W3C validator