Theorem 2pos 12260

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 11144	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11671	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11691	. 2 ⊢ 0 < (1 + 1)
4		df-2 12220	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5127	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5100  (class class class)co 7368  0cc0 11038  1c1 11039   + caddc 11041   < clt 11178  2c2 12212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-2 12220

This theorem is referenced by:  3pos  12262  halfgt0  12368  halflt1  12370  halfpos2  12382  halfnneg2  12384  nominpos  12390  avglt1  12391  avglt2  12392  nn0n0n1ge2b  12482  3halfnz  12583  2rp  12922  hashgt23el  14359  s3fv0  14826  sqreulem  15295  cos2bnd  16125  sin02gt0  16129  sincos2sgn  16131  sin4lt0  16132  epos  16144  sqrt2re  16187  nnoddm1d2  16325  2mulprm  16632  prmgaplem7  16997  slotsdifdsndx  17326  odrngstr  17335  imasvalstr  17383  psgnunilem2  19436  cnfldstr  21323  cnfldstrOLD  21338  bl2in  24356  iihalf1  24893  iihalf2  24896  pcoass  24992  tcphcphlem1  25203  trirn  25368  minveclem2  25394  minveclem4  25400  ovolunlem1a  25465  vitalilem4  25580  mbfi1fseqlem5  25688  pilem2  26430  pilem3  26431  pipos  26436  sinhalfpilem  26440  sincosq1lem  26474  tangtx  26482  sinq12gt0  26484  tan4thpi  26491  sincos6thpi  26493  cosordlem  26507  tanord1  26514  efif1olem2  26520  efif1olem4  26522  cxpcn3lem  26725  ang180lem1  26787  ang180lem2  26788  atantan  26901  atanbndlem  26903  atans2  26909  leibpi  26920  log2tlbnd  26923  basellem1  27059  basellem2  27060  basellem3  27061  ppiltx  27155  ppiub  27183  chtublem  27190  chtub  27191  chpval2  27197  bcmono  27256  bpos1lem  27261  bposlem1  27263  bposlem2  27264  bposlem3  27265  bposlem4  27266  bposlem5  27267  bposlem6  27268  bposlem7  27269  gausslemma2dlem0c  27337  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  gausslemma2dlem3  27347  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgsquadlem1  27359  lgsquadlem2  27360  2lgslem1a1  27368  2lgslem1a2  27369  2lgslem1c  27372  chebbnd1lem1  27448  chebbnd1lem2  27449  chebbnd1lem3  27450  chebbnd1  27451  chtppilimlem1  27452  chtppilimlem2  27453  chtppilim  27454  chebbnd2  27456  chto1lb  27457  chpchtlim  27458  chpo1ub  27459  dchrisum0fno1  27490  mulog2sumlem2  27514  selberglem2  27525  selberg2lem  27529  chpdifbndlem1  27532  logdivbnd  27535  pntrsumo1  27544  pntpbnd1a  27564  pntlemh  27578  pntlemr  27581  pntlemk  27585  pntlemo  27586  pnt2  27592  umgrislfupgrlem  29207  lfgrnloop  29210  lfuhgr1v0e  29339  wwlksnextwrd  29982  wwlksnextfun  29983  wwlksnextinj  29984  clwlkclwwlklem2a2  30080  konigsberg  30344  ex-fl  30534  minvecolem2  30962  minvecolem4  30967  bcsiALT  31266  opsqrlem6  32232  cdj3lem1  32521  wrdt2ind  33045  cyc2fv2  33215  rtelextdg2lem  33903  2sqr3minply  33957  sqsscirc1  34085  omssubadd  34477  signslema  34739  hgt750lem  34828  subfacval3  35402  nn0prpwlem  36535  knoppndvlem18  36748  knoppndvlem19  36749  knoppndvlem21  36751  cnndvlem1  36756  iccioo01  37576  sin2h  37855  cos2h  37856  tan2h  37857  itg2addnclem  37916  3lexlogpow5ineq2  42419  3lexlogpow5ineq4  42420  3lexlogpow5ineq3  42421  3lexlogpow2ineq1  42422  3lexlogpow2ineq2  42423  3lexlogpow5ineq5  42424  aks4d1lem1  42426  aks4d1p1p3  42433  aks4d1p1p2  42434  aks4d1p1p4  42435  aks4d1p1p6  42437  aks4d1p1p7  42438  aks4d1p1p5  42439  aks4d1p1  42440  aks4d1p2  42441  aks4d1p3  42442  aks4d1p5  42444  aks4d1p6  42445  aks4d1p7d1  42446  aks4d1p7  42447  aks4d1p8  42451  aks4d1p9  42452  posbezout  42464  aks6d1c3  42487  2ap1caineq  42509  aks6d1c6lem4  42537  aks6d1c7lem1  42544  aks6d1c7lem2  42545  oexpreposd  42686  asin1half  42721  pellfundex  43237  jm2.22  43346  jm2.23  43347  imo72b2lem0  44515  sumnnodd  45984  sinaover2ne0  46220  stoweidlem14  46366  stoweidlem49  46401  stoweidlem52  46404  wallispilem4  46420  wallispi2lem2  46424  stirlinglem6  46431  stirlinglem15  46440  stirlingr  46442  dirkerval2  46446  dirkertrigeqlem3  46452  dirkercncflem4  46458  fourierdlem24  46483  fourierdlem79  46537  fourierdlem103  46561  fourierdlem104  46562  fourierdlem112  46570  fourierswlem  46582  fouriersw  46583  nthrucw  47238  2ltceilhalf  47682  2tceilhalfelfzo1  47686  lighneallem4a  47962  nnoALTV  48049  nn0oALTV  48050  nn0e  48051  nneven  48052  evengpoap3  48153  gpg3kgrtriexlem1  48437  nn0eo  48882  flnn0div2ge  48887  fldivexpfllog2  48919  fllog2  48922  blennngt2o2  48946  dignn0flhalf  48972  sepfsepc  49281