Theorem 3pos 6005

Description: The number 3 is positive.

Assertion

Ref	Expression
3pos	|- 0 < 3

Proof of Theorem 3pos

Step	Hyp	Ref	Expression
1		2re 5993	. . 3 |- 2 e. RR
2		1re 5455	. . 3 |- 1 e. RR
3		2pos 6003	. . 3 |- 0 < 2
4		lt01 5700	. . 3 |- 0 < 1
5	1, 2, 3, 4	addgt0ii 5621	. 2 |- 0 < (2 + 1)
6		df-3 5985	. 2 |- 3 = (2 + 1)
7	5, 6	breqtrri 2655	1 |- 0 < 3

Syntax hints:   class class class wbr 2634  (class class class)co 3979  0cc0 5254  1c1 5255   + caddc 5257   < clt 5506  2c2 5975  3c3 5976

This theorem is referenced by:  4pos 6006  8th4div3 6045  sqr9 6750  efaddlem20 7389  sin01bndlem1 7500  sin01bndlem3 7502  cos01bndlem3 7504  sin01gt0 7509  cos01gt0 7510  ruclem1 7543  ruclem2 7544  ruclem3 7545  ruclem13 7555  ruclem26 7568  sincos6thpi 8735

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-rep 2708  ax-sep 2718  ax-nul 2725  ax-pow 2758  ax-pr 2795  ax-un 2882  ax-inf2 4642

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-nel 1595  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2012  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-pss 2066  df-nul 2292  df-if 2374  df-pw 2414  df-sn 2424  df-pr 2425  df-tp 2427  df-op 2428  df-uni 2518  df-int 2548  df-iun 2582  df-br 2635  df-opab 2682  df-tr 2696  df-eprel 2848  df-id 2851  df-po 2856  df-so 2866  df-fr 2933  df-we 2950  df-ord 2967  df-on 2968  df-lim 2969  df-suc 2970  df-om 3148  df-xp 3200  df-rel 3201  df-cnv 3202  df-co 3203  df-dm 3204  df-rn 3205  df-res 3206  df-ima 3207  df-fun 3208  df-fn 3209  df-f 3210  df-f1 3211  df-fo 3212  df-f1o 3213  df-fv 3214  df-rdg 3948  df-opr 3981  df-oprab 3982  df-1st 4095  df-2nd 4096  df-1o 4149  df-oadd 4151  df-omul 4152  df-er 4277  df-ec 4279  df-qs 4282  df-en 4386  df-dom 4387  df-sdom 4388  df-ni 5020  df-pli 5021  df-mi 5022  df-lti 5023  df-plpq 5055  df-mpq 5056  df-enq 5057  df-nq 5058  df-plq 5059  df-mq 5060  df-rq 5061  df-ltq 5062  df-1q 5063  df-np 5106  df-1p 5107  df-plp 5108  df-mp 5109  df-ltp 5110  df-plpr 5184  df-mpr 5185  df-enr 5186  df-nr 5187  df-plr 5188  df-mr 5189  df-ltr 5190  df-0r 5191  df-1r 5192  df-m1r 5193  df-c 5260  df-0 5261  df-1 5262  df-i 5263  df-r 5264  df-plus 5265  df-mul 5266  df-lt 5267  df-sub 5376  df-neg 5378  df-pnf 5507  df-mnf 5508  df-xr 5509  df-ltxr 5510  df-le 5511  df-2 5984  df-3 5985

Copyright terms: Public domain