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

Theorem 2pos 10016
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 9025 . . 3  |-  1  e.  RR
2 0lt1 9484 . . 3  |-  0  <  1
31, 1, 2, 2addgt0ii 9503 . 2  |-  0  <  ( 1  +  1 )
4 df-2 9992 . 2  |-  2  =  ( 1  +  1 )
53, 4breqtrri 4180 1  |-  0  <  2
Colors of variables: wff set class
Syntax hints:   class class class wbr 4155  (class class class)co 6022   0cc0 8925   1c1 8926    + caddc 8928    < clt 9055   2c2 9983
This theorem is referenced by:  2ne0  10017  3pos  10018  halfgt0  10122  halflt1  10123  halfpos2  10131  halfnneg2  10133  nominpos  10138  avglt1  10139  avglt2  10140  nn0n0n1ge2b  10215  2rp  10551  expubnd  11369  s3fv0  11781  sqrlem7  11983  sqr4  12007  sqr2gt1lt2  12009  sqreulem  12092  amgm2  12102  iseralt  12407  climcndslem2  12559  climcnds  12560  geoihalfsum  12588  efcllem  12609  ege2le3  12621  cos2bnd  12718  sin02gt0  12722  sincos2sgn  12724  sin4lt0  12725  epos  12735  sqr2re  12778  oexpneg  12840  oddprm  13118  iserodd  13138  odrngstr  13563  imasvalstr  13604  abvtrivd  15857  cnfldstr  16630  bl2in  18333  iihalf1  18829  iihalf2  18831  pcoass  18922  tchcphlem1  19065  minveclem2  19196  minveclem4  19202  ovolunlem1a  19261  vitalilem4  19372  mbfi1fseqlem5  19480  pilem2  20237  pilem3  20238  pipos  20242  sinhalfpilem  20243  sincosq1lem  20274  tangtx  20282  sinq12gt0  20284  sincos4thpi  20290  tan4thpi  20291  sincos6thpi  20292  cosordlem  20302  tanord1  20308  efif1olem2  20314  efif1olem4  20316  cxpcn3lem  20500  ang180lem1  20520  ang180lem2  20521  atantan  20632  atanbndlem  20634  atans2  20640  leibpilem1  20649  leibpi  20651  log2tlbnd  20654  basellem1  20732  basellem2  20733  basellem3  20734  ppisval  20755  ppiltx  20829  chtublem  20864  chtub  20865  chpval2  20871  bcmono  20930  bpos1lem  20935  bposlem1  20937  bposlem2  20938  bposlem3  20939  bposlem4  20940  bposlem5  20941  bposlem6  20942  bposlem7  20943  bposlem8  20944  bposlem9  20945  lgseisenlem1  21002  lgseisenlem2  21003  lgseisenlem3  21004  lgsquadlem1  21007  lgsquadlem2  21008  m1lgs  21015  2sqlem11  21028  chebbnd1lem1  21032  chebbnd1lem2  21033  chebbnd1lem3  21034  chebbnd1  21035  chtppilimlem1  21036  chtppilimlem2  21037  chtppilim  21038  chebbnd2  21040  chto1lb  21041  chpchtlim  21042  chpo1ub  21043  dchrisum0fno1  21074  mulog2sumlem2  21098  log2sumbnd  21107  selberglem2  21109  selberg2lem  21113  chpdifbndlem1  21116  logdivbnd  21119  pntrsumo1  21128  pntpbnd1a  21148  pntlemh  21162  pntlemr  21165  pntlemk  21169  pntlemo  21170  pnt2  21176  ex-fl  21605  nvge0  22013  ipidsq  22059  minvecolem2  22227  minvecolem4  22232  normpar2i  22508  bcsiALT  22531  opsqrlem6  23498  cdj3lem1  23787  sqsscirc1  24112  rnlogblem  24197  subfacval3  24656  4bc2eq6  24985  nn0prpwlem  26018  trirn  26150  pellfundex  26642  rmspecsqrnq  26662  jm2.22  26759  jm2.23  26760  psgnunilem2  27089  stoweidlem14  27433  stoweidlem26  27445  stoweidlem49  27468  stoweidlem52  27471  wallispilem4  27487  wallispi  27489  wallispi2lem2  27491  wallispi2  27492  stirlinglem6  27498  stirlinglem7  27499  stirlinglem15  27507  stirlingr  27509
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643  ax-resscn 8982  ax-1cn 8983  ax-icn 8984  ax-addcl 8985  ax-addrcl 8986  ax-mulcl 8987  ax-mulrcl 8988  ax-mulcom 8989  ax-addass 8990  ax-mulass 8991  ax-distr 8992  ax-i2m1 8993  ax-1ne0 8994  ax-1rid 8995  ax-rnegex 8996  ax-rrecex 8997  ax-cnre 8998  ax-pre-lttri 8999  ax-pre-lttrn 9000  ax-pre-ltadd 9001  ax-pre-mulgt0 9002
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-nel 2555  df-ral 2656  df-rex 2657  df-reu 2658  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-mpt 4211  df-id 4441  df-po 4446  df-so 4447  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-riota 6487  df-er 6843  df-en 7048  df-dom 7049  df-sdom 7050  df-pnf 9057  df-mnf 9058  df-xr 9059  df-ltxr 9060  df-le 9061  df-sub 9227  df-neg 9228  df-2 9992
  Copyright terms: Public domain W3C validator