MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2pos Unicode version

Theorem 2pos 10071
Description: The number 2 is positive. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
2pos  |-  0  <  2

Proof of Theorem 2pos
StepHypRef Expression
1 1re 9079 . . 3  |-  1  e.  RR
2 0lt1 9539 . . 3  |-  0  <  1
31, 1, 2, 2addgt0ii 9558 . 2  |-  0  <  ( 1  +  1 )
4 df-2 10047 . 2  |-  2  =  ( 1  +  1 )
53, 4breqtrri 4229 1  |-  0  <  2
Colors of variables: wff set class
Syntax hints:   class class class wbr 4204  (class class class)co 6072   0cc0 8979   1c1 8980    + caddc 8982    < clt 9109   2c2 10038
This theorem is referenced by:  2ne0  10072  3pos  10073  halfgt0  10177  halflt1  10178  halfpos2  10186  halfnneg2  10188  nominpos  10193  avglt1  10194  avglt2  10195  nn0n0n1ge2b  10270  2rp  10606  expubnd  11428  s3fv0  11840  sqrlem7  12042  sqr4  12066  sqr2gt1lt2  12068  sqreulem  12151  amgm2  12161  iseralt  12466  climcndslem2  12618  climcnds  12619  geoihalfsum  12647  efcllem  12668  ege2le3  12680  cos2bnd  12777  sin02gt0  12781  sincos2sgn  12783  sin4lt0  12784  epos  12794  sqr2re  12837  oexpneg  12899  oddprm  13177  iserodd  13197  odrngstr  13622  imasvalstr  13663  abvtrivd  15916  cnfldstr  16693  bl2in  18418  iihalf1  18944  iihalf2  18946  pcoass  19037  tchcphlem1  19180  minveclem2  19315  minveclem4  19321  ovolunlem1a  19380  vitalilem4  19491  mbfi1fseqlem5  19599  pilem2  20356  pilem3  20357  pipos  20361  sinhalfpilem  20362  sincosq1lem  20393  tangtx  20401  sinq12gt0  20403  sincos4thpi  20409  tan4thpi  20410  sincos6thpi  20411  cosordlem  20421  tanord1  20427  efif1olem2  20433  efif1olem4  20435  cxpcn3lem  20619  ang180lem1  20639  ang180lem2  20640  atantan  20751  atanbndlem  20753  atans2  20759  leibpilem1  20768  leibpi  20770  log2tlbnd  20773  basellem1  20851  basellem2  20852  basellem3  20853  ppisval  20874  ppiltx  20948  chtublem  20983  chtub  20984  chpval2  20990  bcmono  21049  bpos1lem  21054  bposlem1  21056  bposlem2  21057  bposlem3  21058  bposlem4  21059  bposlem5  21060  bposlem6  21061  bposlem7  21062  bposlem8  21063  bposlem9  21064  lgseisenlem1  21121  lgseisenlem2  21122  lgseisenlem3  21123  lgsquadlem1  21126  lgsquadlem2  21127  m1lgs  21134  2sqlem11  21147  chebbnd1lem1  21151  chebbnd1lem2  21152  chebbnd1lem3  21153  chebbnd1  21154  chtppilimlem1  21155  chtppilimlem2  21156  chtppilim  21157  chebbnd2  21159  chto1lb  21160  chpchtlim  21161  chpo1ub  21162  dchrisum0fno1  21193  mulog2sumlem2  21217  log2sumbnd  21226  selberglem2  21228  selberg2lem  21232  chpdifbndlem1  21235  logdivbnd  21238  pntrsumo1  21247  pntpbnd1a  21267  pntlemh  21281  pntlemr  21284  pntlemk  21288  pntlemo  21289  pnt2  21295  ex-fl  21743  nvge0  22151  ipidsq  22197  minvecolem2  22365  minvecolem4  22370  normpar2i  22646  bcsiALT  22669  opsqrlem6  23636  cdj3lem1  23925  sqsscirc1  24294  rnlogblem  24387  subfacval3  24863  4bc2eq6  25192  itg2addnclem  26202  nn0prpwlem  26262  trirn  26394  pellfundex  26886  rmspecsqrnq  26906  jm2.22  27003  jm2.23  27004  psgnunilem2  27333  stoweidlem14  27677  stoweidlem26  27689  stoweidlem49  27712  stoweidlem52  27715  wallispilem4  27731  wallispi  27733  wallispi2lem2  27735  wallispi2  27736  stirlinglem6  27742  stirlinglem7  27743  stirlinglem15  27751  stirlingr  27753  shwrdssizelem1a  28165  usgra2pthlem1  28184
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692  ax-resscn 9036  ax-1cn 9037  ax-icn 9038  ax-addcl 9039  ax-addrcl 9040  ax-mulcl 9041  ax-mulrcl 9042  ax-mulcom 9043  ax-addass 9044  ax-mulass 9045  ax-distr 9046  ax-i2m1 9047  ax-1ne0 9048  ax-1rid 9049  ax-rnegex 9050  ax-rrecex 9051  ax-cnre 9052  ax-pre-lttri 9053  ax-pre-lttrn 9054  ax-pre-ltadd 9055  ax-pre-mulgt0 9056
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-po 4495  df-so 4496  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-oprab 6076  df-mpt2 6077  df-riota 6540  df-er 6896  df-en 7101  df-dom 7102  df-sdom 7103  df-pnf 9111  df-mnf 9112  df-xr 9113  df-ltxr 9114  df-le 9115  df-sub 9282  df-neg 9283  df-2 10047
  Copyright terms: Public domain W3C validator