Theorem 2pos 11741

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 10641	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11162	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11182	. 2 ⊢ 0 < (1 + 1)
4		df-2 11701	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5093	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5066  (class class class)co 7156  0cc0 10537  1c1 10538   + caddc 10540   < clt 10675  2c2 11693

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-2 11701

This theorem is referenced by:  2ne0  11742  3pos  11743  halfgt0  11854  halflt1  11856  halfpos2  11867  halfnneg2  11869  nominpos  11875  avglt1  11876  avglt2  11877  nn0n0n1ge2b  11964  3halfnz  12062  2rp  12395  hashgt23el  13786  s3fv0  14253  sqreulem  14719  cos2bnd  15541  sin02gt0  15545  sincos2sgn  15547  sin4lt0  15548  epos  15560  sqrt2re  15603  nnoddm1d2  15737  2mulprm  16037  prmgaplem7  16393  odrngstr  16679  imasvalstr  16725  psgnunilem2  18623  cnfldstr  20547  cnfldfun  20557  bl2in  23010  iihalf1  23535  iihalf2  23537  pcoass  23628  tcphcphlem1  23838  trirn  24003  minveclem2  24029  minveclem4  24035  ovolunlem1a  24097  vitalilem4  24212  mbfi1fseqlem5  24320  pilem2  25040  pilem3  25041  pipos  25046  sinhalfpilem  25049  sincosq1lem  25083  tangtx  25091  sinq12gt0  25093  sincos6thpi  25101  cosordlem  25115  tanord1  25121  efif1olem2  25127  efif1olem4  25129  cxpcn3lem  25328  ang180lem1  25387  ang180lem2  25388  atantan  25501  atanbndlem  25503  atans2  25509  leibpi  25520  log2tlbnd  25523  basellem1  25658  basellem2  25659  basellem3  25660  ppiltx  25754  ppiub  25780  chtublem  25787  chtub  25788  chpval2  25794  bcmono  25853  bpos1lem  25858  bposlem1  25860  bposlem2  25861  bposlem3  25862  bposlem4  25863  bposlem5  25864  bposlem6  25865  bposlem7  25866  gausslemma2dlem0c  25934  gausslemma2dlem1a  25941  gausslemma2dlem2  25943  gausslemma2dlem3  25944  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgsquadlem1  25956  lgsquadlem2  25957  2lgslem1a1  25965  2lgslem1a2  25966  2lgslem1c  25969  chebbnd1lem1  26045  chebbnd1lem2  26046  chebbnd1lem3  26047  chebbnd1  26048  chtppilimlem1  26049  chtppilimlem2  26050  chtppilim  26051  chebbnd2  26053  chto1lb  26054  chpchtlim  26055  chpo1ub  26056  dchrisum0fno1  26087  mulog2sumlem2  26111  selberglem2  26122  selberg2lem  26126  chpdifbndlem1  26129  logdivbnd  26132  pntrsumo1  26141  pntpbnd1a  26161  pntlemh  26175  pntlemr  26178  pntlemk  26182  pntlemo  26183  pnt2  26189  umgrislfupgrlem  26907  lfgrnloop  26910  lfuhgr1v0e  27036  wwlksnextwrd  27675  wwlksnextfun  27676  wwlksnextinj  27677  clwlkclwwlklem2a2  27771  konigsberg  28036  ex-fl  28226  minvecolem2  28652  minvecolem4  28657  bcsiALT  28956  opsqrlem6  29922  cdj3lem1  30211  wrdt2ind  30627  cyc2fv2  30764  sqsscirc1  31151  omssubadd  31558  signslema  31832  hgt750lem  31922  subfacval3  32436  nn0prpwlem  33670  knoppndvlem18  33868  knoppndvlem19  33869  knoppndvlem21  33871  cnndvlem1  33876  sin2h  34897  cos2h  34898  tan2h  34899  itg2addnclem  34958  oexpreposd  39228  pellfundex  39532  jm2.22  39641  jm2.23  39642  imo72b2lem0  40565  sumnnodd  41960  sinaover2ne0  42198  stoweidlem14  42348  stoweidlem49  42383  stoweidlem52  42386  wallispilem4  42402  wallispi2lem2  42406  stirlinglem6  42413  stirlinglem15  42422  stirlingr  42424  dirkerval2  42428  dirkertrigeqlem3  42434  dirkercncflem4  42440  fourierdlem24  42465  fourierdlem79  42519  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  fourierswlem  42564  fouriersw  42565  lighneallem4a  43822  nnoALTV  43909  nn0oALTV  43910  nn0e  43911  nneven  43912  evengpoap3  44013  nn0eo  44637  flnn0div2ge  44642  fldivexpfllog2  44674  fllog2  44677  blennngt2o2  44701  dignn0flhalf  44727