Theorem 2pos 12450

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

This proof depends on syntax axioms:   class class class wbr 5102  0cc0 11203   < clt 11346  2c2 12400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  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 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-er 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-nn 12339  df-2 12408

This theorem is used by:  halfgt0  12564  halflt1  12566  halfpos2  12578  halfnneg2  12580  nominpos  12586  avglt1  12587  avglt2  12588  nn0n0n1ge2b  12678  3halfnz  12781  2rp  13128  hashgt23el  14572  s3fv0  15047  sqreulem  15532  cos2bnd  16361  sin02gt0  16365  sincos2sgn  16367  sin4lt0  16368  epos  16380  sqrt2re  16423  nnoddm1d2  16561  2mulprm  16873  prmgaplem7  17240  slotsdifdsndx  17570  odrngstr  17579  imasvalstr  17627  psgnunilem2  19714  cnfldstr  21685  bl2in  24724  iihalf1  25257  iihalf2  25259  pcoass  25350  tcphcphlem1  25561  trirn  25726  minveclem2  25752  minveclem4  25758  ovolunlem1a  25822  vitalilem4  25937  mbfi1fseqlem5  26045  pilem2  26784  pilem3  26785  pipos  26792  sinhalfpilem  26797  sincosq1lem  26831  tangtx  26839  sinq12gt0  26841  tan4thpi  26848  sincos6thpi  26849  cosordlem  26863  tanord1  26870  efif1olem2  26876  efif1olem4  26878  cxpcn3lem  27080  ang180lem1  27142  ang180lem2  27143  atantan  27256  atanbndlem  27258  atans2  27264  leibpi  27275  log2tlbnd  27278  basellem1  27413  basellem2  27414  basellem3  27415  ppiltx  27509  ppiub  27536  chtublem  27543  chtub  27544  chpval2  27550  bcmono  27609  bpos1lem  27614  bposlem1  27616  bposlem2  27617  bposlem3  27618  bposlem4  27619  bposlem5  27620  bposlem6  27621  bposlem7  27622  gausslemma2dlem0c  27690  gausslemma2dlem1a  27697  gausslemma2dlem2  27699  gausslemma2dlem3  27700  lgseisenlem1  27707  lgseisenlem2  27708  lgseisenlem3  27709  lgsquadlem1  27712  lgsquadlem2  27713  2lgslem1a1  27721  2lgslem1a2  27722  2lgslem1c  27725  chebbnd1lem1  27801  chebbnd1lem2  27802  chebbnd1lem3  27803  chebbnd1  27804  chtppilimlem1  27805  chtppilimlem2  27806  chtppilim  27807  chebbnd2  27809  chto1lb  27810  chpchtlim  27811  chpo1ub  27812  dchrisum0fno1  27843  mulog2sumlem2  27867  selberglem2  27878  selberg2lem  27882  chpdifbndlem1  27885  logdivbnd  27888  pntrsumo1  27897  pntpbnd1a  27917  pntlemh  27931  pntlemr  27934  pntlemk  27938  pntlemo  27939  pnt2  27945  umgrislfupgrlem  29705  lfgrnloop  29708  lfuhgr1v0e  29840  wwlksnextwrd  30491  wwlksnextfun  30492  wwlksnextinj  30493  clwlkclwwlklem2a2  30589  konigsberg  30863  ex-fl  31053  minvecolem2  31482  minvecolem4  31487  bcsiALT  31786  opsqrlem6  32752  cdj3lem1  33041  wrdt2ind  33562  cyc2fv2  33729  rtelextdg2lem  34404  2sqr3minply  34458  sqsscirc1  34586  omssubadd  34978  signslema  35237  hgt750lem  35326  subfacval3  36040  nn0prpwlem  37202  knoppndvlem18  37487  knoppndvlem19  37488  knoppndvlem21  37490  cnndvlem1  37495  iccioo01  38343  sin2h  38626  cos2h  38627  tan2h  38628  itg2addnclem  38682  3lexlogpow5ineq2  43198  3lexlogpow5ineq4  43199  3lexlogpow5ineq3  43200  3lexlogpow2ineq1  43201  3lexlogpow2ineq2  43202  3lexlogpow5ineq5  43203  aks4d1lem1  43205  aks4d1p1p3  43212  aks4d1p1p2  43213  aks4d1p1p4  43214  aks4d1p1p6  43216  aks4d1p1p7  43217  aks4d1p1p5  43218  aks4d1p1  43219  aks4d1p2  43220  aks4d1p3  43221  aks4d1p5  43223  aks4d1p6  43224  aks4d1p7d1  43225  aks4d1p7  43226  aks4d1p8  43230  aks4d1p9  43231  posbezout  43243  aks6d1c3  43266  2ap1caineq  43288  aks6d1c6lem4  43316  aks6d1c7lem1  43323  aks6d1c7lem2  43324  oexpreposd  43472  asin1half  43501  pellfundex  43986  jm2.22  44095  jm2.23  44096  imo72b2lem0  45258  sumnnodd  46735  sinaover2ne0  46971  stoweidlem14  47117  stoweidlem49  47152  stoweidlem52  47155  wallispilem4  47171  wallispi2lem2  47175  stirlinglem6  47182  stirlinglem15  47191  stirlingr  47193  dirkerval2  47197  dirkertrigeqlem3  47203  dirkercncflem4  47209  fourierdlem24  47234  fourierdlem79  47288  fourierdlem103  47312  fourierdlem104  47313  fourierdlem112  47321  fourierswlem  47333  fouriersw  47334  goldrapos  48023  goldratmolem4  48028  goldratval  48029  2ltceilhalf  48495  2tceilhalfelfzo1  48499  lighneallem4a  48786  nprmdvdsfacm1lem4  48801  nnoALTV  48886  nn0oALTV  48887  nn0e  48888  nneven  48889  evengpoap3  48990  gpg3kgrtriexlem1  49274  nn0eo  49733  flnn0div2ge  49738  fldivexpfllog2  49770  fllog2  49773  blennngt2o2  49797  dignn0flhalf  49823  sepfsepc  50135