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

Theorem 2pos 10087
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 9095 . . 3  |-  1  e.  RR
2 0lt1 9555 . . 3  |-  0  <  1
31, 1, 2, 2addgt0ii 9574 . 2  |-  0  <  ( 1  +  1 )
4 df-2 10063 . 2  |-  2  =  ( 1  +  1 )
53, 4breqtrri 4240 1  |-  0  <  2
Colors of variables: wff set class
Syntax hints:   class class class wbr 4215  (class class class)co 6084   0cc0 8995   1c1 8996    + caddc 8998    < clt 9125   2c2 10054
This theorem is referenced by:  2ne0  10088  3pos  10089  halfgt0  10193  halflt1  10194  halfpos2  10202  halfnneg2  10204  nominpos  10209  avglt1  10210  avglt2  10211  nn0n0n1ge2b  10286  2rp  10622  expubnd  11445  s3fv0  11857  sqrlem7  12059  sqr4  12083  sqr2gt1lt2  12085  sqreulem  12168  amgm2  12178  iseralt  12483  climcndslem2  12635  climcnds  12636  geoihalfsum  12664  efcllem  12685  ege2le3  12697  cos2bnd  12794  sin02gt0  12798  sincos2sgn  12800  sin4lt0  12801  epos  12811  sqr2re  12854  oexpneg  12916  oddprm  13194  iserodd  13214  odrngstr  13639  imasvalstr  13680  abvtrivd  15933  cnfldstr  16710  bl2in  18435  iihalf1  18961  iihalf2  18963  pcoass  19054  tchcphlem1  19197  minveclem2  19332  minveclem4  19338  ovolunlem1a  19397  vitalilem4  19508  mbfi1fseqlem5  19614  pilem2  20373  pilem3  20374  pipos  20378  sinhalfpilem  20379  sincosq1lem  20410  tangtx  20418  sinq12gt0  20420  sincos4thpi  20426  tan4thpi  20427  sincos6thpi  20428  cosordlem  20438  tanord1  20444  efif1olem2  20450  efif1olem4  20452  cxpcn3lem  20636  ang180lem1  20656  ang180lem2  20657  atantan  20768  atanbndlem  20770  atans2  20776  leibpilem1  20785  leibpi  20787  log2tlbnd  20790  basellem1  20868  basellem2  20869  basellem3  20870  ppisval  20891  ppiltx  20965  chtublem  21000  chtub  21001  chpval2  21007  bcmono  21066  bpos1lem  21071  bposlem1  21073  bposlem2  21074  bposlem3  21075  bposlem4  21076  bposlem5  21077  bposlem6  21078  bposlem7  21079  bposlem8  21080  bposlem9  21081  lgseisenlem1  21138  lgseisenlem2  21139  lgseisenlem3  21140  lgsquadlem1  21143  lgsquadlem2  21144  m1lgs  21151  2sqlem11  21164  chebbnd1lem1  21168  chebbnd1lem2  21169  chebbnd1lem3  21170  chebbnd1  21171  chtppilimlem1  21172  chtppilimlem2  21173  chtppilim  21174  chebbnd2  21176  chto1lb  21177  chpchtlim  21178  chpo1ub  21179  dchrisum0fno1  21210  mulog2sumlem2  21234  log2sumbnd  21243  selberglem2  21245  selberg2lem  21249  chpdifbndlem1  21252  logdivbnd  21255  pntrsumo1  21264  pntpbnd1a  21284  pntlemh  21298  pntlemr  21301  pntlemk  21305  pntlemo  21306  pnt2  21312  ex-fl  21760  nvge0  22168  ipidsq  22214  minvecolem2  22382  minvecolem4  22387  normpar2i  22663  bcsiALT  22686  opsqrlem6  23653  cdj3lem1  23942  sqsscirc1  24311  rnlogblem  24404  subfacval3  24880  4bc2eq6  25209  sin2h  26250  cos2h  26251  tan2h  26252  itg2addnclem  26270  nn0prpwlem  26339  trirn  26471  pellfundex  26963  rmspecsqrnq  26983  jm2.22  27080  jm2.23  27081  psgnunilem2  27409  stoweidlem14  27753  stoweidlem26  27765  stoweidlem49  27788  stoweidlem52  27791  wallispilem4  27807  wallispi  27809  wallispi2lem2  27811  wallispi2  27812  stirlinglem6  27818  stirlinglem7  27819  stirlinglem15  27827  stirlingr  27829  2eluzge0  28124  wrdlenge2n0  28208  swrdtrcfvl  28299  usgra2pthlem1  28348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-po 4506  df-so 4507  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-riota 6552  df-er 6908  df-en 7113  df-dom 7114  df-sdom 7115  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-2 10063
  Copyright terms: Public domain W3C validator