Theorem 3pos 12291

Description: The number 3 is positive. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
3pos	⊢ 0 < 3

Proof of Theorem 3pos

Step	Hyp	Ref	Expression
1		2re 12260	. . 3 ⊢ 2 ∈ ℝ
2		1re 11174	. . 3 ⊢ 1 ∈ ℝ
3		2pos 12289	. . 3 ⊢ 0 < 2
4		0lt1 11700	. . 3 ⊢ 0 < 1
5	1, 2, 3, 4	addgt0ii 11720	. 2 ⊢ 0 < (2 + 1)
6		df-3 12250	. 2 ⊢ 3 = (2 + 1)
7	5, 6	breqtrri 5134	1 ⊢ 0 < 3

Syntax hints:   class class class wbr 5107  (class class class)co 7387  0cc0 11068  1c1 11069   + caddc 11071   < clt 11208  2c2 12241  3c3 12242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-2 12249  df-3 12250

This theorem is referenced by:  4pos  12293  3rp  12957  fz0to4untppr  13591  fz0to5un2tp  13592  s4fv0  14861  01sqrexlem7  15214  sqrt9  15239  ef01bndlem  16152  cos2bnd  16156  sin01gt0  16158  cos01gt0  16159  rpnnen2lem3  16184  rpnnen2lem4  16185  rpnnen2lem9  16190  flodddiv4  16385  43prm  17092  slotsdifunifndx  17364  tangtx  26414  sincos6thpi  26425  pige3ALT  26429  log2cnv  26854  log2tlbnd  26855  ppiub  27115  bposlem2  27196  bposlem3  27197  bposlem4  27198  bposlem5  27199  lgsdir2lem1  27236  dchrvmasumiflem1  27412  tgcgr4  28458  frgrogt3nreg  30326  friendshipgt3  30327  ex-gcd  30386  cyc3fv3  33096  cyc3conja  33114  evl1deg3  33547  2sqr3minply  33770  cos9thpiminplylem1  33772  hgt750lemd  34639  hgt750lem2  34643  heiborlem5  37809  heiborlem7  37811  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  aks4d1p1p6  42061  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  aks6d1c7lem1  42168  aks6d1c7lem2  42169  aks6d1c7  42172  aks5lem6  42180  aks5lem8  42189  acos1half  42346  jm2.23  42985  stoweidlem13  46011  stoweidlem26  46024  stoweidlem34  46032  stoweidlem42  46040  stoweidlem59  46057  stoweid  46061  wallispilem4  46066  smfmullem4  46792  257prm  47562  127prm  47600  nfermltl2rev  47744  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  gpgusgralem  48047  gpg3kgrtriexlem3  48076  gpg3kgrtriexlem6  48079  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  sepfsepc  48916