Theorem 2pos 12369

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 11261	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11785	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11805	. 2 ⊢ 0 < (1 + 1)
4		df-2 12329	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5170	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5143  (class class class)co 7431  0cc0 11155  1c1 11156   + caddc 11158   < clt 11295  2c2 12321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-2 12329

This theorem is referenced by:  2ne0  12370  3pos  12371  halfgt0  12482  halflt1  12484  halfpos2  12495  halfnneg2  12497  nominpos  12503  avglt1  12504  avglt2  12505  nn0n0n1ge2b  12595  3halfnz  12697  2rp  13039  hashgt23el  14463  s3fv0  14930  sqreulem  15398  cos2bnd  16224  sin02gt0  16228  sincos2sgn  16230  sin4lt0  16231  epos  16243  sqrt2re  16286  nnoddm1d2  16423  2mulprm  16730  prmgaplem7  17095  slotsdifdsndx  17438  odrngstr  17447  imasvalstr  17496  psgnunilem2  19513  cnfldstr  21366  cnfldstrOLD  21381  cnfldfunALTOLDOLD  21393  bl2in  24410  iihalf1  24958  iihalf2  24961  pcoass  25057  tcphcphlem1  25269  trirn  25434  minveclem2  25460  minveclem4  25466  ovolunlem1a  25531  vitalilem4  25646  mbfi1fseqlem5  25754  pilem2  26496  pilem3  26497  pipos  26502  sinhalfpilem  26505  sincosq1lem  26539  tangtx  26547  sinq12gt0  26549  tan4thpi  26556  sincos6thpi  26558  cosordlem  26572  tanord1  26579  efif1olem2  26585  efif1olem4  26587  cxpcn3lem  26790  ang180lem1  26852  ang180lem2  26853  atantan  26966  atanbndlem  26968  atans2  26974  leibpi  26985  log2tlbnd  26988  basellem1  27124  basellem2  27125  basellem3  27126  ppiltx  27220  ppiub  27248  chtublem  27255  chtub  27256  chpval2  27262  bcmono  27321  bpos1lem  27326  bposlem1  27328  bposlem2  27329  bposlem3  27330  bposlem4  27331  bposlem5  27332  bposlem6  27333  bposlem7  27334  gausslemma2dlem0c  27402  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  gausslemma2dlem3  27412  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgsquadlem1  27424  lgsquadlem2  27425  2lgslem1a1  27433  2lgslem1a2  27434  2lgslem1c  27437  chebbnd1lem1  27513  chebbnd1lem2  27514  chebbnd1lem3  27515  chebbnd1  27516  chtppilimlem1  27517  chtppilimlem2  27518  chtppilim  27519  chebbnd2  27521  chto1lb  27522  chpchtlim  27523  chpo1ub  27524  dchrisum0fno1  27555  mulog2sumlem2  27579  selberglem2  27590  selberg2lem  27594  chpdifbndlem1  27597  logdivbnd  27600  pntrsumo1  27609  pntpbnd1a  27629  pntlemh  27643  pntlemr  27646  pntlemk  27650  pntlemo  27651  pnt2  27657  umgrislfupgrlem  29139  lfgrnloop  29142  lfuhgr1v0e  29271  wwlksnextwrd  29917  wwlksnextfun  29918  wwlksnextinj  29919  clwlkclwwlklem2a2  30012  konigsberg  30276  ex-fl  30466  minvecolem2  30894  minvecolem4  30899  bcsiALT  31198  opsqrlem6  32164  cdj3lem1  32453  wrdt2ind  32938  cyc2fv2  33142  rtelextdg2lem  33767  2sqr3minply  33791  sqsscirc1  33907  omssubadd  34302  signslema  34577  hgt750lem  34666  subfacval3  35194  nn0prpwlem  36323  knoppndvlem18  36530  knoppndvlem19  36531  knoppndvlem21  36533  cnndvlem1  36538  iccioo01  37328  sin2h  37617  cos2h  37618  tan2h  37619  itg2addnclem  37678  3lexlogpow5ineq2  42056  3lexlogpow5ineq4  42057  3lexlogpow5ineq3  42058  3lexlogpow2ineq1  42059  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1lem1  42063  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p2  42078  aks4d1p3  42079  aks4d1p5  42081  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8  42088  aks4d1p9  42089  posbezout  42101  aks6d1c3  42124  2ap1caineq  42146  aks6d1c6lem4  42174  aks6d1c7lem1  42181  aks6d1c7lem2  42182  oexpreposd  42357  asin1half  42387  pellfundex  42897  jm2.22  43007  jm2.23  43008  imo72b2lem0  44178  sumnnodd  45645  sinaover2ne0  45883  stoweidlem14  46029  stoweidlem49  46064  stoweidlem52  46067  wallispilem4  46083  wallispi2lem2  46087  stirlinglem6  46094  stirlinglem15  46103  stirlingr  46105  dirkerval2  46109  dirkertrigeqlem3  46115  dirkercncflem4  46121  fourierdlem24  46146  fourierdlem79  46200  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierswlem  46245  fouriersw  46246  lighneallem4a  47595  nnoALTV  47682  nn0oALTV  47683  nn0e  47684  nneven  47685  evengpoap3  47786  2ltceilhalf  48015  2tceilhalfelfzo1  48018  gpg3kgrtriexlem1  48039  nn0eo  48449  flnn0div2ge  48454  fldivexpfllog2  48486  fllog2  48489  blennngt2o2  48513  dignn0flhalf  48539  sepfsepc  48825