Theorem 2pos 8669

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 7637	. . 3 |- 1 e. RR
2		0lt1 7760	. . 3 |- 0 < 1
3	1, 1, 2, 2	addgt0ii 8120	. 2 |- 0 < ( 1 + 1 )
4		df-2 8637	. 2 |- 2 = ( 1 + 1 )
5	3, 4	breqtrri 3900	1 |- 0 < 2

Syntax hints:   class class class wbr 3875  (class class class)co 5706   0cc0 7500   1c1 7501   + caddc 7503   < clt 7672   2c2 8629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-cnex 7586  ax-resscn 7587  ax-1cn 7588  ax-1re 7589  ax-icn 7590  ax-addcl 7591  ax-addrcl 7592  ax-mulcl 7593  ax-addcom 7595  ax-addass 7597  ax-i2m1 7600  ax-0lt1 7601  ax-0id 7603  ax-rnegex 7604  ax-pre-lttrn 7609  ax-pre-ltadd 7611

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-nel 2363  df-ral 2380  df-rex 2381  df-rab 2384  df-v 2643  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-opab 3930  df-xp 4483  df-iota 5024  df-fv 5067  df-ov 5709  df-pnf 7674  df-mnf 7675  df-ltxr 7677  df-2 8637

This theorem is referenced by:  2ne0  8670  2ap0  8671  3pos  8672  halfgt0  8787  halflt1  8789  halfpos2  8802  halfnneg2  8804  nominpos  8809  avglt1  8810  avglt2  8811  nn0n0n1ge2b  8982  3halfnz  9000  2rp  9296  xleaddadd  9511  2tnp1ge0ge0  9915  mulp1mod1  9979  amgm2  10730  cos2bnd  11265  sin02gt0  11268  sincos2sgn  11270  sin4lt0  11271  epos  11282  oexpneg  11369  oddge22np1  11373  evennn02n  11374  nn0ehalf  11395  nno  11398  nn0oddm1d2  11401  nnoddm1d2  11402  flodddiv4t2lthalf  11429  sqrt2re  11634  sqrt2irrap  11650  bl2in  12331  ex-fl  12540