MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2pos Structured version   Visualization version   GIF version

Theorem 2pos 12264
Description: The number 2 is positive. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
2pos 0 < 2

Proof of Theorem 2pos
StepHypRef Expression
1 1re 11163 . . 3 1 ∈ ℝ
2 0lt1 11685 . . 3 0 < 1
31, 1, 2, 2addgt0ii 11705 . 2 0 < (1 + 1)
4 df-2 12224 . 2 2 = (1 + 1)
53, 4breqtrri 5136 1 0 < 2
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 5109  (class class class)co 7361  0cc0 11059  1c1 11060   + caddc 11062   < clt 11197  2c2 12216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-po 5549  df-so 5550  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8654  df-en 8890  df-dom 8891  df-sdom 8892  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-2 12224
This theorem is referenced by:  2ne0  12265  3pos  12266  halfgt0  12377  halflt1  12379  halfpos2  12390  halfnneg2  12392  nominpos  12398  avglt1  12399  avglt2  12400  nn0n0n1ge2b  12489  3halfnz  12590  2rp  12928  hashgt23el  14333  s3fv0  14789  sqreulem  15253  cos2bnd  16078  sin02gt0  16082  sincos2sgn  16084  sin4lt0  16085  epos  16097  sqrt2re  16140  nnoddm1d2  16276  2mulprm  16577  prmgaplem7  16937  slotsdifdsndx  17283  odrngstr  17292  imasvalstr  17341  psgnunilem2  19285  cnfldstr  20821  cnfldfunALTOLD  20833  bl2in  23776  iihalf1  24317  iihalf2  24319  pcoass  24410  tcphcphlem1  24622  trirn  24787  minveclem2  24813  minveclem4  24819  ovolunlem1a  24883  vitalilem4  24998  mbfi1fseqlem5  25107  pilem2  25834  pilem3  25835  pipos  25840  sinhalfpilem  25843  sincosq1lem  25877  tangtx  25885  sinq12gt0  25887  sincos6thpi  25895  cosordlem  25909  tanord1  25916  efif1olem2  25922  efif1olem4  25924  cxpcn3lem  26123  ang180lem1  26182  ang180lem2  26183  atantan  26296  atanbndlem  26298  atans2  26304  leibpi  26315  log2tlbnd  26318  basellem1  26453  basellem2  26454  basellem3  26455  ppiltx  26549  ppiub  26575  chtublem  26582  chtub  26583  chpval2  26589  bcmono  26648  bpos1lem  26653  bposlem1  26655  bposlem2  26656  bposlem3  26657  bposlem4  26658  bposlem5  26659  bposlem6  26660  bposlem7  26661  gausslemma2dlem0c  26729  gausslemma2dlem1a  26736  gausslemma2dlem2  26738  gausslemma2dlem3  26739  lgseisenlem1  26746  lgseisenlem2  26747  lgseisenlem3  26748  lgsquadlem1  26751  lgsquadlem2  26752  2lgslem1a1  26760  2lgslem1a2  26761  2lgslem1c  26764  chebbnd1lem1  26840  chebbnd1lem2  26841  chebbnd1lem3  26842  chebbnd1  26843  chtppilimlem1  26844  chtppilimlem2  26845  chtppilim  26846  chebbnd2  26848  chto1lb  26849  chpchtlim  26850  chpo1ub  26851  dchrisum0fno1  26882  mulog2sumlem2  26906  selberglem2  26917  selberg2lem  26921  chpdifbndlem1  26924  logdivbnd  26927  pntrsumo1  26936  pntpbnd1a  26956  pntlemh  26970  pntlemr  26973  pntlemk  26977  pntlemo  26978  pnt2  26984  umgrislfupgrlem  28122  lfgrnloop  28125  lfuhgr1v0e  28251  wwlksnextwrd  28891  wwlksnextfun  28892  wwlksnextinj  28893  clwlkclwwlklem2a2  28986  konigsberg  29250  ex-fl  29440  minvecolem2  29866  minvecolem4  29871  bcsiALT  30170  opsqrlem6  31136  cdj3lem1  31425  wrdt2ind  31863  cyc2fv2  32027  sqsscirc1  32553  omssubadd  32964  signslema  33238  hgt750lem  33328  subfacval3  33847  nn0prpwlem  34847  knoppndvlem18  35045  knoppndvlem19  35046  knoppndvlem21  35048  cnndvlem1  35053  iccioo01  35848  sin2h  36118  cos2h  36119  tan2h  36120  itg2addnclem  36179  3lexlogpow5ineq2  40562  3lexlogpow5ineq4  40563  3lexlogpow5ineq3  40564  3lexlogpow2ineq1  40565  3lexlogpow2ineq2  40566  3lexlogpow5ineq5  40567  aks4d1lem1  40569  aks4d1p1p3  40576  aks4d1p1p2  40577  aks4d1p1p4  40578  aks4d1p1p6  40580  aks4d1p1p7  40581  aks4d1p1p5  40582  aks4d1p1  40583  aks4d1p2  40584  aks4d1p3  40585  aks4d1p5  40587  aks4d1p6  40588  aks4d1p7d1  40589  aks4d1p7  40590  aks4d1p8  40594  aks4d1p9  40595  2ap1caineq  40603  oexpreposd  40854  pellfundex  41256  jm2.22  41366  jm2.23  41367  imo72b2lem0  42530  sumnnodd  43961  sinaover2ne0  44199  stoweidlem14  44345  stoweidlem49  44380  stoweidlem52  44383  wallispilem4  44399  wallispi2lem2  44403  stirlinglem6  44410  stirlinglem15  44419  stirlingr  44421  dirkerval2  44425  dirkertrigeqlem3  44431  dirkercncflem4  44437  fourierdlem24  44462  fourierdlem79  44516  fourierdlem103  44540  fourierdlem104  44541  fourierdlem112  44549  fourierswlem  44561  fouriersw  44562  lighneallem4a  45890  nnoALTV  45977  nn0oALTV  45978  nn0e  45979  nneven  45980  evengpoap3  46081  nn0eo  46704  flnn0div2ge  46709  fldivexpfllog2  46741  fllog2  46744  blennngt2o2  46768  dignn0flhalf  46794  sepfsepc  47050
  Copyright terms: Public domain W3C validator