Theorem 2pos 12275

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 11135	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11663	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11683	. 2 ⊢ 0 < (1 + 1)
4		df-2 12235	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5113	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5086  (class class class)co 7360  0cc0 11029  1c1 11030   + caddc 11032   < clt 11170  2c2 12227

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 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

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 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-2 12235

This theorem is referenced by:  3pos  12277  halfgt0  12383  halflt1  12385  halfpos2  12397  halfnneg2  12399  nominpos  12405  avglt1  12406  avglt2  12407  nn0n0n1ge2b  12497  3halfnz  12599  2rp  12938  hashgt23el  14377  s3fv0  14844  sqreulem  15313  cos2bnd  16146  sin02gt0  16150  sincos2sgn  16152  sin4lt0  16153  epos  16165  sqrt2re  16208  nnoddm1d2  16346  2mulprm  16653  prmgaplem7  17019  slotsdifdsndx  17348  odrngstr  17357  imasvalstr  17405  psgnunilem2  19461  cnfldstr  21346  cnfldstrOLD  21361  bl2in  24375  iihalf1  24908  iihalf2  24910  pcoass  25001  tcphcphlem1  25212  trirn  25377  minveclem2  25403  minveclem4  25409  ovolunlem1a  25473  vitalilem4  25588  mbfi1fseqlem5  25696  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  26724  ang180lem1  26786  ang180lem2  26787  atantan  26900  atanbndlem  26902  atans2  26908  leibpi  26919  log2tlbnd  26922  basellem1  27058  basellem2  27059  basellem3  27060  ppiltx  27154  ppiub  27181  chtublem  27188  chtub  27189  chpval2  27195  bcmono  27254  bpos1lem  27259  bposlem1  27261  bposlem2  27262  bposlem3  27263  bposlem4  27264  bposlem5  27265  bposlem6  27266  bposlem7  27267  gausslemma2dlem0c  27335  gausslemma2dlem1a  27342  gausslemma2dlem2  27344  gausslemma2dlem3  27345  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgsquadlem1  27357  lgsquadlem2  27358  2lgslem1a1  27366  2lgslem1a2  27367  2lgslem1c  27370  chebbnd1lem1  27446  chebbnd1lem2  27447  chebbnd1lem3  27448  chebbnd1  27449  chtppilimlem1  27450  chtppilimlem2  27451  chtppilim  27452  chebbnd2  27454  chto1lb  27455  chpchtlim  27456  chpo1ub  27457  dchrisum0fno1  27488  mulog2sumlem2  27512  selberglem2  27523  selberg2lem  27527  chpdifbndlem1  27530  logdivbnd  27533  pntrsumo1  27542  pntpbnd1a  27562  pntlemh  27576  pntlemr  27579  pntlemk  27583  pntlemo  27584  pnt2  27590  umgrislfupgrlem  29205  lfgrnloop  29208  lfuhgr1v0e  29337  wwlksnextwrd  29980  wwlksnextfun  29981  wwlksnextinj  29982  clwlkclwwlklem2a2  30078  konigsberg  30342  ex-fl  30532  minvecolem2  30961  minvecolem4  30966  bcsiALT  31265  opsqrlem6  32231  cdj3lem1  32520  wrdt2ind  33028  cyc2fv2  33198  rtelextdg2lem  33886  2sqr3minply  33940  sqsscirc1  34068  omssubadd  34460  signslema  34722  hgt750lem  34811  subfacval3  35387  nn0prpwlem  36520  knoppndvlem18  36805  knoppndvlem19  36806  knoppndvlem21  36808  cnndvlem1  36813  iccioo01  37657  sin2h  37945  cos2h  37946  tan2h  37947  itg2addnclem  38006  3lexlogpow5ineq2  42508  3lexlogpow5ineq4  42509  3lexlogpow5ineq3  42510  3lexlogpow2ineq1  42511  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1lem1  42515  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p2  42530  aks4d1p3  42531  aks4d1p5  42533  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8  42540  aks4d1p9  42541  posbezout  42553  aks6d1c3  42576  2ap1caineq  42598  aks6d1c6lem4  42626  aks6d1c7lem1  42633  aks6d1c7lem2  42634  oexpreposd  42768  asin1half  42803  pellfundex  43332  jm2.22  43441  jm2.23  43442  imo72b2lem0  44610  sumnnodd  46078  sinaover2ne0  46314  stoweidlem14  46460  stoweidlem49  46495  stoweidlem52  46498  wallispilem4  46514  wallispi2lem2  46518  stirlinglem6  46525  stirlinglem15  46534  stirlingr  46536  dirkerval2  46540  dirkertrigeqlem3  46546  dirkercncflem4  46552  fourierdlem24  46577  fourierdlem79  46631  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  fourierswlem  46676  fouriersw  46677  nthrucw  47332  goldrapos  47345  2ltceilhalf  47792  2tceilhalfelfzo1  47796  lighneallem4a  48083  nprmdvdsfacm1lem4  48098  nnoALTV  48183  nn0oALTV  48184  nn0e  48185  nneven  48186  evengpoap3  48287  gpg3kgrtriexlem1  48571  nn0eo  49016  flnn0div2ge  49021  fldivexpfllog2  49053  fllog2  49056  blennngt2o2  49080  dignn0flhalf  49106  sepfsepc  49415