Theorem 2pos 12220

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 11104	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11631	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11651	. 2 ⊢ 0 < (1 + 1)
4		df-2 12180	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5116	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5089  (class class class)co 7341  0cc0 10998  1c1 10999   + caddc 11001   < clt 11138  2c2 12172

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 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-resscn 11055  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-mulcom 11062  ax-addass 11063  ax-mulass 11064  ax-distr 11065  ax-i2m1 11066  ax-1ne0 11067  ax-1rid 11068  ax-rnegex 11069  ax-rrecex 11070  ax-cnre 11071  ax-pre-lttri 11072  ax-pre-lttrn 11073  ax-pre-ltadd 11074  ax-pre-mulgt0 11075

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 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11140  df-mnf 11141  df-xr 11142  df-ltxr 11143  df-le 11144  df-sub 11338  df-neg 11339  df-2 12180

This theorem is referenced by:  3pos  12222  halfgt0  12328  halflt1  12330  halfpos2  12342  halfnneg2  12344  nominpos  12350  avglt1  12351  avglt2  12352  nn0n0n1ge2b  12442  3halfnz  12544  2rp  12887  hashgt23el  14323  s3fv0  14790  sqreulem  15259  cos2bnd  16089  sin02gt0  16093  sincos2sgn  16095  sin4lt0  16096  epos  16108  sqrt2re  16151  nnoddm1d2  16289  2mulprm  16596  prmgaplem7  16961  slotsdifdsndx  17290  odrngstr  17299  imasvalstr  17347  psgnunilem2  19400  cnfldstr  21286  cnfldstrOLD  21301  bl2in  24308  iihalf1  24845  iihalf2  24848  pcoass  24944  tcphcphlem1  25155  trirn  25320  minveclem2  25346  minveclem4  25352  ovolunlem1a  25417  vitalilem4  25532  mbfi1fseqlem5  25640  pilem2  26382  pilem3  26383  pipos  26388  sinhalfpilem  26392  sincosq1lem  26426  tangtx  26434  sinq12gt0  26436  tan4thpi  26443  sincos6thpi  26445  cosordlem  26459  tanord1  26466  efif1olem2  26472  efif1olem4  26474  cxpcn3lem  26677  ang180lem1  26739  ang180lem2  26740  atantan  26853  atanbndlem  26855  atans2  26861  leibpi  26872  log2tlbnd  26875  basellem1  27011  basellem2  27012  basellem3  27013  ppiltx  27107  ppiub  27135  chtublem  27142  chtub  27143  chpval2  27149  bcmono  27208  bpos1lem  27213  bposlem1  27215  bposlem2  27216  bposlem3  27217  bposlem4  27218  bposlem5  27219  bposlem6  27220  bposlem7  27221  gausslemma2dlem0c  27289  gausslemma2dlem1a  27296  gausslemma2dlem2  27298  gausslemma2dlem3  27299  lgseisenlem1  27306  lgseisenlem2  27307  lgseisenlem3  27308  lgsquadlem1  27311  lgsquadlem2  27312  2lgslem1a1  27320  2lgslem1a2  27321  2lgslem1c  27324  chebbnd1lem1  27400  chebbnd1lem2  27401  chebbnd1lem3  27402  chebbnd1  27403  chtppilimlem1  27404  chtppilimlem2  27405  chtppilim  27406  chebbnd2  27408  chto1lb  27409  chpchtlim  27410  chpo1ub  27411  dchrisum0fno1  27442  mulog2sumlem2  27466  selberglem2  27477  selberg2lem  27481  chpdifbndlem1  27484  logdivbnd  27487  pntrsumo1  27496  pntpbnd1a  27516  pntlemh  27530  pntlemr  27533  pntlemk  27537  pntlemo  27538  pnt2  27544  umgrislfupgrlem  29093  lfgrnloop  29096  lfuhgr1v0e  29225  wwlksnextwrd  29868  wwlksnextfun  29869  wwlksnextinj  29870  clwlkclwwlklem2a2  29963  konigsberg  30227  ex-fl  30417  minvecolem2  30845  minvecolem4  30850  bcsiALT  31149  opsqrlem6  32115  cdj3lem1  32404  wrdt2ind  32924  cyc2fv2  33081  rtelextdg2lem  33729  2sqr3minply  33783  sqsscirc1  33911  omssubadd  34303  signslema  34565  hgt750lem  34654  subfacval3  35201  nn0prpwlem  36335  knoppndvlem18  36542  knoppndvlem19  36543  knoppndvlem21  36545  cnndvlem1  36550  iccioo01  37340  sin2h  37629  cos2h  37630  tan2h  37631  itg2addnclem  37690  3lexlogpow5ineq2  42067  3lexlogpow5ineq4  42068  3lexlogpow5ineq3  42069  3lexlogpow2ineq1  42070  3lexlogpow2ineq2  42071  3lexlogpow5ineq5  42072  aks4d1lem1  42074  aks4d1p1p3  42081  aks4d1p1p2  42082  aks4d1p1p4  42083  aks4d1p1p6  42085  aks4d1p1p7  42086  aks4d1p1p5  42087  aks4d1p1  42088  aks4d1p2  42089  aks4d1p3  42090  aks4d1p5  42092  aks4d1p6  42093  aks4d1p7d1  42094  aks4d1p7  42095  aks4d1p8  42099  aks4d1p9  42100  posbezout  42112  aks6d1c3  42135  2ap1caineq  42157  aks6d1c6lem4  42185  aks6d1c7lem1  42192  aks6d1c7lem2  42193  oexpreposd  42334  asin1half  42369  pellfundex  42898  jm2.22  43007  jm2.23  43008  imo72b2lem0  44177  sumnnodd  45649  sinaover2ne0  45885  stoweidlem14  46031  stoweidlem49  46066  stoweidlem52  46069  wallispilem4  46085  wallispi2lem2  46089  stirlinglem6  46096  stirlinglem15  46105  stirlingr  46107  dirkerval2  46111  dirkertrigeqlem3  46117  dirkercncflem4  46123  fourierdlem24  46148  fourierdlem79  46202  fourierdlem103  46226  fourierdlem104  46227  fourierdlem112  46235  fourierswlem  46247  fouriersw  46248  2ltceilhalf  47338  2tceilhalfelfzo1  47342  lighneallem4a  47618  nnoALTV  47705  nn0oALTV  47706  nn0e  47707  nneven  47708  evengpoap3  47809  gpg3kgrtriexlem1  48093  nn0eo  48539  flnn0div2ge  48544  fldivexpfllog2  48576  fllog2  48579  blennngt2o2  48603  dignn0flhalf  48629  sepfsepc  48938