Theorem 2pos 11112

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 10039	. . 3 |- 1 e. RR
2		0lt1 10550	. . 3 |- 0 < 1
3	1, 1, 2, 2	addgt0ii 10570	. 2 |- 0 < ( 1 + 1 )
4		df-2 11079	. 2 |- 2 = ( 1 + 1 )
5	3, 4	breqtrri 4680	1 |- 0 < 2

Syntax hints:   class class class wbr 4653  (class class class)co 6650   0cc0 9936   1c1 9937   + caddc 9939   < clt 10074   2c2 11070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-2 11079

This theorem is referenced by:  2ne0  11113  3pos  11114  halfgt0  11248  halflt1  11250  halfpos2  11261  halfnneg2  11263  nominpos  11269  avglt1  11270  avglt2  11271  nn0n0n1ge2b  11359  3halfnz  11456  2rp  11837  zgt1rpn0n1  11871  2tnp1ge0ge0  12630  fldiv4lem1div2uz2  12637  s3fv0  13636  2swrd2eqwrdeq  13696  sqrlem7  13989  sqreulem  14099  amgm2  14109  iseralt  14415  climcndslem2  14582  climcnds  14583  geoihalfsum  14614  efcllem  14808  cos2bnd  14918  sin02gt0  14922  sincos2sgn  14924  sin4lt0  14925  epos  14935  sqrt2re  14980  oexpneg  15069  oddge22np1  15073  evennn02n  15074  nn0ehalf  15095  nno  15098  nn0oddm1d2  15101  nnoddm1d2  15102  flodddiv4t2lthalf  15140  oddprm  15515  iserodd  15540  prmgaplem7  15761  odrngstr  16066  imasvalstr  16112  psgnunilem2  17915  cnfldstr  19748  cnfldfun  19758  bl2in  22205  iihalf1  22730  iihalf2  22732  pcoass  22824  tchcphlem1  23034  trirn  23183  minveclem2  23197  minveclem4  23203  ovolunlem1a  23264  vitalilem4  23380  mbfi1fseqlem5  23486  pilem2  24206  pilem3  24207  pipos  24212  sinhalfpilem  24215  sincosq1lem  24249  tangtx  24257  sinq12gt0  24259  sincos6thpi  24267  cosordlem  24277  tanord1  24283  efif1olem2  24289  efif1olem4  24291  cxpcn3lem  24488  ang180lem1  24539  ang180lem2  24540  atantan  24650  atanbndlem  24652  atans2  24658  leibpilem1  24667  leibpi  24669  log2tlbnd  24672  basellem1  24807  basellem2  24808  basellem3  24809  ppiltx  24903  ppiub  24929  chtublem  24936  chtub  24937  chpval2  24943  bcmono  25002  bpos1lem  25007  bposlem1  25009  bposlem2  25010  bposlem3  25011  bposlem4  25012  bposlem5  25013  bposlem6  25014  bposlem7  25015  gausslemma2dlem0c  25083  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  gausslemma2dlem3  25093  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgsquadlem1  25105  lgsquadlem2  25106  2lgslem1a1  25114  2lgslem1a2  25115  2lgslem1c  25118  chebbnd1lem1  25158  chebbnd1lem2  25159  chebbnd1lem3  25160  chebbnd1  25161  chtppilimlem1  25162  chtppilimlem2  25163  chtppilim  25164  chebbnd2  25166  chto1lb  25167  chpchtlim  25168  chpo1ub  25169  dchrisum0fno1  25200  mulog2sumlem2  25224  selberglem2  25235  selberg2lem  25239  chpdifbndlem1  25242  logdivbnd  25245  pntrsumo1  25254  pntpbnd1a  25274  pntlemh  25288  pntlemr  25291  pntlemk  25295  pntlemo  25296  pnt2  25302  umgrislfupgrlem  26017  lfgrnloop  26020  lfuhgr1v0e  26146  wwlksnextwrd  26792  wwlksnextfun  26793  wwlksnextinj  26794  clwlkclwwlklem2a2  26894  konigsberg  27119  ex-fl  27304  nvge0  27528  minvecolem2  27731  minvecolem4  27736  bcsiALT  28036  opsqrlem6  29004  cdj3lem1  29293  sqsscirc1  29954  omssubadd  30362  signslema  30639  hgt750lem  30729  subfacval3  31171  nn0prpwlem  32317  knoppndvlem18  32520  knoppndvlem19  32521  knoppndvlem21  32523  cnndvlem1  32528  sin2h  33399  cos2h  33400  tan2h  33401  itg2addnclem  33461  pellfundex  37450  rmspecsqrtnqOLD  37471  jm2.22  37562  jm2.23  37563  imo72b2lem0  38465  sumnnodd  39862  sinaover2ne0  40079  stoweidlem14  40231  stoweidlem49  40266  stoweidlem52  40269  wallispilem4  40285  wallispi2lem2  40289  stirlinglem6  40296  stirlinglem15  40305  stirlingr  40307  dirkerval2  40311  dirkertrigeqlem3  40317  dirkercncflem4  40323  fourierdlem24  40348  fourierdlem79  40402  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierswlem  40447  fouriersw  40448  lighneallem4a  41525  oexpnegALTV  41588  nnoALTV  41606  nn0oALTV  41607  nn0e  41608  evengpoap3  41687  nn0eo  42322  flnn0div2ge  42327  fldivexpfllog2  42359  fllog2  42362  blennngt2o2  42386  dignn0flhalf  42412