Theorem 2pos 12314

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 11213	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11735	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11755	. 2 ⊢ 0 < (1 + 1)
4		df-2 12274	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5175	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5148  (class class class)co 7408  0cc0 11109  1c1 11110   + caddc 11112   < clt 11247  2c2 12266

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-2 12274

This theorem is referenced by:  2ne0  12315  3pos  12316  halfgt0  12427  halflt1  12429  halfpos2  12440  halfnneg2  12442  nominpos  12448  avglt1  12449  avglt2  12450  nn0n0n1ge2b  12539  3halfnz  12640  2rp  12978  hashgt23el  14383  s3fv0  14841  sqreulem  15305  cos2bnd  16130  sin02gt0  16134  sincos2sgn  16136  sin4lt0  16137  epos  16149  sqrt2re  16192  nnoddm1d2  16328  2mulprm  16629  prmgaplem7  16989  slotsdifdsndx  17338  odrngstr  17347  imasvalstr  17396  psgnunilem2  19362  cnfldstr  20945  cnfldfunALTOLD  20957  bl2in  23905  iihalf1  24446  iihalf2  24448  pcoass  24539  tcphcphlem1  24751  trirn  24916  minveclem2  24942  minveclem4  24948  ovolunlem1a  25012  vitalilem4  25127  mbfi1fseqlem5  25236  pilem2  25963  pilem3  25964  pipos  25969  sinhalfpilem  25972  sincosq1lem  26006  tangtx  26014  sinq12gt0  26016  sincos6thpi  26024  cosordlem  26038  tanord1  26045  efif1olem2  26051  efif1olem4  26053  cxpcn3lem  26252  ang180lem1  26311  ang180lem2  26312  atantan  26425  atanbndlem  26427  atans2  26433  leibpi  26444  log2tlbnd  26447  basellem1  26582  basellem2  26583  basellem3  26584  ppiltx  26678  ppiub  26704  chtublem  26711  chtub  26712  chpval2  26718  bcmono  26777  bpos1lem  26782  bposlem1  26784  bposlem2  26785  bposlem3  26786  bposlem4  26787  bposlem5  26788  bposlem6  26789  bposlem7  26790  gausslemma2dlem0c  26858  gausslemma2dlem1a  26865  gausslemma2dlem2  26867  gausslemma2dlem3  26868  lgseisenlem1  26875  lgseisenlem2  26876  lgseisenlem3  26877  lgsquadlem1  26880  lgsquadlem2  26881  2lgslem1a1  26889  2lgslem1a2  26890  2lgslem1c  26893  chebbnd1lem1  26969  chebbnd1lem2  26970  chebbnd1lem3  26971  chebbnd1  26972  chtppilimlem1  26973  chtppilimlem2  26974  chtppilim  26975  chebbnd2  26977  chto1lb  26978  chpchtlim  26979  chpo1ub  26980  dchrisum0fno1  27011  mulog2sumlem2  27035  selberglem2  27046  selberg2lem  27050  chpdifbndlem1  27053  logdivbnd  27056  pntrsumo1  27065  pntpbnd1a  27085  pntlemh  27099  pntlemr  27102  pntlemk  27106  pntlemo  27107  pnt2  27113  umgrislfupgrlem  28379  lfgrnloop  28382  lfuhgr1v0e  28508  wwlksnextwrd  29148  wwlksnextfun  29149  wwlksnextinj  29150  clwlkclwwlklem2a2  29243  konigsberg  29507  ex-fl  29697  minvecolem2  30123  minvecolem4  30128  bcsiALT  30427  opsqrlem6  31393  cdj3lem1  31682  wrdt2ind  32112  cyc2fv2  32276  sqsscirc1  32883  omssubadd  33294  signslema  33568  hgt750lem  33658  subfacval3  34175  nn0prpwlem  35202  knoppndvlem18  35400  knoppndvlem19  35401  knoppndvlem21  35403  cnndvlem1  35408  iccioo01  36203  sin2h  36473  cos2h  36474  tan2h  36475  itg2addnclem  36534  3lexlogpow5ineq2  40915  3lexlogpow5ineq4  40916  3lexlogpow5ineq3  40917  3lexlogpow2ineq1  40918  3lexlogpow2ineq2  40919  3lexlogpow5ineq5  40920  aks4d1lem1  40922  aks4d1p1p3  40929  aks4d1p1p2  40930  aks4d1p1p4  40931  aks4d1p1p6  40933  aks4d1p1p7  40934  aks4d1p1p5  40935  aks4d1p1  40936  aks4d1p2  40937  aks4d1p3  40938  aks4d1p5  40940  aks4d1p6  40941  aks4d1p7d1  40942  aks4d1p7  40943  aks4d1p8  40947  aks4d1p9  40948  2ap1caineq  40956  oexpreposd  41212  pellfundex  41614  jm2.22  41724  jm2.23  41725  imo72b2lem0  42907  sumnnodd  44336  sinaover2ne0  44574  stoweidlem14  44720  stoweidlem49  44755  stoweidlem52  44758  wallispilem4  44774  wallispi2lem2  44778  stirlinglem6  44785  stirlinglem15  44794  stirlingr  44796  dirkerval2  44800  dirkertrigeqlem3  44806  dirkercncflem4  44812  fourierdlem24  44837  fourierdlem79  44891  fourierdlem103  44915  fourierdlem104  44916  fourierdlem112  44924  fourierswlem  44936  fouriersw  44937  lighneallem4a  46266  nnoALTV  46353  nn0oALTV  46354  nn0e  46355  nneven  46356  evengpoap3  46457  nn0eo  47204  flnn0div2ge  47209  fldivexpfllog2  47241  fllog2  47244  blennngt2o2  47268  dignn0flhalf  47294  sepfsepc  47550