Theorem 2pos 12346

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 12315	. 2 ⊢ 2 ∈ ℕ
2	1	nngt0i 12276	1 ⊢ 0 < 2

Syntax hints:   class class class wbr 5110  0cc0 11101   < clt 11244  2c2 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-nn 12235  df-2 12304

This theorem is referenced by:  halfgt0  12460  halflt1  12462  halfpos2  12474  halfnneg2  12476  nominpos  12482  avglt1  12483  avglt2  12484  nn0n0n1ge2b  12574  3halfnz  12676  2rp  13022  hashgt23el  14463  s3fv0  14930  sqreulem  15413  cos2bnd  16245  sin02gt0  16249  sincos2sgn  16251  sin4lt0  16252  epos  16264  sqrt2re  16307  nnoddm1d2  16445  2mulprm  16752  prmgaplem7  17118  slotsdifdsndx  17448  odrngstr  17457  imasvalstr  17505  psgnunilem2  19566  cnfldstr  21505  bl2in  24538  iihalf1  25071  iihalf2  25073  pcoass  25164  tcphcphlem1  25375  trirn  25540  minveclem2  25566  minveclem4  25572  ovolunlem1a  25636  vitalilem4  25751  mbfi1fseqlem5  25859  pilem2  26593  pilem3  26594  pipos  26601  sinhalfpilem  26606  sincosq1lem  26640  tangtx  26648  sinq12gt0  26650  tan4thpi  26657  sincos6thpi  26659  cosordlem  26673  tanord1  26680  efif1olem2  26686  efif1olem4  26688  cxpcn3lem  26890  ang180lem1  26952  ang180lem2  26953  atantan  27066  atanbndlem  27068  atans2  27074  leibpi  27085  log2tlbnd  27088  basellem1  27223  basellem2  27224  basellem3  27225  ppiltx  27319  ppiub  27346  chtublem  27353  chtub  27354  chpval2  27360  bcmono  27419  bpos1lem  27424  bposlem1  27426  bposlem2  27427  bposlem3  27428  bposlem4  27429  bposlem5  27430  bposlem6  27431  bposlem7  27432  gausslemma2dlem0c  27500  gausslemma2dlem1a  27507  gausslemma2dlem2  27509  gausslemma2dlem3  27510  lgseisenlem1  27517  lgseisenlem2  27518  lgseisenlem3  27519  lgsquadlem1  27522  lgsquadlem2  27523  2lgslem1a1  27531  2lgslem1a2  27532  2lgslem1c  27535  chebbnd1lem1  27611  chebbnd1lem2  27612  chebbnd1lem3  27613  chebbnd1  27614  chtppilimlem1  27615  chtppilimlem2  27616  chtppilim  27617  chebbnd2  27619  chto1lb  27620  chpchtlim  27621  chpo1ub  27622  dchrisum0fno1  27653  mulog2sumlem2  27677  selberglem2  27688  selberg2lem  27692  chpdifbndlem1  27695  logdivbnd  27698  pntrsumo1  27707  pntpbnd1a  27727  pntlemh  27741  pntlemr  27744  pntlemk  27748  pntlemo  27749  pnt2  27755  umgrislfupgrlem  29450  lfgrnloop  29453  lfuhgr1v0e  29582  wwlksnextwrd  30224  wwlksnextfun  30225  wwlksnextinj  30226  clwlkclwwlklem2a2  30322  konigsberg  30586  ex-fl  30776  minvecolem2  31205  minvecolem4  31210  bcsiALT  31509  opsqrlem6  32475  cdj3lem1  32764  wrdt2ind  33251  cyc2fv2  33420  rtelextdg2lem  34094  2sqr3minply  34148  sqsscirc1  34276  omssubadd  34668  signslema  34927  hgt750lem  35016  subfacval3  35659  nn0prpwlem  36811  knoppndvlem18  37096  knoppndvlem19  37097  knoppndvlem21  37099  cnndvlem1  37104  iccioo01  37951  sin2h  38239  cos2h  38240  tan2h  38241  itg2addnclem  38300  3lexlogpow5ineq2  42800  3lexlogpow5ineq4  42801  3lexlogpow5ineq3  42802  3lexlogpow2ineq1  42803  3lexlogpow2ineq2  42804  3lexlogpow5ineq5  42805  aks4d1lem1  42807  aks4d1p1p3  42814  aks4d1p1p2  42815  aks4d1p1p4  42816  aks4d1p1p6  42818  aks4d1p1p7  42819  aks4d1p1p5  42820  aks4d1p1  42821  aks4d1p2  42822  aks4d1p3  42823  aks4d1p5  42825  aks4d1p6  42826  aks4d1p7d1  42827  aks4d1p7  42828  aks4d1p8  42832  aks4d1p9  42833  posbezout  42845  aks6d1c3  42868  2ap1caineq  42890  aks6d1c6lem4  42918  aks6d1c7lem1  42925  aks6d1c7lem2  42926  oexpreposd  43061  asin1half  43096  pellfundex  43593  jm2.22  43702  jm2.23  43703  imo72b2lem0  44871  sumnnodd  46326  sinaover2ne0  46562  stoweidlem14  46708  stoweidlem49  46743  stoweidlem52  46746  wallispilem4  46762  wallispi2lem2  46766  stirlinglem6  46773  stirlinglem15  46782  stirlingr  46784  dirkerval2  46788  dirkertrigeqlem3  46794  dirkercncflem4  46800  fourierdlem24  46825  fourierdlem79  46879  fourierdlem103  46903  fourierdlem104  46904  fourierdlem112  46912  fourierswlem  46924  fouriersw  46925  nthrucw  47582  goldrapos  47597  2ltceilhalf  48046  2tceilhalfelfzo1  48050  lighneallem4a  48337  nprmdvdsfacm1lem4  48352  nnoALTV  48437  nn0oALTV  48438  nn0e  48439  nneven  48440  evengpoap3  48541  gpg3kgrtriexlem1  48825  nn0eo  49285  flnn0div2ge  49290  fldivexpfllog2  49322  fllog2  49325  blennngt2o2  49349  dignn0flhalf  49375  sepfsepc  49683