Theorem 2pos 12225

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 11109	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11636	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11656	. 2 ⊢ 0 < (1 + 1)
4		df-2 12185	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5118	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5091  (class class class)co 7346  0cc0 11003  1c1 11004   + caddc 11006   < clt 11143  2c2 12177

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-resscn 11060  ax-1cn 11061  ax-icn 11062  ax-addcl 11063  ax-addrcl 11064  ax-mulcl 11065  ax-mulrcl 11066  ax-mulcom 11067  ax-addass 11068  ax-mulass 11069  ax-distr 11070  ax-i2m1 11071  ax-1ne0 11072  ax-1rid 11073  ax-rnegex 11074  ax-rrecex 11075  ax-cnre 11076  ax-pre-lttri 11077  ax-pre-lttrn 11078  ax-pre-ltadd 11079  ax-pre-mulgt0 11080

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-po 5524  df-so 5525  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11145  df-mnf 11146  df-xr 11147  df-ltxr 11148  df-le 11149  df-sub 11343  df-neg 11344  df-2 12185

This theorem is referenced by:  3pos  12227  halfgt0  12333  halflt1  12335  halfpos2  12347  halfnneg2  12349  nominpos  12355  avglt1  12356  avglt2  12357  nn0n0n1ge2b  12447  3halfnz  12549  2rp  12892  hashgt23el  14328  s3fv0  14795  sqreulem  15264  cos2bnd  16094  sin02gt0  16098  sincos2sgn  16100  sin4lt0  16101  epos  16113  sqrt2re  16156  nnoddm1d2  16294  2mulprm  16601  prmgaplem7  16966  slotsdifdsndx  17295  odrngstr  17304  imasvalstr  17352  psgnunilem2  19405  cnfldstr  21291  cnfldstrOLD  21306  bl2in  24313  iihalf1  24850  iihalf2  24853  pcoass  24949  tcphcphlem1  25160  trirn  25325  minveclem2  25351  minveclem4  25357  ovolunlem1a  25422  vitalilem4  25537  mbfi1fseqlem5  25645  pilem2  26387  pilem3  26388  pipos  26393  sinhalfpilem  26397  sincosq1lem  26431  tangtx  26439  sinq12gt0  26441  tan4thpi  26448  sincos6thpi  26450  cosordlem  26464  tanord1  26471  efif1olem2  26477  efif1olem4  26479  cxpcn3lem  26682  ang180lem1  26744  ang180lem2  26745  atantan  26858  atanbndlem  26860  atans2  26866  leibpi  26877  log2tlbnd  26880  basellem1  27016  basellem2  27017  basellem3  27018  ppiltx  27112  ppiub  27140  chtublem  27147  chtub  27148  chpval2  27154  bcmono  27213  bpos1lem  27218  bposlem1  27220  bposlem2  27221  bposlem3  27222  bposlem4  27223  bposlem5  27224  bposlem6  27225  bposlem7  27226  gausslemma2dlem0c  27294  gausslemma2dlem1a  27301  gausslemma2dlem2  27303  gausslemma2dlem3  27304  lgseisenlem1  27311  lgseisenlem2  27312  lgseisenlem3  27313  lgsquadlem1  27316  lgsquadlem2  27317  2lgslem1a1  27325  2lgslem1a2  27326  2lgslem1c  27329  chebbnd1lem1  27405  chebbnd1lem2  27406  chebbnd1lem3  27407  chebbnd1  27408  chtppilimlem1  27409  chtppilimlem2  27410  chtppilim  27411  chebbnd2  27413  chto1lb  27414  chpchtlim  27415  chpo1ub  27416  dchrisum0fno1  27447  mulog2sumlem2  27471  selberglem2  27482  selberg2lem  27486  chpdifbndlem1  27489  logdivbnd  27492  pntrsumo1  27501  pntpbnd1a  27521  pntlemh  27535  pntlemr  27538  pntlemk  27542  pntlemo  27543  pnt2  27549  umgrislfupgrlem  29098  lfgrnloop  29101  lfuhgr1v0e  29230  wwlksnextwrd  29873  wwlksnextfun  29874  wwlksnextinj  29875  clwlkclwwlklem2a2  29968  konigsberg  30232  ex-fl  30422  minvecolem2  30850  minvecolem4  30855  bcsiALT  31154  opsqrlem6  32120  cdj3lem1  32409  wrdt2ind  32929  cyc2fv2  33086  rtelextdg2lem  33734  2sqr3minply  33788  sqsscirc1  33916  omssubadd  34308  signslema  34570  hgt750lem  34659  subfacval3  35221  nn0prpwlem  36355  knoppndvlem18  36562  knoppndvlem19  36563  knoppndvlem21  36565  cnndvlem1  36570  iccioo01  37360  sin2h  37649  cos2h  37650  tan2h  37651  itg2addnclem  37710  3lexlogpow5ineq2  42087  3lexlogpow5ineq4  42088  3lexlogpow5ineq3  42089  3lexlogpow2ineq1  42090  3lexlogpow2ineq2  42091  3lexlogpow5ineq5  42092  aks4d1lem1  42094  aks4d1p1p3  42101  aks4d1p1p2  42102  aks4d1p1p4  42103  aks4d1p1p6  42105  aks4d1p1p7  42106  aks4d1p1p5  42107  aks4d1p1  42108  aks4d1p2  42109  aks4d1p3  42110  aks4d1p5  42112  aks4d1p6  42113  aks4d1p7d1  42114  aks4d1p7  42115  aks4d1p8  42119  aks4d1p9  42120  posbezout  42132  aks6d1c3  42155  2ap1caineq  42177  aks6d1c6lem4  42205  aks6d1c7lem1  42212  aks6d1c7lem2  42213  oexpreposd  42354  asin1half  42389  pellfundex  42918  jm2.22  43027  jm2.23  43028  imo72b2lem0  44197  sumnnodd  45669  sinaover2ne0  45905  stoweidlem14  46051  stoweidlem49  46086  stoweidlem52  46089  wallispilem4  46105  wallispi2lem2  46109  stirlinglem6  46116  stirlinglem15  46125  stirlingr  46127  dirkerval2  46131  dirkertrigeqlem3  46137  dirkercncflem4  46143  fourierdlem24  46168  fourierdlem79  46222  fourierdlem103  46246  fourierdlem104  46247  fourierdlem112  46255  fourierswlem  46267  fouriersw  46268  2ltceilhalf  47358  2tceilhalfelfzo1  47362  lighneallem4a  47638  nnoALTV  47725  nn0oALTV  47726  nn0e  47727  nneven  47728  evengpoap3  47829  gpg3kgrtriexlem1  48113  nn0eo  48559  flnn0div2ge  48564  fldivexpfllog2  48596  fllog2  48599  blennngt2o2  48623  dignn0flhalf  48649  sepfsepc  48958