Theorem 2pos 10623

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 9584	. . 3 |- 1 e. RR
2		0lt1 10071	. . 3 |- 0 < 1
3	1, 1, 2, 2	addgt0ii 10091	. 2 |- 0 < ( 1 + 1 )
4		df-2 10590	. 2 |- 2 = ( 1 + 1 )
5	3, 4	breqtrri 4464	1 |- 0 < 2

Syntax hints:   class class class wbr 4439  (class class class)co 6270   0cc0 9481   1c1 9482   + caddc 9484   < clt 9617   2c2 10581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-po 4789  df-so 4790  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-2 10590

This theorem is referenced by:  2ne0  10624  3pos  10625  halfgt0  10752  halflt1  10753  halfpos2  10764  halfnneg2  10766  nominpos  10771  avglt1  10772  avglt2  10773  nn0n0n1ge2b  10856  2rp  11226  zgt1rpn0n1  11258  s3fv0  12844  2swrd2eqwrdeq  12882  sqrlem7  13164  sqreulem  13274  amgm2  13284  iseralt  13589  climcndslem2  13744  climcnds  13745  geoihalfsum  13773  efcllem  13895  cos2bnd  14005  sin02gt0  14009  sincos2sgn  14011  sin4lt0  14012  epos  14022  sqrt2re  14067  oexpneg  14133  oddprm  14423  iserodd  14443  odrngstr  14895  imasvalstr  14941  psgnunilem2  16719  cnfldstr  18617  bl2in  21069  iihalf1  21597  iihalf2  21599  pcoass  21690  tchcphlem1  21844  trirn  21993  minveclem2  22007  minveclem4  22013  ovolunlem1a  22073  vitalilem4  22186  mbfi1fseqlem5  22292  pilem2  23013  pilem3  23014  pipos  23019  sinhalfpilem  23022  sincosq1lem  23056  tangtx  23064  sinq12gt0  23066  sincos6thpi  23074  cosordlem  23084  tanord1  23090  efif1olem2  23096  efif1olem4  23098  cxpcn3lem  23289  ang180lem1  23340  ang180lem2  23341  atantan  23451  atanbndlem  23453  atans2  23459  leibpilem1  23468  leibpi  23470  log2tlbnd  23473  basellem1  23552  basellem2  23553  basellem3  23554  ppiltx  23649  ppiub  23677  chtublem  23684  chtub  23685  chpval2  23691  bcmono  23750  bpos1lem  23755  bposlem1  23757  bposlem2  23758  bposlem3  23759  bposlem4  23760  bposlem5  23761  bposlem6  23762  bposlem7  23763  lgseisenlem1  23822  lgseisenlem2  23823  lgseisenlem3  23824  lgsquadlem1  23827  lgsquadlem2  23828  chebbnd1lem1  23852  chebbnd1lem2  23853  chebbnd1lem3  23854  chebbnd1  23855  chtppilimlem1  23856  chtppilimlem2  23857  chtppilim  23858  chebbnd2  23860  chto1lb  23861  chpchtlim  23862  chpo1ub  23863  dchrisum0fno1  23894  mulog2sumlem2  23918  selberglem2  23929  selberg2lem  23933  chpdifbndlem1  23936  logdivbnd  23939  pntrsumo1  23948  pntpbnd1a  23968  pntlemh  23982  pntlemr  23985  pntlemk  23989  pntlemo  23990  pnt2  23996  wwlkextwrd  24930  wwlkextfun  24931  wwlkextinj  24932  clwwlkn0  24976  clwlkisclwwlklem2a2  24982  ex-fl  25370  nvge0  25775  minvecolem2  25989  minvecolem4  25994  bcsiALT  26294  opsqrlem6  27262  cdj3lem1  27551  sqsscirc1  28125  omssubadd  28508  signslema  28783  subfacval3  28897  sin2h  30285  cos2h  30286  tan2h  30287  itg2addnclem  30306  nn0prpwlem  30380  pellfundex  31061  rmspecsqrtnq  31081  jm2.22  31176  jm2.23  31177  sumnnodd  31875  sinaover2ne0  31907  stoweidlem14  32035  stoweidlem49  32070  stoweidlem52  32073  wallispilem4  32089  wallispi2lem2  32093  stirlinglem6  32100  stirlinglem15  32109  stirlingr  32111  dirkerval2  32115  dirkertrigeqlem3  32121  dirkercncflem4  32127  fourierdlem24  32152  fourierdlem79  32207  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  fourierswlem  32252  fouriersw  32253  oexpnegALTV  32583  nnoALTV  32601  nn0oALTV  32602  nn0e  32603  3halfnz  33380  nno  33392  nn0eo  33399  flnn0div2ge  33404  fldivexpfllog2  33440  fllog2  33443  blennngt2o2  33467  dignn0flhalf  33493  imo72b2lem0  38434