Theorem 2pos 12343

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 11235	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11759	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11779	. 2 ⊢ 0 < (1 + 1)
4		df-2 12303	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5146	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5119  (class class class)co 7405  0cc0 11129  1c1 11130   + caddc 11132   < clt 11269  2c2 12295

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 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-2 12303

This theorem is referenced by:  3pos  12345  halfgt0  12456  halflt1  12458  halfpos2  12470  halfnneg2  12472  nominpos  12478  avglt1  12479  avglt2  12480  nn0n0n1ge2b  12570  3halfnz  12672  2rp  13013  hashgt23el  14442  s3fv0  14910  sqreulem  15378  cos2bnd  16206  sin02gt0  16210  sincos2sgn  16212  sin4lt0  16213  epos  16225  sqrt2re  16268  nnoddm1d2  16405  2mulprm  16712  prmgaplem7  17077  slotsdifdsndx  17408  odrngstr  17417  imasvalstr  17465  psgnunilem2  19476  cnfldstr  21317  cnfldstrOLD  21332  bl2in  24339  iihalf1  24876  iihalf2  24879  pcoass  24975  tcphcphlem1  25187  trirn  25352  minveclem2  25378  minveclem4  25384  ovolunlem1a  25449  vitalilem4  25564  mbfi1fseqlem5  25672  pilem2  26414  pilem3  26415  pipos  26420  sinhalfpilem  26424  sincosq1lem  26458  tangtx  26466  sinq12gt0  26468  tan4thpi  26475  sincos6thpi  26477  cosordlem  26491  tanord1  26498  efif1olem2  26504  efif1olem4  26506  cxpcn3lem  26709  ang180lem1  26771  ang180lem2  26772  atantan  26885  atanbndlem  26887  atans2  26893  leibpi  26904  log2tlbnd  26907  basellem1  27043  basellem2  27044  basellem3  27045  ppiltx  27139  ppiub  27167  chtublem  27174  chtub  27175  chpval2  27181  bcmono  27240  bpos1lem  27245  bposlem1  27247  bposlem2  27248  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem7  27253  gausslemma2dlem0c  27321  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  gausslemma2dlem3  27331  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgsquadlem1  27343  lgsquadlem2  27344  2lgslem1a1  27352  2lgslem1a2  27353  2lgslem1c  27356  chebbnd1lem1  27432  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  chtppilimlem2  27437  chtppilim  27438  chebbnd2  27440  chto1lb  27441  chpchtlim  27442  chpo1ub  27443  dchrisum0fno1  27474  mulog2sumlem2  27498  selberglem2  27509  selberg2lem  27513  chpdifbndlem1  27516  logdivbnd  27519  pntrsumo1  27528  pntpbnd1a  27548  pntlemh  27562  pntlemr  27565  pntlemk  27569  pntlemo  27570  pnt2  27576  umgrislfupgrlem  29101  lfgrnloop  29104  lfuhgr1v0e  29233  wwlksnextwrd  29879  wwlksnextfun  29880  wwlksnextinj  29881  clwlkclwwlklem2a2  29974  konigsberg  30238  ex-fl  30428  minvecolem2  30856  minvecolem4  30861  bcsiALT  31160  opsqrlem6  32126  cdj3lem1  32415  wrdt2ind  32929  cyc2fv2  33133  rtelextdg2lem  33760  2sqr3minply  33814  sqsscirc1  33939  omssubadd  34332  signslema  34594  hgt750lem  34683  subfacval3  35211  nn0prpwlem  36340  knoppndvlem18  36547  knoppndvlem19  36548  knoppndvlem21  36550  cnndvlem1  36555  iccioo01  37345  sin2h  37634  cos2h  37635  tan2h  37636  itg2addnclem  37695  3lexlogpow5ineq2  42068  3lexlogpow5ineq4  42069  3lexlogpow5ineq3  42070  3lexlogpow2ineq1  42071  3lexlogpow2ineq2  42072  3lexlogpow5ineq5  42073  aks4d1lem1  42075  aks4d1p1p3  42082  aks4d1p1p2  42083  aks4d1p1p4  42084  aks4d1p1p6  42086  aks4d1p1p7  42087  aks4d1p1p5  42088  aks4d1p1  42089  aks4d1p2  42090  aks4d1p3  42091  aks4d1p5  42093  aks4d1p6  42094  aks4d1p7d1  42095  aks4d1p7  42096  aks4d1p8  42100  aks4d1p9  42101  posbezout  42113  aks6d1c3  42136  2ap1caineq  42158  aks6d1c6lem4  42186  aks6d1c7lem1  42193  aks6d1c7lem2  42194  oexpreposd  42371  asin1half  42400  pellfundex  42909  jm2.22  43019  jm2.23  43020  imo72b2lem0  44189  sumnnodd  45659  sinaover2ne0  45897  stoweidlem14  46043  stoweidlem49  46078  stoweidlem52  46081  wallispilem4  46097  wallispi2lem2  46101  stirlinglem6  46108  stirlinglem15  46117  stirlingr  46119  dirkerval2  46123  dirkertrigeqlem3  46129  dirkercncflem4  46135  fourierdlem24  46160  fourierdlem79  46214  fourierdlem103  46238  fourierdlem104  46239  fourierdlem112  46247  fourierswlem  46259  fouriersw  46260  2ltceilhalf  47357  2tceilhalfelfzo1  47361  lighneallem4a  47622  nnoALTV  47709  nn0oALTV  47710  nn0e  47711  nneven  47712  evengpoap3  47813  gpg3kgrtriexlem1  48085  nn0eo  48508  flnn0div2ge  48513  fldivexpfllog2  48545  fllog2  48548  blennngt2o2  48572  dignn0flhalf  48598  sepfsepc  48902