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  34722  signslema  34981  hgt750lem  35070  subfacval3  35702  nn0prpwlem  36874  knoppndvlem18  37159  knoppndvlem19  37160  knoppndvlem21  37162  cnndvlem1  37167  iccioo01  38014  sin2h  38302  cos2h  38303  tan2h  38304  itg2addnclem  38363  3lexlogpow5ineq2  42863  3lexlogpow5ineq4  42864  3lexlogpow5ineq3  42865  3lexlogpow2ineq1  42866  3lexlogpow2ineq2  42867  3lexlogpow5ineq5  42868  aks4d1lem1  42870  aks4d1p1p3  42877  aks4d1p1p2  42878  aks4d1p1p4  42879  aks4d1p1p6  42881  aks4d1p1p7  42882  aks4d1p1p5  42883  aks4d1p1  42884  aks4d1p2  42885  aks4d1p3  42886  aks4d1p5  42888  aks4d1p6  42889  aks4d1p7d1  42890  aks4d1p7  42891  aks4d1p8  42895  aks4d1p9  42896  posbezout  42908  aks6d1c3  42931  2ap1caineq  42953  aks6d1c6lem4  42981  aks6d1c7lem1  42988  aks6d1c7lem2  42989  oexpreposd  43124  asin1half  43159  pellfundex  43654  jm2.22  43763  jm2.23  43764  imo72b2lem0  44932  sumnnodd  46387  sinaover2ne0  46623  stoweidlem14  46769  stoweidlem49  46804  stoweidlem52  46807  wallispilem4  46823  wallispi2lem2  46827  stirlinglem6  46834  stirlinglem15  46843  stirlingr  46845  dirkerval2  46849  dirkertrigeqlem3  46855  dirkercncflem4  46861  fourierdlem24  46886  fourierdlem79  46940  fourierdlem103  46964  fourierdlem104  46965  fourierdlem112  46973  fourierswlem  46985  fouriersw  46986  goldrapos  47661  2ltceilhalf  48110  2tceilhalfelfzo1  48114  lighneallem4a  48401  nprmdvdsfacm1lem4  48416  nnoALTV  48501  nn0oALTV  48502  nn0e  48503  nneven  48504  evengpoap3  48605  gpg3kgrtriexlem1  48889  nn0eo  49349  flnn0div2ge  49354  fldivexpfllog2  49386  fllog2  49389  blennngt2o2  49413  dignn0flhalf  49439  sepfsepc  49747