Theorem 2pos 12360

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 11254	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11776	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11796	. 2 ⊢ 0 < (1 + 1)
4		df-2 12320	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5172	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5145  (class class class)co 7415  0cc0 11148  1c1 11149   + caddc 11151   < clt 11288  2c2 12312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7737  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3366  df-rab 3421  df-v 3466  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4325  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4908  df-br 5146  df-opab 5208  df-mpt 5229  df-id 5572  df-po 5586  df-so 5587  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6497  df-fun 6547  df-fn 6548  df-f 6549  df-f1 6550  df-fo 6551  df-f1o 6552  df-fv 6553  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-er 8725  df-en 8966  df-dom 8967  df-sdom 8968  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-2 12320

This theorem is referenced by:  2ne0  12361  3pos  12362  halfgt0  12473  halflt1  12475  halfpos2  12486  halfnneg2  12488  nominpos  12494  avglt1  12495  avglt2  12496  nn0n0n1ge2b  12585  3halfnz  12686  2rp  13026  hashgt23el  14435  s3fv0  14894  sqreulem  15358  cos2bnd  16184  sin02gt0  16188  sincos2sgn  16190  sin4lt0  16191  epos  16203  sqrt2re  16246  nnoddm1d2  16382  2mulprm  16688  prmgaplem7  17053  slotsdifdsndx  17402  odrngstr  17411  imasvalstr  17460  psgnunilem2  19488  cnfldstr  21340  cnfldstrOLD  21355  cnfldfunALTOLDOLD  21367  bl2in  24393  iihalf1  24939  iihalf2  24942  pcoass  25038  tcphcphlem1  25250  trirn  25415  minveclem2  25441  minveclem4  25447  ovolunlem1a  25512  vitalilem4  25627  mbfi1fseqlem5  25736  pilem2  26478  pilem3  26479  pipos  26484  sinhalfpilem  26487  sincosq1lem  26521  tangtx  26529  sinq12gt0  26531  sincos6thpi  26539  cosordlem  26553  tanord1  26560  efif1olem2  26566  efif1olem4  26568  cxpcn3lem  26771  ang180lem1  26833  ang180lem2  26834  atantan  26947  atanbndlem  26949  atans2  26955  leibpi  26966  log2tlbnd  26969  basellem1  27105  basellem2  27106  basellem3  27107  ppiltx  27201  ppiub  27229  chtublem  27236  chtub  27237  chpval2  27243  bcmono  27302  bpos1lem  27307  bposlem1  27309  bposlem2  27310  bposlem3  27311  bposlem4  27312  bposlem5  27313  bposlem6  27314  bposlem7  27315  gausslemma2dlem0c  27383  gausslemma2dlem1a  27390  gausslemma2dlem2  27392  gausslemma2dlem3  27393  lgseisenlem1  27400  lgseisenlem2  27401  lgseisenlem3  27402  lgsquadlem1  27405  lgsquadlem2  27406  2lgslem1a1  27414  2lgslem1a2  27415  2lgslem1c  27418  chebbnd1lem1  27494  chebbnd1lem2  27495  chebbnd1lem3  27496  chebbnd1  27497  chtppilimlem1  27498  chtppilimlem2  27499  chtppilim  27500  chebbnd2  27502  chto1lb  27503  chpchtlim  27504  chpo1ub  27505  dchrisum0fno1  27536  mulog2sumlem2  27560  selberglem2  27571  selberg2lem  27575  chpdifbndlem1  27578  logdivbnd  27581  pntrsumo1  27590  pntpbnd1a  27610  pntlemh  27624  pntlemr  27627  pntlemk  27631  pntlemo  27632  pnt2  27638  umgrislfupgrlem  29054  lfgrnloop  29057  lfuhgr1v0e  29186  wwlksnextwrd  29827  wwlksnextfun  29828  wwlksnextinj  29829  clwlkclwwlklem2a2  29922  konigsberg  30186  ex-fl  30376  minvecolem2  30804  minvecolem4  30809  bcsiALT  31108  opsqrlem6  32074  cdj3lem1  32363  wrdt2ind  32819  cyc2fv2  33003  rtelextdg2lem  33598  2sqr3minply  33619  sqsscirc1  33735  omssubadd  34146  signslema  34420  hgt750lem  34509  subfacval3  35029  nn0prpwlem  36046  knoppndvlem18  36244  knoppndvlem19  36245  knoppndvlem21  36247  cnndvlem1  36252  iccioo01  37046  sin2h  37323  cos2h  37324  tan2h  37325  itg2addnclem  37384  3lexlogpow5ineq2  41766  3lexlogpow5ineq4  41767  3lexlogpow5ineq3  41768  3lexlogpow2ineq1  41769  3lexlogpow2ineq2  41770  3lexlogpow5ineq5  41771  aks4d1lem1  41773  aks4d1p1p3  41780  aks4d1p1p2  41781  aks4d1p1p4  41782  aks4d1p1p6  41784  aks4d1p1p7  41785  aks4d1p1p5  41786  aks4d1p1  41787  aks4d1p2  41788  aks4d1p3  41789  aks4d1p5  41791  aks4d1p6  41792  aks4d1p7d1  41793  aks4d1p7  41794  aks4d1p8  41798  aks4d1p9  41799  posbezout  41811  aks6d1c3  41834  2ap1caineq  41856  aks6d1c6lem4  41884  aks6d1c7lem1  41891  aks6d1c7lem2  41892  oexpreposd  42047  pellfundex  42579  jm2.22  42689  jm2.23  42690  imo72b2lem0  43868  sumnnodd  45286  sinaover2ne0  45524  stoweidlem14  45670  stoweidlem49  45705  stoweidlem52  45708  wallispilem4  45724  wallispi2lem2  45728  stirlinglem6  45735  stirlinglem15  45744  stirlingr  45746  dirkerval2  45750  dirkertrigeqlem3  45756  dirkercncflem4  45762  fourierdlem24  45787  fourierdlem79  45841  fourierdlem103  45865  fourierdlem104  45866  fourierdlem112  45874  fourierswlem  45886  fouriersw  45887  lighneallem4a  47215  nnoALTV  47302  nn0oALTV  47303  nn0e  47304  nneven  47305  evengpoap3  47406  nn0eo  47951  flnn0div2ge  47956  fldivexpfllog2  47988  fllog2  47991  blennngt2o2  48015  dignn0flhalf  48041  sepfsepc  48296