Theorem 3pos 12314

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 12283	. . 3 ⊢ 2 ∈ ℝ
2		1re 11211	. . 3 ⊢ 1 ∈ ℝ
3		2pos 12312	. . 3 ⊢ 0 < 2
4		0lt1 11733	. . 3 ⊢ 0 < 1
5	1, 2, 3, 4	addgt0ii 11753	. 2 ⊢ 0 < (2 + 1)
6		df-3 12273	. 2 ⊢ 3 = (2 + 1)
7	5, 6	breqtrri 5175	1 ⊢ 0 < 3

Syntax hints:   class class class wbr 5148  (class class class)co 7406  0cc0 11107  1c1 11108   + caddc 11110   < clt 11245  2c2 12264  3c3 12265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-2 12272  df-3 12273

This theorem is referenced by:  3ne0  12315  4pos  12316  3rp  12977  fz0to4untppr  13601  s4fv0  14843  01sqrexlem7  15192  sqrt9  15217  ef01bndlem  16124  cos2bnd  16128  sin01gt0  16130  cos01gt0  16131  rpnnen2lem3  16156  rpnnen2lem4  16157  rpnnen2lem9  16162  flodddiv4  16353  43prm  17052  slotsdifunifndx  17343  cnfldfunALTOLD  20951  tangtx  26007  sincos6thpi  26017  pige3ALT  26021  log2cnv  26439  log2tlbnd  26440  ppiub  26697  bposlem2  26778  bposlem3  26779  bposlem4  26780  bposlem5  26781  lgsdir2lem1  26818  dchrvmasumiflem1  26994  tgcgr4  27772  frgrogt3nreg  29640  friendshipgt3  29641  ex-gcd  29700  cyc3fv3  32286  cyc3conja  32304  hgt750lemd  33649  hgt750lem2  33653  heiborlem5  36672  heiborlem7  36674  3lexlogpow5ineq2  40909  3lexlogpow5ineq4  40910  3lexlogpow5ineq3  40911  3lexlogpow2ineq1  40912  3lexlogpow2ineq2  40913  3lexlogpow5ineq5  40914  aks4d1lem1  40916  aks4d1p1p6  40927  aks4d1p1p5  40929  aks4d1p1  40930  aks4d1p2  40931  aks4d1p3  40932  aks4d1p5  40934  aks4d1p6  40935  aks4d1p7d1  40936  aks4d1p7  40937  aks4d1p8  40941  aks4d1p9  40942  acos1half  41019  jm2.23  41721  stoweidlem13  44716  stoweidlem26  44729  stoweidlem34  44737  stoweidlem42  44745  stoweidlem59  44762  stoweid  44766  wallispilem4  44771  smfmullem4  45497  257prm  46216  127prm  46254  nfermltl2rev  46398  sepfsepc  47514