Theorem 2pos 10527

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 9499	. . 3 |- 1 e. RR
2		0lt1 9976	. . 3 |- 0 < 1
3	1, 1, 2, 2	addgt0ii 9996	. 2 |- 0 < ( 1 + 1 )
4		df-2 10494	. 2 |- 2 = ( 1 + 1 )
5	3, 4	breqtrri 4428	1 |- 0 < 2

Syntax hints:   class class class wbr 4403  (class class class)co 6203   0cc0 9396   1c1 9397   + caddc 9399   < clt 9532   2c2 10485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485  ax-resscn 9453  ax-1cn 9454  ax-icn 9455  ax-addcl 9456  ax-addrcl 9457  ax-mulcl 9458  ax-mulrcl 9459  ax-mulcom 9460  ax-addass 9461  ax-mulass 9462  ax-distr 9463  ax-i2m1 9464  ax-1ne0 9465  ax-1rid 9466  ax-rnegex 9467  ax-rrecex 9468  ax-cnre 9469  ax-pre-lttri 9470  ax-pre-lttrn 9471  ax-pre-ltadd 9472  ax-pre-mulgt0 9473

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-po 4752  df-so 4753  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-riota 6164  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-er 7214  df-en 7424  df-dom 7425  df-sdom 7426  df-pnf 9534  df-mnf 9535  df-xr 9536  df-ltxr 9537  df-le 9538  df-sub 9711  df-neg 9712  df-2 10494

This theorem is referenced by:  2ne0  10528  3pos  10529  halfgt0  10656  halflt1  10657  halfpos2  10668  halfnneg2  10670  nominpos  10675  avglt1  10676  avglt2  10677  nn0n0n1ge2b  10758  2eluzge0  11014  2rp  11110  s3fv0  12636  2swrd2eqwrdeq  12674  sqrlem7  12859  sqreulem  12968  amgm2  12978  iseralt  13283  climcndslem2  13434  climcnds  13435  geoihalfsum  13463  efcllem  13484  cos2bnd  13593  sin02gt0  13597  sincos2sgn  13599  sin4lt0  13600  epos  13610  sqr2re  13653  oexpneg  13716  oddprm  14003  iserodd  14023  odrngstr  14467  imasvalstr  14512  psgnunilem2  16123  cnfldstr  17948  bl2in  20110  iihalf1  20638  iihalf2  20640  pcoass  20731  tchcphlem1  20885  trirn  21034  minveclem2  21048  minveclem4  21054  ovolunlem1a  21114  vitalilem4  21227  mbfi1fseqlem5  21333  pilem2  22053  pilem3  22054  pipos  22059  sinhalfpilem  22061  sincosq1lem  22095  tangtx  22103  sinq12gt0  22105  sincos6thpi  22113  cosordlem  22123  tanord1  22129  efif1olem2  22135  efif1olem4  22137  cxpcn3lem  22321  ang180lem1  22341  ang180lem2  22342  atantan  22454  atanbndlem  22456  atans2  22462  leibpilem1  22471  leibpi  22473  log2tlbnd  22476  basellem1  22554  basellem2  22555  basellem3  22556  ppiltx  22651  chtublem  22686  chtub  22687  chpval2  22693  bcmono  22752  bpos1lem  22757  bposlem1  22759  bposlem2  22760  bposlem3  22761  bposlem4  22762  bposlem5  22763  bposlem6  22764  bposlem7  22765  lgseisenlem1  22824  lgseisenlem2  22825  lgseisenlem3  22826  lgsquadlem1  22829  lgsquadlem2  22830  chebbnd1lem1  22854  chebbnd1lem2  22855  chebbnd1lem3  22856  chebbnd1  22857  chtppilimlem1  22858  chtppilimlem2  22859  chtppilim  22860  chebbnd2  22862  chto1lb  22863  chpchtlim  22864  chpo1ub  22865  dchrisum0fno1  22896  mulog2sumlem2  22920  selberglem2  22931  selberg2lem  22935  chpdifbndlem1  22938  logdivbnd  22941  pntrsumo1  22950  pntpbnd1a  22970  pntlemh  22984  pntlemr  22987  pntlemk  22991  pntlemo  22992  pnt2  22998  ex-fl  23826  nvge0  24234  minvecolem2  24448  minvecolem4  24453  bcsiALT  24753  opsqrlem6  25721  cdj3lem1  26010  sqsscirc1  26503  rnlogblem  26623  signslema  27127  subfacval3  27241  sin2h  28590  cos2h  28591  tan2h  28592  itg2addnclem  28611  nn0prpwlem  28685  pellfundex  29395  rmspecsqrnq  29415  jm2.22  29512  jm2.23  29513  stoweidlem14  29977  stoweidlem49  30012  stoweidlem52  30015  wallispilem4  30031  wallispi2lem2  30035  stirlinglem6  30042  stirlinglem15  30051  stirlingr  30053  ccatw2s1p1  30437  wwlkextwrd  30528  wwlkextfun  30529  wwlkextinj  30530  clwwlkn0  30605  clwlkisclwwlklem2a2  30610