Theorem 2pos 9378

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 8319	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 8447	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 8813	. 2 ⊢ 0 < (1 + 1)
4		df-2 9346	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 4155	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 4128  (class class class)co 6079  0cc0 8173  1c1 8174   + caddc 8176   < clt 8354  2c2 9338

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682  ax-cnex 8264  ax-resscn 8265  ax-1cn 8266  ax-1re 8267  ax-icn 8268  ax-addcl 8269  ax-addrcl 8270  ax-mulcl 8271  ax-addcom 8273  ax-addass 8275  ax-i2m1 8278  ax-0lt1 8279  ax-0id 8281  ax-rnegex 8282  ax-pre-lttrn 8287  ax-pre-ltadd 8289

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-opab 4191  df-xp 4778  df-iota 5335  df-fv 5383  df-ov 6082  df-pnf 8356  df-mnf 8357  df-ltxr 8359  df-2 9346

This theorem is referenced by:  2ne0  9379  2ap0  9380  3pos  9381  halfgt0  9503  halflt1  9505  halfpos2  9518  halfnneg2  9520  nominpos  9526  avglt1  9527  avglt2  9528  nn0n0n1ge2b  9708  3halfnz  9726  2rp  10042  xleaddadd  10272  2tnp1ge0ge0  10719  mulp1mod1  10785  s3fv0g  11546  amgm2  11867  cos2bnd  12510  sin02gt0  12514  sincos2sgn  12516  sin4lt0  12517  epos  12531  oexpneg  12627  oddge22np1  12631  evennn02n  12632  nn0ehalf  12653  nno  12656  nn0oddm1d2  12659  nnoddm1d2  12660  flodddiv4t2lthalf  12689  sqrt2re  12924  sqrt2irrap  12941  slotsdifdsndx  13562  imasvalstrd  13602  cnfldstr  14878  bl2in  15487  pilem3  15867  pipos  15872  sinhalfpilem  15875  sincosq1lem  15909  sinq12gt0  15914  coseq00topi  15919  coseq0negpitopi  15920  tangtx  15922  sincos4thpi  15924  tan4thpi  15925  sincos6thpi  15926  cosordlem  15933  cos02pilt1  15935  log2tlbndlog2  16065  gausslemma2dlem0c  16153  gausslemma2dlem1a  16160  gausslemma2dlem2  16164  gausslemma2dlem3  16165  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem3  16174  lgsquadlem1  16179  lgsquadlem2  16180  2lgslem1a1  16188  2lgslem1a2  16189  2lgslem1c  16192  2lgslem3a1  16199  konigsberg  16717  ex-fl  16722