Theorem 2pos 9127

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 8071	. . 3 |- 1 e. RR
2		0lt1 8199	. . 3 |- 0 < 1
3	1, 1, 2, 2	addgt0ii 8564	. 2 |- 0 < ( 1 + 1 )
4		df-2 9095	. 2 |- 2 = ( 1 + 1 )
5	3, 4	breqtrri 4071	1 |- 0 < 2

Syntax hints:   class class class wbr 4044  (class class class)co 5944   0cc0 7925   1c1 7926   + caddc 7928   < clt 8107   2c2 9087

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253  ax-un 4480  ax-setind 4585  ax-cnex 8016  ax-resscn 8017  ax-1cn 8018  ax-1re 8019  ax-icn 8020  ax-addcl 8021  ax-addrcl 8022  ax-mulcl 8023  ax-addcom 8025  ax-addass 8027  ax-i2m1 8030  ax-0lt1 8031  ax-0id 8033  ax-rnegex 8034  ax-pre-lttrn 8039  ax-pre-ltadd 8041

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ne 2377  df-nel 2472  df-ral 2489  df-rex 2490  df-rab 2493  df-v 2774  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-xp 4681  df-iota 5232  df-fv 5279  df-ov 5947  df-pnf 8109  df-mnf 8110  df-ltxr 8112  df-2 9095

This theorem is referenced by:  2ne0  9128  2ap0  9129  3pos  9130  halfgt0  9252  halflt1  9254  halfpos2  9267  halfnneg2  9269  nominpos  9275  avglt1  9276  avglt2  9277  nn0n0n1ge2b  9452  3halfnz  9470  2rp  9780  xleaddadd  10009  2tnp1ge0ge0  10444  mulp1mod1  10510  amgm2  11429  cos2bnd  12071  sin02gt0  12075  sincos2sgn  12077  sin4lt0  12078  epos  12092  oexpneg  12188  oddge22np1  12192  evennn02n  12193  nn0ehalf  12214  nno  12217  nn0oddm1d2  12220  nnoddm1d2  12221  flodddiv4t2lthalf  12250  sqrt2re  12485  sqrt2irrap  12502  slotsdifdsndx  13057  imasvalstrd  13102  cnfldstr  14320  bl2in  14875  pilem3  15255  pipos  15260  sinhalfpilem  15263  sincosq1lem  15297  sinq12gt0  15302  coseq00topi  15307  coseq0negpitopi  15308  tangtx  15310  sincos4thpi  15312  tan4thpi  15313  sincos6thpi  15314  cosordlem  15321  cos02pilt1  15323  gausslemma2dlem0c  15528  gausslemma2dlem1a  15535  gausslemma2dlem2  15539  gausslemma2dlem3  15540  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgsquadlem1  15554  lgsquadlem2  15555  2lgslem1a1  15563  2lgslem1a2  15564  2lgslem1c  15567  2lgslem3a1  15574  ex-fl  15661