Theorem 2pos 12336

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

Syntax hints:   class class class wbr 5105  0cc0 11088   < clt 11231  2c2 12286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-nn 12225  df-2 12294

This theorem is referenced by:  halfgt0  12450  halflt1  12452  halfpos2  12464  halfnneg2  12466  nominpos  12472  avglt1  12473  avglt2  12474  nn0n0n1ge2b  12564  3halfnz  12666  2rp  13012  hashgt23el  14451  s3fv0  14918  sqreulem  15401  cos2bnd  16234  sin02gt0  16238  sincos2sgn  16240  sin4lt0  16241  epos  16253  sqrt2re  16296  nnoddm1d2  16434  2mulprm  16741  prmgaplem7  17107  slotsdifdsndx  17437  odrngstr  17446  imasvalstr  17494  psgnunilem2  19556  cnfldstr  21484  bl2in  24518  iihalf1  25051  iihalf2  25053  pcoass  25144  tcphcphlem1  25355  trirn  25520  minveclem2  25546  minveclem4  25552  ovolunlem1a  25616  vitalilem4  25731  mbfi1fseqlem5  25839  pilem2  26573  pilem3  26574  pipos  26581  sinhalfpilem  26586  sincosq1lem  26620  tangtx  26628  sinq12gt0  26630  tan4thpi  26637  sincos6thpi  26639  cosordlem  26653  tanord1  26660  efif1olem2  26666  efif1olem4  26668  cxpcn3lem  26870  ang180lem1  26932  ang180lem2  26933  atantan  27046  atanbndlem  27048  atans2  27054  leibpi  27065  log2tlbnd  27068  basellem1  27203  basellem2  27204  basellem3  27205  ppiltx  27299  ppiub  27326  chtublem  27333  chtub  27334  chpval2  27340  bcmono  27399  bpos1lem  27404  bposlem1  27406  bposlem2  27407  bposlem3  27408  bposlem4  27409  bposlem5  27410  bposlem6  27411  bposlem7  27412  gausslemma2dlem0c  27480  gausslemma2dlem1a  27487  gausslemma2dlem2  27489  gausslemma2dlem3  27490  lgseisenlem1  27497  lgseisenlem2  27498  lgseisenlem3  27499  lgsquadlem1  27502  lgsquadlem2  27503  2lgslem1a1  27511  2lgslem1a2  27512  2lgslem1c  27515  chebbnd1lem1  27591  chebbnd1lem2  27592  chebbnd1lem3  27593  chebbnd1  27594  chtppilimlem1  27595  chtppilimlem2  27596  chtppilim  27597  chebbnd2  27599  chto1lb  27600  chpchtlim  27601  chpo1ub  27602  dchrisum0fno1  27633  mulog2sumlem2  27657  selberglem2  27668  selberg2lem  27672  chpdifbndlem1  27675  logdivbnd  27678  pntrsumo1  27687  pntpbnd1a  27707  pntlemh  27721  pntlemr  27724  pntlemk  27728  pntlemo  27729  pnt2  27735  umgrislfupgrlem  29381  lfgrnloop  29384  lfuhgr1v0e  29513  wwlksnextwrd  30155  wwlksnextfun  30156  wwlksnextinj  30157  clwlkclwwlklem2a2  30253  konigsberg  30517  ex-fl  30707  minvecolem2  31136  minvecolem4  31141  bcsiALT  31440  opsqrlem6  32406  cdj3lem1  32695  wrdt2ind  33186  cyc2fv2  33355  rtelextdg2lem  34033  2sqr3minply  34087  sqsscirc1  34215  omssubadd  34607  signslema  34866  hgt750lem  34955  subfacval3  35552  nn0prpwlem  36695  knoppndvlem18  36980  knoppndvlem19  36981  knoppndvlem21  36983  cnndvlem1  36988  iccioo01  37833  sin2h  38121  cos2h  38122  tan2h  38123  itg2addnclem  38182  3lexlogpow5ineq2  42684  3lexlogpow5ineq4  42685  3lexlogpow5ineq3  42686  3lexlogpow2ineq1  42687  3lexlogpow2ineq2  42688  3lexlogpow5ineq5  42689  aks4d1lem1  42691  aks4d1p1p3  42698  aks4d1p1p2  42699  aks4d1p1p4  42700  aks4d1p1p6  42702  aks4d1p1p7  42703  aks4d1p1p5  42704  aks4d1p1  42705  aks4d1p2  42706  aks4d1p3  42707  aks4d1p5  42709  aks4d1p6  42710  aks4d1p7d1  42711  aks4d1p7  42712  aks4d1p8  42716  aks4d1p9  42717  posbezout  42729  aks6d1c3  42752  2ap1caineq  42774  aks6d1c6lem4  42802  aks6d1c7lem1  42809  aks6d1c7lem2  42810  oexpreposd  42943  asin1half  42978  pellfundex  43475  jm2.22  43584  jm2.23  43585  imo72b2lem0  44753  sumnnodd  46204  sinaover2ne0  46440  stoweidlem14  46586  stoweidlem49  46621  stoweidlem52  46624  wallispilem4  46640  wallispi2lem2  46644  stirlinglem6  46651  stirlinglem15  46660  stirlingr  46662  dirkerval2  46666  dirkertrigeqlem3  46672  dirkercncflem4  46678  fourierdlem24  46703  fourierdlem79  46757  fourierdlem103  46781  fourierdlem104  46782  fourierdlem112  46790  fourierswlem  46802  fouriersw  46803  nthrucw  47460  goldrapos  47475  2ltceilhalf  47924  2tceilhalfelfzo1  47928  lighneallem4a  48215  nprmdvdsfacm1lem4  48230  nnoALTV  48315  nn0oALTV  48316  nn0e  48317  nneven  48318  evengpoap3  48419  gpg3kgrtriexlem1  48703  nn0eo  49159  flnn0div2ge  49164  fldivexpfllog2  49196  fllog2  49199  blennngt2o2  49223  dignn0flhalf  49249  sepfsepc  49557