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

Theorem 2rp 12384
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 11700 . 2 2 ∈ ℝ
2 2pos 11729 . 2 0 < 2
31, 2elrpii 12382 1 2 ∈ ℝ+
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  2c2 11681  +crp 12379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-po 5468  df-so 5469  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-2 11689  df-rp 12380
This theorem is referenced by:  rphalfcl  12406  2tnp1ge0ge0  13189  flhalf  13190  fldiv4lem1div2uz2  13196  discr  13591  2swrd2eqwrdeq  14305  sqrlem7  14598  abstri  14680  amgm2  14719  iseralt  15031  climcndslem2  15195  climcnds  15196  efcllem  15421  oexpneg  15684  mod2eq1n2dvds  15686  oddge22np1  15688  evennn02n  15689  nn0ehalf  15719  nno  15723  nn0oddm1d2  15726  flodddiv4t2lthalf  15757  bitsfzolem  15773  bitsfzo  15774  bitsmod  15775  bitsinv1  15781  sadasslem  15809  sadeq  15811  oddprm  16137  iserodd  16162  prmreclem6  16247  prmgaplem7  16383  2expltfac  16416  psgnunilem4  18556  efgsfo  18796  efgredlemd  18801  efgredlem  18804  chfacfscmul0  21396  chfacfpmmul0  21400  psmetge0  22851  xmetge0  22883  metnrmlem3  23398  pcoass  23557  aaliou3lem1  24860  aaliou3lem2  24861  aaliou3lem3  24862  aaliou3lem8  24863  aaliou3lem5  24865  aaliou3lem6  24866  aaliou3lem7  24867  aaliou3lem9  24868  cosordlem  25042  2irrexpq  25240  loglesqrt  25266  sqrt2cxp2logb9e3  25304  log2cnv  25450  log2ub  25455  log2le1  25456  birthday  25460  cxp2limlem  25481  divsqrtsumlem  25485  emcllem7  25507  emre  25511  emgt0  25512  harmonicbnd3  25513  zetacvg  25520  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamucov  25543  cht2  25677  cht3  25678  chtub  25716  bclbnd  25784  bposlem6  25793  bposlem7  25794  bposlem8  25795  bposlem9  25796  gausslemma2dlem1a  25869  2lgslem3b  25901  2lgslem3c  25902  2lgslem3d  25903  2lgslem3a1  25904  2lgslem3d1  25907  chebbnd1lem2  25974  chebbnd1lem3  25975  chebbnd1  25976  chto1ub  25980  chpo1ubb  25985  rplogsumlem1  25988  selbergb  26053  selberg2b  26056  chpdifbndlem2  26058  pntrsumbnd2  26071  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntrlog2bnd  26088  pntpbnd1a  26089  pntpbnd1  26090  pntpbnd2  26091  pntpbnd  26092  pntibndlem2  26095  pntibndlem3  26096  pntibnd  26097  pntlemr  26106  nvge0  28378  nmcexi  29731  cshw1s2  30562  sqsscirc1  31051  dya2ub  31428  dya2iocress  31432  dya2iocbrsiga  31433  dya2icobrsiga  31434  dya2icoseg  31435  sxbrsigalem2  31444  omssubadd  31458  fiblem  31556  fibp1  31559  coinflipprob  31637  signstfveq0  31747  hgt750lemd  31819  logdivsqrle  31821  hgt750lem  31822  logi  32864  unbdqndv2  33748  knoppndvlem12  33760  knoppndvlem14  33762  knoppndvlem17  33765  knoppndvlem18  33766  taupilem1  34485  taupilem2  34486  taupi  34487  poimirlem29  34803  itg2addnclem  34825  ftc1anclem7  34855  ftc1anc  34857  isbnd2  34944  fltne  39152  proot1ex  39681  oddfl  41423  sumnnodd  41791  wallispilem3  42233  wallispilem4  42234  wallispi  42236  wallispi2lem1  42237  stirlinglem2  42241  stirlinglem3  42242  stirlinglem4  42243  stirlinglem5  42244  stirlinglem6  42245  stirlinglem7  42246  stirlinglem10  42249  stirlinglem11  42250  stirlinglem13  42252  stirlinglem14  42253  stirlinglem15  42254  stirlingr  42256  dirker2re  42258  dirkerdenne0  42259  dirkerper  42262  dirkertrigeqlem1  42264  dirkertrigeqlem3  42266  dirkertrigeq  42267  dirkercncflem1  42269  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem10  42283  fourierdlem24  42297  fourierdlem62  42334  fourierdlem79  42351  fourierdlem87  42359  sqwvfoura  42394  sqwvfourb  42395  sge0ad2en  42594  ovnsubaddlem1  42733  hoiqssbllem1  42785  hoiqssbllem2  42786  hoiqssbllem3  42787  lighneallem3  43619  dfeven3  43670  dfodd4  43671  oexpnegALTV  43689  flnn0div2ge  44491  logbpw2m1  44525  fllog2  44526  blennnelnn  44534  nnpw2blen  44538  blen1b  44546  blennnt2  44547  nnolog2flm1  44548  blennngt2o2  44550  blennn0e2  44552  0dig2nn0e  44570  dignn0flhalflem1  44573  dignn0flhalflem2  44574
  Copyright terms: Public domain W3C validator