Theorem 2pos 12363

Description: The number 2 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
2pos	⊢ 0 < 2

Proof of Theorem 2pos

Step	Hyp	Ref	Expression
1		2nn 12332	. 2 ⊢ 2 ∈ ℕ
2	1	nngt0i 12293	1 ⊢ 0 < 2

This proof depends on syntax axioms:   class class class wbr 5114  0cc0 11118   < clt 11261  2c2 12313

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-nn 12252  df-2 12321

This theorem is used by:  halfgt0  12477  halflt1  12479  halfpos2  12491  halfnneg2  12493  nominpos  12499  avglt1  12500  avglt2  12501  nn0n0n1ge2b  12591  3halfnz  12693  2rp  13039  hashgt23el  14481  s3fv0  14954  sqreulem  15437  cos2bnd  16269  sin02gt0  16273  sincos2sgn  16275  sin4lt0  16276  epos  16288  sqrt2re  16331  nnoddm1d2  16469  2mulprm  16776  prmgaplem7  17142  slotsdifdsndx  17472  odrngstr  17481  imasvalstr  17529  psgnunilem2  19596  cnfldstr  21561  bl2in  24594  iihalf1  25127  iihalf2  25129  pcoass  25220  tcphcphlem1  25431  trirn  25596  minveclem2  25622  minveclem4  25628  ovolunlem1a  25692  vitalilem4  25807  mbfi1fseqlem5  25915  pilem2  26652  pilem3  26653  pipos  26660  sinhalfpilem  26665  sincosq1lem  26699  tangtx  26707  sinq12gt0  26709  tan4thpi  26716  sincos6thpi  26718  cosordlem  26732  tanord1  26739  efif1olem2  26745  efif1olem4  26747  cxpcn3lem  26949  ang180lem1  27011  ang180lem2  27012  atantan  27125  atanbndlem  27127  atans2  27133  leibpi  27144  log2tlbnd  27147  basellem1  27282  basellem2  27283  basellem3  27284  ppiltx  27378  ppiub  27405  chtublem  27412  chtub  27413  chpval2  27419  bcmono  27478  bpos1lem  27483  bposlem1  27485  bposlem2  27486  bposlem3  27487  bposlem4  27488  bposlem5  27489  bposlem6  27490  bposlem7  27491  gausslemma2dlem0c  27559  gausslemma2dlem1a  27566  gausslemma2dlem2  27568  gausslemma2dlem3  27569  lgseisenlem1  27576  lgseisenlem2  27577  lgseisenlem3  27578  lgsquadlem1  27581  lgsquadlem2  27582  2lgslem1a1  27590  2lgslem1a2  27591  2lgslem1c  27594  chebbnd1lem1  27670  chebbnd1lem2  27671  chebbnd1lem3  27672  chebbnd1  27673  chtppilimlem1  27674  chtppilimlem2  27675  chtppilim  27676  chebbnd2  27678  chto1lb  27679  chpchtlim  27680  chpo1ub  27681  dchrisum0fno1  27712  mulog2sumlem2  27736  selberglem2  27747  selberg2lem  27751  chpdifbndlem1  27754  logdivbnd  27757  pntrsumo1  27766  pntpbnd1a  27786  pntlemh  27800  pntlemr  27803  pntlemk  27807  pntlemo  27808  pnt2  27814  umgrislfupgrlem  29509  lfgrnloop  29512  lfuhgr1v0e  29641  wwlksnextwrd  30283  wwlksnextfun  30284  wwlksnextinj  30285  clwlkclwwlklem2a2  30381  konigsberg  30645  ex-fl  30835  minvecolem2  31264  minvecolem4  31269  bcsiALT  31568  opsqrlem6  32534  cdj3lem1  32823  wrdt2ind  33306  cyc2fv2  33473  rtelextdg2lem  34147  2sqr3minply  34201  sqsscirc1  34329  omssubadd  34721  signslema  34980  hgt750lem  35069  subfacval3  35701  nn0prpwlem  36873  knoppndvlem18  37158  knoppndvlem19  37159  knoppndvlem21  37161  cnndvlem1  37166  iccioo01  38013  sin2h  38301  cos2h  38302  tan2h  38303  itg2addnclem  38362  3lexlogpow5ineq2  42862  3lexlogpow5ineq4  42863  3lexlogpow5ineq3  42864  3lexlogpow2ineq1  42865  3lexlogpow2ineq2  42866  3lexlogpow5ineq5  42867  aks4d1lem1  42869  aks4d1p1p3  42876  aks4d1p1p2  42877  aks4d1p1p4  42878  aks4d1p1p6  42880  aks4d1p1p7  42881  aks4d1p1p5  42882  aks4d1p1  42883  aks4d1p2  42884  aks4d1p3  42885  aks4d1p5  42887  aks4d1p6  42888  aks4d1p7d1  42889  aks4d1p7  42890  aks4d1p8  42894  aks4d1p9  42895  posbezout  42907  aks6d1c3  42930  2ap1caineq  42952  aks6d1c6lem4  42980  aks6d1c7lem1  42987  aks6d1c7lem2  42988  oexpreposd  43123  asin1half  43158  pellfundex  43653  jm2.22  43762  jm2.23  43763  imo72b2lem0  44931  sumnnodd  46386  sinaover2ne0  46622  stoweidlem14  46768  stoweidlem49  46803  stoweidlem52  46806  wallispilem4  46822  wallispi2lem2  46826  stirlinglem6  46833  stirlinglem15  46842  stirlingr  46844  dirkerval2  46848  dirkertrigeqlem3  46854  dirkercncflem4  46860  fourierdlem24  46885  fourierdlem79  46939  fourierdlem103  46963  fourierdlem104  46964  fourierdlem112  46972  fourierswlem  46984  fouriersw  46985  goldrapos  47660  2ltceilhalf  48109  2tceilhalfelfzo1  48113  lighneallem4a  48400  nprmdvdsfacm1lem4  48415  nnoALTV  48500  nn0oALTV  48501  nn0e  48502  nneven  48503  evengpoap3  48604  gpg3kgrtriexlem1  48888  nn0eo  49348  flnn0div2ge  49353  fldivexpfllog2  49385  fllog2  49388  blennngt2o2  49412  dignn0flhalf  49438  sepfsepc  49746