Theorem 2pos 10729

Description: The number 2 is positive. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2pos	|- 0 < 2

Proof of Theorem 2pos

Step	Hyp	Ref	Expression
1		1re 9668	. . 3 |- 1 e. RR
2		0lt1 10164	. . 3 |- 0 < 1
3	1, 1, 2, 2	addgt0ii 10184	. 2 |- 0 < ( 1 + 1 )
4		df-2 10696	. 2 |- 2 = ( 1 + 1 )
5	3, 4	breqtrri 4442	1 |- 0 < 2

Syntax hints:   class class class wbr 4416  (class class class)co 6315   0cc0 9565   1c1 9566   + caddc 9568   < clt 9701   2c2 10687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-2 10696

This theorem is referenced by:  2ne0  10730  3pos  10731  halfgt0  10859  halflt1  10860  halfpos2  10871  halfnneg2  10873  nominpos  10878  avglt1  10879  avglt2  10880  nn0n0n1ge2b  10962  2rp  11336  zgt1rpn0n1  11369  s3fv0  13022  2swrd2eqwrdeq  13077  sqrlem7  13361  sqreulem  13471  amgm2  13481  iseralt  13800  climcndslem2  13957  climcnds  13958  geoihalfsum  13987  efcllem  14181  cos2bnd  14291  sin02gt0  14295  sincos2sgn  14297  sin4lt0  14298  epos  14308  sqrt2re  14351  oexpneg  14417  oddprm  14814  iserodd  14834  prmgaplem7  15076  odrngstr  15353  imasvalstr  15399  psgnunilem2  17185  cnfldstr  19021  bl2in  21464  iihalf1  22008  iihalf2  22010  pcoass  22104  tchcphlem1  22258  trirn  22403  minveclem2  22417  minveclem4  22423  minveclem2OLD  22429  minveclem4OLD  22435  ovolunlem1a  22498  vitalilem4  22618  mbfi1fseqlem5  22726  pilem2  23456  pilem2OLD  23457  pilem3  23458  pilem3OLD  23459  pipos  23464  sinhalfpilem  23467  sincosq1lem  23501  tangtx  23509  sinq12gt0  23511  sincos6thpi  23519  cosordlem  23529  tanord1  23535  efif1olem2  23541  efif1olem4  23543  cxpcn3lem  23736  ang180lem1  23787  ang180lem2  23788  atantan  23898  atanbndlem  23900  atans2  23906  leibpilem1  23915  leibpi  23917  log2tlbnd  23920  basellem1  24056  basellem2  24057  basellem3  24058  ppiltx  24153  ppiub  24181  chtublem  24188  chtub  24189  chpval2  24195  bcmono  24254  bpos1lem  24259  bposlem1  24261  bposlem2  24262  bposlem3  24263  bposlem4  24264  bposlem5  24265  bposlem6  24266  bposlem7  24267  lgseisenlem1  24326  lgseisenlem2  24327  lgseisenlem3  24328  lgsquadlem1  24331  lgsquadlem2  24332  chebbnd1lem1  24356  chebbnd1lem2  24357  chebbnd1lem3  24358  chebbnd1  24359  chtppilimlem1  24360  chtppilimlem2  24361  chtppilim  24362  chebbnd2  24364  chto1lb  24365  chpchtlim  24366  chpo1ub  24367  dchrisum0fno1  24398  mulog2sumlem2  24422  selberglem2  24433  selberg2lem  24437  chpdifbndlem1  24440  logdivbnd  24443  pntrsumo1  24452  pntpbnd1a  24472  pntlemh  24486  pntlemr  24489  pntlemk  24493  pntlemo  24494  pnt2  24500  wwlkextwrd  25505  wwlkextfun  25506  wwlkextinj  25507  clwwlkn0  25551  clwlkisclwwlklem2a2  25557  ex-fl  25946  nvge0  26352  minvecolem2  26566  minvecolem4  26571  minvecolem2OLD  26576  minvecolem4OLD  26581  bcsiALT  26881  opsqrlem6  27847  cdj3lem1  28136  sqsscirc1  28763  omssubadd  29177  omssubaddOLD  29181  signslema  29500  subfacval3  29961  nn0prpwlem  31027  sin2h  31980  cos2h  31981  tan2h  31982  itg2addnclem  32038  pellfundex  35779  rmspecsqrtnq  35799  jm2.22  35895  jm2.23  35896  imo72b2lem0  36653  sumnnodd  37748  sinaover2ne0  37781  stoweidlem14  37912  stoweidlem49  37948  stoweidlem52  37951  wallispilem4  37968  wallispi2lem2  37972  stirlinglem6  37979  stirlinglem15  37988  stirlingr  37990  dirkerval2  37994  dirkertrigeqlem3  38000  dirkercncflem4  38006  fourierdlem24  38031  fourierdlem79  38087  fourierdlem103  38111  fourierdlem104  38112  fourierdlem112  38120  fourierswlem  38132  fouriersw  38133  oexpnegALTV  38844  nnoALTV  38862  nn0oALTV  38863  nn0e  38864  evengpoap3  38932  umgrislfupgrlem  39718  3halfnz  40590  nno  40601  nn0eo  40608  flnn0div2ge  40613  fldivexpfllog2  40649  fllog2  40652  blennngt2o2  40676  dignn0flhalf  40702