Theorem 2pos 9126

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 8070	. . 3 |- 1 e. RR
2		0lt1 8198	. . 3 |- 0 < 1
3	1, 1, 2, 2	addgt0ii 8563	. 2 |- 0 < ( 1 + 1 )
4		df-2 9094	. 2 |- 2 = ( 1 + 1 )
5	3, 4	breqtrri 4070	1 |- 0 < 2

Syntax hints:   class class class wbr 4043  (class class class)co 5943   0cc0 7924   1c1 7925   + caddc 7927   < clt 8106   2c2 9086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4479  ax-setind 4584  ax-cnex 8015  ax-resscn 8016  ax-1cn 8017  ax-1re 8018  ax-icn 8019  ax-addcl 8020  ax-addrcl 8021  ax-mulcl 8022  ax-addcom 8024  ax-addass 8026  ax-i2m1 8029  ax-0lt1 8030  ax-0id 8032  ax-rnegex 8033  ax-pre-lttrn 8038  ax-pre-ltadd 8040

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-xp 4680  df-iota 5231  df-fv 5278  df-ov 5946  df-pnf 8108  df-mnf 8109  df-ltxr 8111  df-2 9094

This theorem is referenced by:  2ne0  9127  2ap0  9128  3pos  9129  halfgt0  9251  halflt1  9253  halfpos2  9266  halfnneg2  9268  nominpos  9274  avglt1  9275  avglt2  9276  nn0n0n1ge2b  9451  3halfnz  9469  2rp  9779  xleaddadd  10008  2tnp1ge0ge0  10442  mulp1mod1  10508  amgm2  11400  cos2bnd  12042  sin02gt0  12046  sincos2sgn  12048  sin4lt0  12049  epos  12063  oexpneg  12159  oddge22np1  12163  evennn02n  12164  nn0ehalf  12185  nno  12188  nn0oddm1d2  12191  nnoddm1d2  12192  flodddiv4t2lthalf  12221  sqrt2re  12456  sqrt2irrap  12473  slotsdifdsndx  13028  imasvalstrd  13073  cnfldstr  14291  bl2in  14846  pilem3  15226  pipos  15231  sinhalfpilem  15234  sincosq1lem  15268  sinq12gt0  15273  coseq00topi  15278  coseq0negpitopi  15279  tangtx  15281  sincos4thpi  15283  tan4thpi  15284  sincos6thpi  15285  cosordlem  15292  cos02pilt1  15294  gausslemma2dlem0c  15499  gausslemma2dlem1a  15506  gausslemma2dlem2  15510  gausslemma2dlem3  15511  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgsquadlem1  15525  lgsquadlem2  15526  2lgslem1a1  15534  2lgslem1a2  15535  2lgslem1c  15538  2lgslem3a1  15545  ex-fl  15623