Theorem 2pos 12248

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 11132	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11659	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11679	. 2 ⊢ 0 < (1 + 1)
4		df-2 12208	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5125	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5098  (class class class)co 7358  0cc0 11026  1c1 11027   + caddc 11029   < clt 11166  2c2 12200

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-2 12208

This theorem is referenced by:  3pos  12250  halfgt0  12356  halflt1  12358  halfpos2  12370  halfnneg2  12372  nominpos  12378  avglt1  12379  avglt2  12380  nn0n0n1ge2b  12470  3halfnz  12571  2rp  12910  hashgt23el  14347  s3fv0  14814  sqreulem  15283  cos2bnd  16113  sin02gt0  16117  sincos2sgn  16119  sin4lt0  16120  epos  16132  sqrt2re  16175  nnoddm1d2  16313  2mulprm  16620  prmgaplem7  16985  slotsdifdsndx  17314  odrngstr  17323  imasvalstr  17371  psgnunilem2  19424  cnfldstr  21311  cnfldstrOLD  21326  bl2in  24344  iihalf1  24881  iihalf2  24884  pcoass  24980  tcphcphlem1  25191  trirn  25356  minveclem2  25382  minveclem4  25388  ovolunlem1a  25453  vitalilem4  25568  mbfi1fseqlem5  25676  pilem2  26418  pilem3  26419  pipos  26424  sinhalfpilem  26428  sincosq1lem  26462  tangtx  26470  sinq12gt0  26472  tan4thpi  26479  sincos6thpi  26481  cosordlem  26495  tanord1  26502  efif1olem2  26508  efif1olem4  26510  cxpcn3lem  26713  ang180lem1  26775  ang180lem2  26776  atantan  26889  atanbndlem  26891  atans2  26897  leibpi  26908  log2tlbnd  26911  basellem1  27047  basellem2  27048  basellem3  27049  ppiltx  27143  ppiub  27171  chtublem  27178  chtub  27179  chpval2  27185  bcmono  27244  bpos1lem  27249  bposlem1  27251  bposlem2  27252  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem6  27256  bposlem7  27257  gausslemma2dlem0c  27325  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  gausslemma2dlem3  27335  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgsquadlem1  27347  lgsquadlem2  27348  2lgslem1a1  27356  2lgslem1a2  27357  2lgslem1c  27360  chebbnd1lem1  27436  chebbnd1lem2  27437  chebbnd1lem3  27438  chebbnd1  27439  chtppilimlem1  27440  chtppilimlem2  27441  chtppilim  27442  chebbnd2  27444  chto1lb  27445  chpchtlim  27446  chpo1ub  27447  dchrisum0fno1  27478  mulog2sumlem2  27502  selberglem2  27513  selberg2lem  27517  chpdifbndlem1  27520  logdivbnd  27523  pntrsumo1  27532  pntpbnd1a  27552  pntlemh  27566  pntlemr  27569  pntlemk  27573  pntlemo  27574  pnt2  27580  umgrislfupgrlem  29195  lfgrnloop  29198  lfuhgr1v0e  29327  wwlksnextwrd  29970  wwlksnextfun  29971  wwlksnextinj  29972  clwlkclwwlklem2a2  30068  konigsberg  30332  ex-fl  30522  minvecolem2  30950  minvecolem4  30955  bcsiALT  31254  opsqrlem6  32220  cdj3lem1  32509  wrdt2ind  33035  cyc2fv2  33204  rtelextdg2lem  33883  2sqr3minply  33937  sqsscirc1  34065  omssubadd  34457  signslema  34719  hgt750lem  34808  subfacval3  35383  nn0prpwlem  36516  knoppndvlem18  36729  knoppndvlem19  36730  knoppndvlem21  36732  cnndvlem1  36737  iccioo01  37528  sin2h  37807  cos2h  37808  tan2h  37809  itg2addnclem  37868  3lexlogpow5ineq2  42305  3lexlogpow5ineq4  42306  3lexlogpow5ineq3  42307  3lexlogpow2ineq1  42308  3lexlogpow2ineq2  42309  3lexlogpow5ineq5  42310  aks4d1lem1  42312  aks4d1p1p3  42319  aks4d1p1p2  42320  aks4d1p1p4  42321  aks4d1p1p6  42323  aks4d1p1p7  42324  aks4d1p1p5  42325  aks4d1p1  42326  aks4d1p2  42327  aks4d1p3  42328  aks4d1p5  42330  aks4d1p6  42331  aks4d1p7d1  42332  aks4d1p7  42333  aks4d1p8  42337  aks4d1p9  42338  posbezout  42350  aks6d1c3  42373  2ap1caineq  42395  aks6d1c6lem4  42423  aks6d1c7lem1  42430  aks6d1c7lem2  42431  oexpreposd  42573  asin1half  42608  pellfundex  43124  jm2.22  43233  jm2.23  43234  imo72b2lem0  44402  sumnnodd  45872  sinaover2ne0  46108  stoweidlem14  46254  stoweidlem49  46289  stoweidlem52  46292  wallispilem4  46308  wallispi2lem2  46312  stirlinglem6  46319  stirlinglem15  46328  stirlingr  46330  dirkerval2  46334  dirkertrigeqlem3  46340  dirkercncflem4  46346  fourierdlem24  46371  fourierdlem79  46425  fourierdlem103  46449  fourierdlem104  46450  fourierdlem112  46458  fourierswlem  46470  fouriersw  46471  nthrucw  47126  2ltceilhalf  47570  2tceilhalfelfzo1  47574  lighneallem4a  47850  nnoALTV  47937  nn0oALTV  47938  nn0e  47939  nneven  47940  evengpoap3  48041  gpg3kgrtriexlem1  48325  nn0eo  48770  flnn0div2ge  48775  fldivexpfllog2  48807  fllog2  48810  blennngt2o2  48834  dignn0flhalf  48860  sepfsepc  49169