Theorem 2pos 12235

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 11119	. . 3 ⊢ 1 ∈ ℝ
2		0lt1 11646	. . 3 ⊢ 0 < 1
3	1, 1, 2, 2	addgt0ii 11666	. 2 ⊢ 0 < (1 + 1)
4		df-2 12195	. 2 ⊢ 2 = (1 + 1)
5	3, 4	breqtrri 5120	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5093  (class class class)co 7352  0cc0 11013  1c1 11014   + caddc 11016   < clt 11153  2c2 12187

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089  ax-pre-mulgt0 11090

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 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-sub 11353  df-neg 11354  df-2 12195

This theorem is referenced by:  3pos  12237  halfgt0  12343  halflt1  12345  halfpos2  12357  halfnneg2  12359  nominpos  12365  avglt1  12366  avglt2  12367  nn0n0n1ge2b  12457  3halfnz  12558  2rp  12897  hashgt23el  14333  s3fv0  14800  sqreulem  15269  cos2bnd  16099  sin02gt0  16103  sincos2sgn  16105  sin4lt0  16106  epos  16118  sqrt2re  16161  nnoddm1d2  16299  2mulprm  16606  prmgaplem7  16971  slotsdifdsndx  17300  odrngstr  17309  imasvalstr  17357  psgnunilem2  19409  cnfldstr  21295  cnfldstrOLD  21310  bl2in  24316  iihalf1  24853  iihalf2  24856  pcoass  24952  tcphcphlem1  25163  trirn  25328  minveclem2  25354  minveclem4  25360  ovolunlem1a  25425  vitalilem4  25540  mbfi1fseqlem5  25648  pilem2  26390  pilem3  26391  pipos  26396  sinhalfpilem  26400  sincosq1lem  26434  tangtx  26442  sinq12gt0  26444  tan4thpi  26451  sincos6thpi  26453  cosordlem  26467  tanord1  26474  efif1olem2  26480  efif1olem4  26482  cxpcn3lem  26685  ang180lem1  26747  ang180lem2  26748  atantan  26861  atanbndlem  26863  atans2  26869  leibpi  26880  log2tlbnd  26883  basellem1  27019  basellem2  27020  basellem3  27021  ppiltx  27115  ppiub  27143  chtublem  27150  chtub  27151  chpval2  27157  bcmono  27216  bpos1lem  27221  bposlem1  27223  bposlem2  27224  bposlem3  27225  bposlem4  27226  bposlem5  27227  bposlem6  27228  bposlem7  27229  gausslemma2dlem0c  27297  gausslemma2dlem1a  27304  gausslemma2dlem2  27306  gausslemma2dlem3  27307  lgseisenlem1  27314  lgseisenlem2  27315  lgseisenlem3  27316  lgsquadlem1  27319  lgsquadlem2  27320  2lgslem1a1  27328  2lgslem1a2  27329  2lgslem1c  27332  chebbnd1lem1  27408  chebbnd1lem2  27409  chebbnd1lem3  27410  chebbnd1  27411  chtppilimlem1  27412  chtppilimlem2  27413  chtppilim  27414  chebbnd2  27416  chto1lb  27417  chpchtlim  27418  chpo1ub  27419  dchrisum0fno1  27450  mulog2sumlem2  27474  selberglem2  27485  selberg2lem  27489  chpdifbndlem1  27492  logdivbnd  27495  pntrsumo1  27504  pntpbnd1a  27524  pntlemh  27538  pntlemr  27541  pntlemk  27545  pntlemo  27546  pnt2  27552  umgrislfupgrlem  29102  lfgrnloop  29105  lfuhgr1v0e  29234  wwlksnextwrd  29877  wwlksnextfun  29878  wwlksnextinj  29879  clwlkclwwlklem2a2  29975  konigsberg  30239  ex-fl  30429  minvecolem2  30857  minvecolem4  30862  bcsiALT  31161  opsqrlem6  32127  cdj3lem1  32416  wrdt2ind  32941  cyc2fv2  33098  rtelextdg2lem  33760  2sqr3minply  33814  sqsscirc1  33942  omssubadd  34334  signslema  34596  hgt750lem  34685  subfacval3  35254  nn0prpwlem  36387  knoppndvlem18  36594  knoppndvlem19  36595  knoppndvlem21  36597  cnndvlem1  36602  iccioo01  37392  sin2h  37670  cos2h  37671  tan2h  37672  itg2addnclem  37731  3lexlogpow5ineq2  42168  3lexlogpow5ineq4  42169  3lexlogpow5ineq3  42170  3lexlogpow2ineq1  42171  3lexlogpow2ineq2  42172  3lexlogpow5ineq5  42173  aks4d1lem1  42175  aks4d1p1p3  42182  aks4d1p1p2  42183  aks4d1p1p4  42184  aks4d1p1p6  42186  aks4d1p1p7  42187  aks4d1p1p5  42188  aks4d1p1  42189  aks4d1p2  42190  aks4d1p3  42191  aks4d1p5  42193  aks4d1p6  42194  aks4d1p7d1  42195  aks4d1p7  42196  aks4d1p8  42200  aks4d1p9  42201  posbezout  42213  aks6d1c3  42236  2ap1caineq  42258  aks6d1c6lem4  42286  aks6d1c7lem1  42293  aks6d1c7lem2  42294  oexpreposd  42440  asin1half  42475  pellfundex  43003  jm2.22  43112  jm2.23  43113  imo72b2lem0  44282  sumnnodd  45754  sinaover2ne0  45990  stoweidlem14  46136  stoweidlem49  46171  stoweidlem52  46174  wallispilem4  46190  wallispi2lem2  46194  stirlinglem6  46201  stirlinglem15  46210  stirlingr  46212  dirkerval2  46216  dirkertrigeqlem3  46222  dirkercncflem4  46228  fourierdlem24  46253  fourierdlem79  46307  fourierdlem103  46331  fourierdlem104  46332  fourierdlem112  46340  fourierswlem  46352  fouriersw  46353  nthrucw  47008  2ltceilhalf  47452  2tceilhalfelfzo1  47456  lighneallem4a  47732  nnoALTV  47819  nn0oALTV  47820  nn0e  47821  nneven  47822  evengpoap3  47923  gpg3kgrtriexlem1  48207  nn0eo  48653  flnn0div2ge  48658  fldivexpfllog2  48690  fllog2  48693  blennngt2o2  48717  dignn0flhalf  48743  sepfsepc  49052