Theorem 2pos 12076

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 10976	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11497	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11517	. 2 ⊢ 0 < (1 + 1)
4		df-2 12036	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5106	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5079  (class class class)co 7271  0cc0 10872  1c1 10873   + caddc 10875   < clt 11010  2c2 12028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-mulcom 10936  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-i2m1 10940  ax-1ne0 10941  ax-1rid 10942  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945  ax-pre-lttri 10946  ax-pre-lttrn 10947  ax-pre-ltadd 10948  ax-pre-mulgt0 10949

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-riota 7228  df-ov 7274  df-oprab 7275  df-mpo 7276  df-er 8481  df-en 8717  df-dom 8718  df-sdom 8719  df-pnf 11012  df-mnf 11013  df-xr 11014  df-ltxr 11015  df-le 11016  df-sub 11207  df-neg 11208  df-2 12036

This theorem is referenced by:  2ne0  12077  3pos  12078  halfgt0  12189  halflt1  12191  halfpos2  12202  halfnneg2  12204  nominpos  12210  avglt1  12211  avglt2  12212  nn0n0n1ge2b  12301  3halfnz  12399  2rp  12734  hashgt23el  14137  s3fv0  14602  sqreulem  15069  cos2bnd  15895  sin02gt0  15899  sincos2sgn  15901  sin4lt0  15902  epos  15914  sqrt2re  15957  nnoddm1d2  16093  2mulprm  16396  prmgaplem7  16756  slotsdifdsndx  17102  odrngstr  17111  imasvalstr  17160  psgnunilem2  19101  cnfldstr  20597  cnfldfunOLD  20608  bl2in  23551  iihalf1  24092  iihalf2  24094  pcoass  24185  tcphcphlem1  24397  trirn  24562  minveclem2  24588  minveclem4  24594  ovolunlem1a  24658  vitalilem4  24773  mbfi1fseqlem5  24882  pilem2  25609  pilem3  25610  pipos  25615  sinhalfpilem  25618  sincosq1lem  25652  tangtx  25660  sinq12gt0  25662  sincos6thpi  25670  cosordlem  25684  tanord1  25691  efif1olem2  25697  efif1olem4  25699  cxpcn3lem  25898  ang180lem1  25957  ang180lem2  25958  atantan  26071  atanbndlem  26073  atans2  26079  leibpi  26090  log2tlbnd  26093  basellem1  26228  basellem2  26229  basellem3  26230  ppiltx  26324  ppiub  26350  chtublem  26357  chtub  26358  chpval2  26364  bcmono  26423  bpos1lem  26428  bposlem1  26430  bposlem2  26431  bposlem3  26432  bposlem4  26433  bposlem5  26434  bposlem6  26435  bposlem7  26436  gausslemma2dlem0c  26504  gausslemma2dlem1a  26511  gausslemma2dlem2  26513  gausslemma2dlem3  26514  lgseisenlem1  26521  lgseisenlem2  26522  lgseisenlem3  26523  lgsquadlem1  26526  lgsquadlem2  26527  2lgslem1a1  26535  2lgslem1a2  26536  2lgslem1c  26539  chebbnd1lem1  26615  chebbnd1lem2  26616  chebbnd1lem3  26617  chebbnd1  26618  chtppilimlem1  26619  chtppilimlem2  26620  chtppilim  26621  chebbnd2  26623  chto1lb  26624  chpchtlim  26625  chpo1ub  26626  dchrisum0fno1  26657  mulog2sumlem2  26681  selberglem2  26692  selberg2lem  26696  chpdifbndlem1  26699  logdivbnd  26702  pntrsumo1  26711  pntpbnd1a  26731  pntlemh  26745  pntlemr  26748  pntlemk  26752  pntlemo  26753  pnt2  26759  umgrislfupgrlem  27490  lfgrnloop  27493  lfuhgr1v0e  27619  wwlksnextwrd  28258  wwlksnextfun  28259  wwlksnextinj  28260  clwlkclwwlklem2a2  28353  konigsberg  28617  ex-fl  28807  minvecolem2  29233  minvecolem4  29238  bcsiALT  29537  opsqrlem6  30503  cdj3lem1  30792  wrdt2ind  31221  cyc2fv2  31385  sqsscirc1  31854  omssubadd  32263  signslema  32537  hgt750lem  32627  subfacval3  33147  nn0prpwlem  34507  knoppndvlem18  34705  knoppndvlem19  34706  knoppndvlem21  34708  cnndvlem1  34713  iccioo01  35494  sin2h  35763  cos2h  35764  tan2h  35765  itg2addnclem  35824  3lexlogpow5ineq2  40060  3lexlogpow5ineq4  40061  3lexlogpow5ineq3  40062  3lexlogpow2ineq1  40063  3lexlogpow2ineq2  40064  3lexlogpow5ineq5  40065  aks4d1lem1  40067  aks4d1p1p3  40074  aks4d1p1p2  40075  aks4d1p1p4  40076  aks4d1p1p6  40078  aks4d1p1p7  40079  aks4d1p1p5  40080  aks4d1p1  40081  aks4d1p2  40082  aks4d1p3  40083  aks4d1p5  40085  aks4d1p6  40086  aks4d1p7d1  40087  aks4d1p7  40088  aks4d1p8  40092  aks4d1p9  40093  2ap1caineq  40098  oexpreposd  40318  pellfundex  40705  jm2.22  40814  jm2.23  40815  imo72b2lem0  41746  sumnnodd  43142  sinaover2ne0  43380  stoweidlem14  43526  stoweidlem49  43561  stoweidlem52  43564  wallispilem4  43580  wallispi2lem2  43584  stirlinglem6  43591  stirlinglem15  43600  stirlingr  43602  dirkerval2  43606  dirkertrigeqlem3  43612  dirkercncflem4  43618  fourierdlem24  43643  fourierdlem79  43697  fourierdlem103  43721  fourierdlem104  43722  fourierdlem112  43730  fourierswlem  43742  fouriersw  43743  lighneallem4a  45029  nnoALTV  45116  nn0oALTV  45117  nn0e  45118  nneven  45119  evengpoap3  45220  nn0eo  45843  flnn0div2ge  45848  fldivexpfllog2  45880  fllog2  45883  blennngt2o2  45907  dignn0flhalf  45933  sepfsepc  46190