Theorem 2pos 12289

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 11174	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11700	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11720	. 2 ⊢ 0 < (1 + 1)
4		df-2 12249	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5134	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5107  (class class class)co 7387  0cc0 11068  1c1 11069   + caddc 11071   < clt 11208  2c2 12241

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-2 12249

This theorem is referenced by:  3pos  12291  halfgt0  12397  halflt1  12399  halfpos2  12411  halfnneg2  12413  nominpos  12419  avglt1  12420  avglt2  12421  nn0n0n1ge2b  12511  3halfnz  12613  2rp  12956  hashgt23el  14389  s3fv0  14857  sqreulem  15326  cos2bnd  16156  sin02gt0  16160  sincos2sgn  16162  sin4lt0  16163  epos  16175  sqrt2re  16218  nnoddm1d2  16356  2mulprm  16663  prmgaplem7  17028  slotsdifdsndx  17357  odrngstr  17366  imasvalstr  17414  psgnunilem2  19425  cnfldstr  21266  cnfldstrOLD  21281  bl2in  24288  iihalf1  24825  iihalf2  24828  pcoass  24924  tcphcphlem1  25135  trirn  25300  minveclem2  25326  minveclem4  25332  ovolunlem1a  25397  vitalilem4  25512  mbfi1fseqlem5  25620  pilem2  26362  pilem3  26363  pipos  26368  sinhalfpilem  26372  sincosq1lem  26406  tangtx  26414  sinq12gt0  26416  tan4thpi  26423  sincos6thpi  26425  cosordlem  26439  tanord1  26446  efif1olem2  26452  efif1olem4  26454  cxpcn3lem  26657  ang180lem1  26719  ang180lem2  26720  atantan  26833  atanbndlem  26835  atans2  26841  leibpi  26852  log2tlbnd  26855  basellem1  26991  basellem2  26992  basellem3  26993  ppiltx  27087  ppiub  27115  chtublem  27122  chtub  27123  chpval2  27129  bcmono  27188  bpos1lem  27193  bposlem1  27195  bposlem2  27196  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem7  27201  gausslemma2dlem0c  27269  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem3  27279  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgsquadlem1  27291  lgsquadlem2  27292  2lgslem1a1  27300  2lgslem1a2  27301  2lgslem1c  27304  chebbnd1lem1  27380  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem1  27384  chtppilimlem2  27385  chtppilim  27386  chebbnd2  27388  chto1lb  27389  chpchtlim  27390  chpo1ub  27391  dchrisum0fno1  27422  mulog2sumlem2  27446  selberglem2  27457  selberg2lem  27461  chpdifbndlem1  27464  logdivbnd  27467  pntrsumo1  27476  pntpbnd1a  27496  pntlemh  27510  pntlemr  27513  pntlemk  27517  pntlemo  27518  pnt2  27524  umgrislfupgrlem  29049  lfgrnloop  29052  lfuhgr1v0e  29181  wwlksnextwrd  29827  wwlksnextfun  29828  wwlksnextinj  29829  clwlkclwwlklem2a2  29922  konigsberg  30186  ex-fl  30376  minvecolem2  30804  minvecolem4  30809  bcsiALT  31108  opsqrlem6  32074  cdj3lem1  32363  wrdt2ind  32875  cyc2fv2  33079  rtelextdg2lem  33716  2sqr3minply  33770  sqsscirc1  33898  omssubadd  34291  signslema  34553  hgt750lem  34642  subfacval3  35176  nn0prpwlem  36310  knoppndvlem18  36517  knoppndvlem19  36518  knoppndvlem21  36520  cnndvlem1  36525  iccioo01  37315  sin2h  37604  cos2h  37605  tan2h  37606  itg2addnclem  37665  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  aks6d1c3  42111  2ap1caineq  42133  aks6d1c6lem4  42161  aks6d1c7lem1  42168  aks6d1c7lem2  42169  oexpreposd  42310  asin1half  42345  pellfundex  42874  jm2.22  42984  jm2.23  42985  imo72b2lem0  44154  sumnnodd  45628  sinaover2ne0  45866  stoweidlem14  46012  stoweidlem49  46047  stoweidlem52  46050  wallispilem4  46066  wallispi2lem2  46070  stirlinglem6  46077  stirlinglem15  46086  stirlingr  46088  dirkerval2  46092  dirkertrigeqlem3  46098  dirkercncflem4  46104  fourierdlem24  46129  fourierdlem79  46183  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierswlem  46228  fouriersw  46229  2ltceilhalf  47329  2tceilhalfelfzo1  47333  lighneallem4a  47609  nnoALTV  47696  nn0oALTV  47697  nn0e  47698  nneven  47699  evengpoap3  47800  gpg3kgrtriexlem1  48074  nn0eo  48517  flnn0div2ge  48522  fldivexpfllog2  48554  fllog2  48557  blennngt2o2  48581  dignn0flhalf  48607  sepfsepc  48916