Theorem 3pos 12250

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 12219	. . 3 ⊢ 2 ∈ ℝ
2		1re 11132	. . 3 ⊢ 1 ∈ ℝ
3		2pos 12248	. . 3 ⊢ 0 < 2
4		0lt1 11659	. . 3 ⊢ 0 < 1
5	1, 2, 3, 4	addgt0ii 11679	. 2 ⊢ 0 < (2 + 1)
6		df-3 12209	. 2 ⊢ 3 = (2 + 1)
7	5, 6	breqtrri 5125	1 ⊢ 0 < 3

Syntax hints:   class class class wbr 5098  (class class class)co 7358  0cc0 11026  1c1 11027   + caddc 11029   < clt 11166  2c2 12200  3c3 12201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-2 12208  df-3 12209

This theorem is referenced by:  4pos  12252  3rp  12911  fz0to4untppr  13546  fz0to5un2tp  13547  s4fv0  14818  01sqrexlem7  15171  sqrt9  15196  ef01bndlem  16109  cos2bnd  16113  sin01gt0  16115  cos01gt0  16116  rpnnen2lem3  16141  rpnnen2lem4  16142  rpnnen2lem9  16147  flodddiv4  16342  43prm  17049  slotsdifunifndx  17321  tangtx  26470  sincos6thpi  26481  pige3ALT  26485  log2cnv  26910  log2tlbnd  26911  ppiub  27171  bposlem2  27252  bposlem3  27253  bposlem4  27254  bposlem5  27255  lgsdir2lem1  27292  dchrvmasumiflem1  27468  tgcgr4  28603  frgrogt3nreg  30472  friendshipgt3  30473  ex-gcd  30532  cyc3fv3  33221  cyc3conja  33239  evl1deg3  33659  2sqr3minply  33937  cos9thpiminplylem1  33939  hgt750lemd  34805  hgt750lem2  34809  heiborlem5  38016  heiborlem7  38018  3lexlogpow5ineq2  42309  3lexlogpow5ineq4  42310  3lexlogpow5ineq3  42311  3lexlogpow2ineq1  42312  3lexlogpow2ineq2  42313  3lexlogpow5ineq5  42314  aks4d1lem1  42316  aks4d1p1p6  42327  aks4d1p1p5  42329  aks4d1p1  42330  aks4d1p2  42331  aks4d1p3  42332  aks4d1p5  42334  aks4d1p6  42335  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8  42341  aks4d1p9  42342  aks6d1c7lem1  42434  aks6d1c7lem2  42435  aks6d1c7  42438  aks5lem6  42446  aks5lem8  42455  acos1half  42613  jm2.23  43238  stoweidlem13  46257  stoweidlem26  46270  stoweidlem34  46278  stoweidlem42  46286  stoweidlem59  46303  stoweid  46307  wallispilem4  46312  smfmullem4  47038  257prm  47807  127prm  47845  nfermltl2rev  47989  usgrexmpl1lem  48267  usgrexmpl2lem  48272  usgrexmpl2nb0  48277  gpgusgralem  48302  gpg3kgrtriexlem3  48331  gpg3kgrtriexlem6  48334  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  gpg5edgnedg  48376  sepfsepc  49173