Theorem 2pos 12319

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

Syntax hints:   class class class wbr 5099  0cc0 11070   < clt 11213  2c2 12269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-mulcom 11134  ax-addass 11135  ax-mulass 11136  ax-distr 11137  ax-i2m1 11138  ax-1ne0 11139  ax-1rid 11140  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143  ax-pre-lttri 11144  ax-pre-lttrn 11145  ax-pre-ltadd 11146  ax-pre-mulgt0 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-riota 7349  df-ov 7395  df-oprab 7396  df-mpo 7397  df-om 7843  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-er 8673  df-en 8924  df-dom 8925  df-sdom 8926  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11413  df-neg 11414  df-nn 12208  df-2 12277

This theorem is referenced by:  halfgt0  12433  halflt1  12435  halfpos2  12447  halfnneg2  12449  nominpos  12455  avglt1  12456  avglt2  12457  nn0n0n1ge2b  12547  3halfnz  12649  2rp  12995  hashgt23el  14434  s3fv0  14901  sqreulem  15370  cos2bnd  16203  sin02gt0  16207  sincos2sgn  16209  sin4lt0  16210  epos  16222  sqrt2re  16265  nnoddm1d2  16403  2mulprm  16710  prmgaplem7  17076  slotsdifdsndx  17406  odrngstr  17415  imasvalstr  17463  psgnunilem2  19518  cnfldstr  21406  bl2in  24440  iihalf1  24973  iihalf2  24975  pcoass  25066  tcphcphlem1  25277  trirn  25442  minveclem2  25468  minveclem4  25474  ovolunlem1a  25538  vitalilem4  25653  mbfi1fseqlem5  25761  pilem2  26492  pilem3  26493  pipos  26500  sinhalfpilem  26505  sincosq1lem  26539  tangtx  26547  sinq12gt0  26549  tan4thpi  26556  sincos6thpi  26558  cosordlem  26572  tanord1  26579  efif1olem2  26585  efif1olem4  26587  cxpcn3lem  26789  ang180lem1  26851  ang180lem2  26852  atantan  26965  atanbndlem  26967  atans2  26973  leibpi  26984  log2tlbnd  26987  basellem1  27122  basellem2  27123  basellem3  27124  ppiltx  27218  ppiub  27245  chtublem  27252  chtub  27253  chpval2  27259  bcmono  27318  bpos1lem  27323  bposlem1  27325  bposlem2  27326  bposlem3  27327  bposlem4  27328  bposlem5  27329  bposlem6  27330  bposlem7  27331  gausslemma2dlem0c  27399  gausslemma2dlem1a  27406  gausslemma2dlem2  27408  gausslemma2dlem3  27409  lgseisenlem1  27416  lgseisenlem2  27417  lgseisenlem3  27418  lgsquadlem1  27421  lgsquadlem2  27422  2lgslem1a1  27430  2lgslem1a2  27431  2lgslem1c  27434  chebbnd1lem1  27510  chebbnd1lem2  27511  chebbnd1lem3  27512  chebbnd1  27513  chtppilimlem1  27514  chtppilimlem2  27515  chtppilim  27516  chebbnd2  27518  chto1lb  27519  chpchtlim  27520  chpo1ub  27521  dchrisum0fno1  27552  mulog2sumlem2  27576  selberglem2  27587  selberg2lem  27591  chpdifbndlem1  27594  logdivbnd  27597  pntrsumo1  27606  pntpbnd1a  27626  pntlemh  27640  pntlemr  27643  pntlemk  27647  pntlemo  27648  pnt2  27654  umgrislfupgrlem  29269  lfgrnloop  29272  lfuhgr1v0e  29401  wwlksnextwrd  30043  wwlksnextfun  30044  wwlksnextinj  30045  clwlkclwwlklem2a2  30141  konigsberg  30405  ex-fl  30595  minvecolem2  31024  minvecolem4  31029  bcsiALT  31328  opsqrlem6  32294  cdj3lem1  32583  wrdt2ind  33092  cyc2fv2  33263  rtelextdg2lem  33984  2sqr3minply  34038  sqsscirc1  34166  omssubadd  34558  signslema  34820  hgt750lem  34909  subfacval3  35503  nn0prpwlem  36646  knoppndvlem18  36931  knoppndvlem19  36932  knoppndvlem21  36934  cnndvlem1  36939  iccioo01  37785  sin2h  38073  cos2h  38074  tan2h  38075  itg2addnclem  38134  3lexlogpow5ineq2  42636  3lexlogpow5ineq4  42637  3lexlogpow5ineq3  42638  3lexlogpow2ineq1  42639  3lexlogpow2ineq2  42640  3lexlogpow5ineq5  42641  aks4d1lem1  42643  aks4d1p1p3  42650  aks4d1p1p2  42651  aks4d1p1p4  42652  aks4d1p1p6  42654  aks4d1p1p7  42655  aks4d1p1p5  42656  aks4d1p1  42657  aks4d1p2  42658  aks4d1p3  42659  aks4d1p5  42661  aks4d1p6  42662  aks4d1p7d1  42663  aks4d1p7  42664  aks4d1p8  42668  aks4d1p9  42669  posbezout  42681  aks6d1c3  42704  2ap1caineq  42726  aks6d1c6lem4  42754  aks6d1c7lem1  42761  aks6d1c7lem2  42762  oexpreposd  42895  asin1half  42930  pellfundex  43427  jm2.22  43536  jm2.23  43537  imo72b2lem0  44705  sumnnodd  46170  sinaover2ne0  46406  stoweidlem14  46552  stoweidlem49  46587  stoweidlem52  46590  wallispilem4  46606  wallispi2lem2  46610  stirlinglem6  46617  stirlinglem15  46626  stirlingr  46628  dirkerval2  46632  dirkertrigeqlem3  46638  dirkercncflem4  46644  fourierdlem24  46669  fourierdlem79  46723  fourierdlem103  46747  fourierdlem104  46748  fourierdlem112  46756  fourierswlem  46768  fouriersw  46769  nthrucw  47426  goldrapos  47441  2ltceilhalf  47890  2tceilhalfelfzo1  47894  lighneallem4a  48181  nprmdvdsfacm1lem4  48196  nnoALTV  48281  nn0oALTV  48282  nn0e  48283  nneven  48284  evengpoap3  48385  gpg3kgrtriexlem1  48669  nn0eo  49114  flnn0div2ge  49119  fldivexpfllog2  49151  fllog2  49154  blennngt2o2  49178  dignn0flhalf  49204  sepfsepc  49513