Theorem 2pos 11553

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 10441	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 10965	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 10985	. 2 ⊢ 0 < (1 + 1)
4		df-2 11506	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 4957	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 4930  (class class class)co 6978  0cc0 10337  1c1 10338   + caddc 10340   < clt 10476  2c2 11498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-resscn 10394  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-mulcom 10401  ax-addass 10402  ax-mulass 10403  ax-distr 10404  ax-i2m1 10405  ax-1ne0 10406  ax-1rid 10407  ax-rnegex 10408  ax-rrecex 10409  ax-cnre 10410  ax-pre-lttri 10411  ax-pre-lttrn 10412  ax-pre-ltadd 10413  ax-pre-mulgt0 10414

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-po 5327  df-so 5328  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-riota 6939  df-ov 6981  df-oprab 6982  df-mpo 6983  df-er 8091  df-en 8309  df-dom 8310  df-sdom 8311  df-pnf 10478  df-mnf 10479  df-xr 10480  df-ltxr 10481  df-le 10482  df-sub 10674  df-neg 10675  df-2 11506

This theorem is referenced by:  2ne0  11554  3pos  11555  halfgt0  11666  halflt1  11668  halfpos2  11679  halfnneg2  11681  nominpos  11687  avglt1  11688  avglt2  11689  nn0n0n1ge2b  11778  3halfnz  11877  2rp  12212  hashgt23el  13601  s3fv0  14118  sqreulem  14583  cos2bnd  15404  sin02gt0  15408  sincos2sgn  15410  sin4lt0  15411  epos  15423  sqrt2re  15466  nnoddm1d2  15600  2mulprm  15896  prmgaplem7  16252  odrngstr  16538  imasvalstr  16584  psgnunilem2  18388  cnfldstr  20252  cnfldfun  20262  bl2in  22716  iihalf1  23241  iihalf2  23243  pcoass  23334  tcphcphlem1  23544  trirn  23709  minveclem2  23735  minveclem4  23741  ovolunlem1a  23803  vitalilem4  23918  mbfi1fseqlem5  24026  pilem2  24746  pilem3  24747  pipos  24752  sinhalfpilem  24755  sincosq1lem  24789  tangtx  24797  sinq12gt0  24799  sincos6thpi  24807  cosordlem  24819  tanord1  24825  efif1olem2  24831  efif1olem4  24833  cxpcn3lem  25032  ang180lem1  25091  ang180lem2  25092  atantan  25205  atanbndlem  25207  atans2  25213  leibpilem1OLD  25223  leibpi  25225  log2tlbnd  25228  basellem1  25363  basellem2  25364  basellem3  25365  ppiltx  25459  ppiub  25485  chtublem  25492  chtub  25493  chpval2  25499  bcmono  25558  bpos1lem  25563  bposlem1  25565  bposlem2  25566  bposlem3  25567  bposlem4  25568  bposlem5  25569  bposlem6  25570  bposlem7  25571  gausslemma2dlem0c  25639  gausslemma2dlem1a  25646  gausslemma2dlem2  25648  gausslemma2dlem3  25649  lgseisenlem1  25656  lgseisenlem2  25657  lgseisenlem3  25658  lgsquadlem1  25661  lgsquadlem2  25662  2lgslem1a1  25670  2lgslem1a2  25671  2lgslem1c  25674  chebbnd1lem1  25750  chebbnd1lem2  25751  chebbnd1lem3  25752  chebbnd1  25753  chtppilimlem1  25754  chtppilimlem2  25755  chtppilim  25756  chebbnd2  25758  chto1lb  25759  chpchtlim  25760  chpo1ub  25761  dchrisum0fno1  25792  mulog2sumlem2  25816  selberglem2  25827  selberg2lem  25831  chpdifbndlem1  25834  logdivbnd  25837  pntrsumo1  25846  pntpbnd1a  25866  pntlemh  25880  pntlemr  25883  pntlemk  25887  pntlemo  25888  pnt2  25894  umgrislfupgrlem  26613  lfgrnloop  26616  lfuhgr1v0e  26742  wwlksnextwrd  27391  wwlksnextfun  27392  wwlksnextinj  27393  wwlksnextwrdOLD  27396  wwlksnextfunOLD  27397  wwlksnextinjOLD  27398  clwlkclwwlklem2a2  27502  konigsberg  27792  ex-fl  28007  minvecolem2  28433  minvecolem4  28438  bcsiALT  28738  opsqrlem6  29706  cdj3lem1  29995  cycpm2cl  30452  cyc2fv2  30454  sqsscirc1  30795  omssubadd  31203  signslema  31478  hgt750lem  31570  subfacval3  32021  nn0prpwlem  33191  knoppndvlem18  33388  knoppndvlem19  33389  knoppndvlem21  33391  cnndvlem1  33396  sin2h  34323  cos2h  34324  tan2h  34325  itg2addnclem  34384  oexpreposd  38611  pellfundex  38879  jm2.22  38988  jm2.23  38989  imo72b2lem0  39880  sumnnodd  41343  sinaover2ne0  41580  stoweidlem14  41731  stoweidlem49  41766  stoweidlem52  41769  wallispilem4  41785  wallispi2lem2  41789  stirlinglem6  41796  stirlinglem15  41805  stirlingr  41807  dirkerval2  41811  dirkertrigeqlem3  41817  dirkercncflem4  41823  fourierdlem24  41848  fourierdlem79  41902  fourierdlem103  41926  fourierdlem104  41927  fourierdlem112  41935  fourierswlem  41947  fouriersw  41948  lighneallem4a  43142  nnoALTV  43229  nn0oALTV  43230  nn0e  43231  nneven  43232  evengpoap3  43333  nn0eo  43957  flnn0div2ge  43962  fldivexpfllog2  43994  fllog2  43997  blennngt2o2  44021  dignn0flhalf  44047